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