[Haskell-cafe] Type Family Relations

[Austin Seipp]

Excerpts from Thomas M. DuBuisson's message of Sat Jan 03 09:22:47 -0600 2009:
> 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?
> 

The problem is that type classes are open - anybody can
extend this family i.e.

> type instance AddressOf IPv4Header = IPv4
> type instance HeaderOf IPv4 = IPv4Header
> type instance AddressOf IPv6Header = IPv4
>
> ipv4func :: (AddressOf x ~ IPv4) => x -> ...

And it will perfectly accept arguments with a type of IPv6Header.

There is a proposal for extending GHC to support type invariants of
this nature, but it is not implemented:

      http://tomschrijvers.blogspot.com/2008/11/type-invariants-for-haskell.html

Austin