Hello, Usually, you can program such things by using super-classes. Here is how you could encode your example: {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances #-} class HeaderOf addr hdr | addr -> hdr class HeaderOf addr hdr => AddressOf hdr addr | addr -> hdr data IPv4Header = C1 data IPv4 = C2 data AppAddress = C3 data AppHeader = C4 instance AddressOf IPv4Header IPv4 instance HeaderOf IPv4 IPv4Header {- results in error: instance AddressOf AppHeader AppAddress instance HeaderOf AppAddress [AppHeader] -} Hope that this helps, Iavor On Sat, Jan 3, 2009 at 7:22 AM, Thomas DuBuisson <thomas.dubuisson@gmail.com> wrote:
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe