Cafe, 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? Cheers, Tom _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
