Hi, I like collecting examples of different type system related issues, and I am curious in what way is the solution that I posted limited. Do you happen to have an example? Thanks, Iavor
On Sat, Jan 3, 2009 at 8:35 PM, Thomas DuBuisson <[email protected]> wrote: > Thank you all for the responses. I find the solution that omits type > families [Diatchki] to be too limiting while the solution 'class (Dual > (Dual s) ~ s) =>' [Ingram] isn't globally enforced. I've yet to > closely study your first solution, Ryan, but it appears to be what I > was looking for - I'll give it a try in the coming week. > > Tom > > On Sat, Jan 3, 2009 at 8:18 PM, Iavor Diatchki <[email protected]> > wrote: >> 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 >> <[email protected]> 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 >>> [email protected] >>> http://www.haskell.org/mailman/listinfo/haskell-cafe >>> >> > _______________________________________________ > Haskell-Cafe mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
