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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
