[Haskell-cafe] Type Family Relations

Thomas DuBuisson thomas.dubuisson at gmail.com
Sat Jan 3 10:22:47 EST 2009

I am wondering if there is a way to enforce compile time checking of
an axiom relating two separate type families.

Mandatory contrived example:

> type family AddressOf h
> type family HeaderOf a
> -- I'm looking for something to the effect of:
> type axiom HeaderOf (AddressOf x) ~ x
> -- Valid:
> type instance AddressOf IPv4Header = IPv4
> type instance HeaderOf IPv4 = IPv4Header
> -- Invalid
> type instance AddressOf AppHeader = AppAddress
> type instance HeaderOf AppAddress = [AppHeader]

So this is  a universally enforced type equivalence.  The stipulation
could be arbitrarily complex, checked at compile time, and must hold
for all instances of either type family.

Am I making this too hard?  Is there already a solution I'm missing?


More information about the Haskell-Cafe mailing list