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