[Haskell-cafe] Type Family Relations

[Matt Morrow]

Generalizing the previous post, with:

-----------------------------------------------------------------------------
{-# LANGUAGE GADTs #-}

module Equ where

data a:==:b where
  Equ :: (a ~ b) => a:==:b

symm :: (a:==:a)
symm = Equ

refl :: (a:==:b) -> (b:==:a)
refl Equ = Equ

trans :: (a:==:b) -> (b:==:c) -> (a:==:c)
trans Equ Equ = Equ

cast :: (a:==:b) -> (a -> b)
cast Equ = id
-----------------------------------------------------------------------------

We can do (e.g.):

> data IPv4Header = C1
> data IPv4       = C2
> type instance HeaderOf IPv4 = IPv4Header
> type instance AddressOf IPv4Header = IPv4

t0 :: IPv4 :==: AddressOf IPv4Header
t0 = Equ

t1 :: IPv4Header :==: HeaderOf IPv4
t1 = Equ

t2 :: IPv4 :==: AddressOf (HeaderOf IPv4)
t2 = Equ

t3 :: IPv4Header :==: HeaderOf (AddressOf IPv4Header)
t3 = Equ

-- And interestingly `t6' shows that the type family option
-- in the previous case is slightly stronger that the funcdeps
-- option, ie the type fams one corresponds to the funcdeps
-- addr -> hdr, hdr -> addr (instead of the weaker addr -> hdr).
-- If this isn't desired I'd bet there's a way to modify the type
-- instances to get the desired behavior.

t5 :: AddrHdrPair a b
    -> a :==: AddressOf (HeaderOf a)
t5 AddrHdrPair = Equ

t6 :: AddrHdrPair a b
    -> b :==: HeaderOf (AddressOf b)
t6 AddrHdrPair = Equ

Matt