[Haskell-cafe] Type Family Relations
mad.one at gmail.com
Sat Jan 3 12:45:57 EST 2009
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:
More information about the Haskell-Cafe