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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Thomas DuBuisson
I've been fighting this same problem for a while. The solution I've
come up with is to encode the axioms into a typeclass which gives you a proof of the axioms. Here's an excerpt from some code I've been playing around with; HaskTy and Lift are type families. -- Theorem: for all t instance of Lift, (forall env. HaskTy (Lift t) env == t) data HaskTy_Lift_Id t env = (t ~ HaskTy (Lift t) env) => HaskTy_Lift_Id class Thm_HaskTy_Lift_Id t where thm_haskty_lift_id :: forall env. HaskTy_Lift_Id t env instance Thm_HaskTy_Lift_Id Int where thm_haskty_lift_id = HaskTy_Lift_Id instance Thm_HaskTy_Lift_Id Bool where thm_haskty_lift_id = HaskTy_Lift_Id lemma_haskty_lift_id_app :: HaskTy_Lift_Id a env -> HaskTy_Lift_Id b env -> HaskTy_Lift_Id (a -> b) env lemma_haskty_lift_id_app HaskTy_Lift_Id HaskTy_Lift_Id = HaskTy_Lift_Id instance (Thm_HaskTy_Lift_Id a, Thm_HaskTy_Lift_Id b) => Thm_HaskTy_Lift_Id (a -> b) where thm_haskty_lift_id = lemma_haskty_lift_id_app thm_haskty_lift_id thm_haskty_lift_id As you can see, I encode a witness of the type equality into a concrete data type. You then direct the typechecker as to how to prove the type equality using the typeclass mechanism; the class instances closely mirror the type family instances. You then add this typeclass as a context on functions that require the equality. Control.Coroutine[1] uses a similar restriction: class Connect s where connect :: (s ~ Dual c, c ~ Dual s) => InSession s a -> InSession c b -> (a,b) A cleaner solution, that sadly doesn't work in GHC6.10 [2], would be something like: class (s ~ Dual (Dual s)) => Connect s where connect :: InSession s a -> InSession (Dual s) b -> (a,b) The difference is mainly one of efficiency; even though there is only one constructor for Thm_HaskTy_Lift_Id t env, at runtime the code still has to prove that evaluation terminates (to avoid _|_ giving an unsound proof of type equality). This means that deeply nested instances of the (a -> b) instance require calling dictionary constructors to match the tree, until eventually we see that each leaf is a valid constructor. If the type equality could be brought into scope by just bringing the typeclass into scope, the dictionaries themselves could remain unevaluated at runtime. -- ryan [1] http://hackage.haskell.org/cgi-bin/hackage-scripts/package/Coroutine [2] http://hackage.haskell.org/trac/ghc/ticket/2102 On Sat, Jan 3, 2009 at 7:22 AM, Thomas DuBuisson <[hidden email]> 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 > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe > Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Thomas DuBuisson
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 <[hidden email]> 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 > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe > Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 <[hidden email]> 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 > <[hidden email]> 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 >> [hidden email] >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> > Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 <[hidden email]> 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 <[hidden email]> 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 >> <[hidden email]> 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 >>> [hidden email] >>> http://www.haskell.org/mailman/listinfo/haskell-cafe >>> >> > _______________________________________________ > Haskell-Cafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe > Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
> 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? Hi Iavor, I think that >>> class HeaderOf addr hdr | addr -> hdr does not enforce that there must be a corresponding instance AddressOf hdr addr. Hence, the type checker cannot use that information either. Do you have a way to remedy that? Cheers, Tom > On Sat, Jan 3, 2009 at 8:35 PM, Thomas DuBuisson > <[hidden email]> 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 <[hidden email]> 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 >>> <[hidden email]> 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 >>>> [hidden email] >>>> http://www.haskell.org/mailman/listinfo/haskell-cafe >>>> >>> >> _______________________________________________ >> Haskell-Cafe mailing list >> [hidden email] >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> > _______________________________________________ > Haskell-Cafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe > -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: [hidden email] url: http://www.cs.kuleuven.be/~toms/ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Thomas DuBuisson
Hi Thomas,
The specific problem you describe has a simple solution using multiple parameter classes with syntactic sugar for functional notation instead of type families [1]: > class AddressOf h a | h -> a, a -> h -- bijections > class HeaderOf a h | a -> h, h -> a > instance HeaderOf (AddressOf h) h -- "your axiom" By the way, without the syntactic sugar, the instance declaration shown here is just: > instance AddressOf h a => HeaderOf a h -- also "your axiom" Individual (address,header) pairs are documented with a single instance, as in: > instance AddressOf IPv4Header IPv4 And now the type system can derive "HeaderOf IPv4 IPv4Header" automatically using "your axiom". But you won't be able to add the invalid AppHeader example because it will conflict (either with overlapping instances or with covering, depending on how you approach it). I like this approach because we only have to give a single instance instead of writing a pair of declarations that have to be checked for mutual consistency. I conclude that perhaps your example doesn't illustrate the kind of "arbitrarily complex" constraints you had in mind. Maybe you could elaborate? All the best, Mark [1] http://web.cecs.pdx.edu/~mpj/pubs/fundeps-design.html Thomas DuBuisson 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 > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Thomas DuBuisson
Hi,
> I think that > >>> class HeaderOf addr hdr | addr -> hdr > does not enforce that there must be a corresponding instance > AddressOf hdr addr. Hence, the type checker cannot use that information > either. Do you have a way to remedy that? I've often wanted something similar, and experimenting with this the following two options seem to be equivalent and work as desired: ----------------------------------------------------------------------------- -- both options share this code: -- | The crucial assertion ipv4 :: AddrHdrPair IPv4 IPv4Header ipv4 = AddrHdrPair data IPv4Header = C1 data IPv4 = C2 data AppAddress = C3 data AppHeader = C4 ----------------------------------------------------------------------------- -- OPTION(1): -- type families + GADT with equality constraints type family HeaderOf addr type family AddressOf hdr data AddrHdrPair hdr addr where AddrHdrPair :: (hdr ~ HeaderOf addr ,addr ~ AddressOf hdr) => AddrHdrPair addr hdr type instance HeaderOf IPv4 = IPv4Header type instance AddressOf IPv4Header = IPv4 ----------------------------------------------------------------------------- -- OPTION(2): -- classes + GADT with instance constraints class HeaderOf addr hdr | addr -> hdr class AddressOf hdr addr | addr -> hdr data AddrHdrPair hdr addr where AddrHdrPair :: (HeaderOf addr hdr ,AddressOf hdr addr) => AddrHdrPair addr hdr instance AddressOf IPv4Header IPv4 instance HeaderOf IPv4 IPv4Header ----------------------------------------------------------------------------- -- And commenting out the above instances in turn -- to verify that everything indeed works, and to -- compare error message content: {- -- type instance HeaderOf IPv4 = IPv4Header Cafe0.hs:9:0: Couldn't match expected type `HeaderOf IPv4' against inferred type `IPv4Header' When generalising the type(s) for `ipv4' Failed, modules loaded: none. -- type instance AddressOf IPv4Header = IPv4 Cafe0.hs:9:0: Couldn't match expected type `AddressOf IPv4Header' against inferred type `IPv4' When generalising the type(s) for `ipv4' Failed, modules loaded: none. -} {- -- instance AddressOf IPv4Header IPv4 Cafe0.hs:9:7: No instance for (AddressOf IPv4Header IPv4) arising from a use of `AddrHdrPair' at Cafe0.hs:9:7-17 Possible fix: add an instance declaration for (AddressOf IPv4Header IPv4) In the expression: AddrHdrPair In the definition of `ipv4': ipv4 = AddrHdrPair Failed, modules loaded: none. -- instance HeaderOf IPv4 IPv4Header Cafe0.hs:9:7: No instance for (HeaderOf IPv4 IPv4Header) arising from a use of `AddrHdrPair' at Cafe0.hs:9:7-17 Possible fix: add an instance declaration for (HeaderOf IPv4 IPv4Header) In the expression: AddrHdrPair In the definition of `ipv4': ipv4 = AddrHdrPair Failed, modules loaded: none. -} -- endcode ----------------------------------------------------------------------------- I'm not sure if there are any circumstances under which these two don't behave equivalently. All the best, Matt _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Generalizing the previous post, with:
----------------------------------------------------------------------------- {-# LANGUAGE GADTs #-} module Equ where data a:==:b where Equ :: (a ~ b) => a:==:b symm :: (a:==:a) symm = Equ refl :: (a:==:b) -> (b:==:a) refl Equ = Equ trans :: (a:==:b) -> (b:==:c) -> (a:==:c) trans Equ Equ = Equ cast :: (a:==:b) -> (a -> b) cast Equ = id ----------------------------------------------------------------------------- We can do (e.g.): > data IPv4Header = C1 > data IPv4 = C2 > type instance HeaderOf IPv4 = IPv4Header > type instance AddressOf IPv4Header = IPv4 t0 :: IPv4 :==: AddressOf IPv4Header t0 = Equ t1 :: IPv4Header :==: HeaderOf IPv4 t1 = Equ t2 :: IPv4 :==: AddressOf (HeaderOf IPv4) t2 = Equ t3 :: IPv4Header :==: HeaderOf (AddressOf IPv4Header) t3 = Equ -- And interestingly `t6' shows that the type family option -- in the previous case is slightly stronger that the funcdeps -- option, ie the type fams one corresponds to the funcdeps -- addr -> hdr, hdr -> addr (instead of the weaker addr -> hdr). -- If this isn't desired I'd bet there's a way to modify the type -- instances to get the desired behavior. t5 :: AddrHdrPair a b -> a :==: AddressOf (HeaderOf a) t5 AddrHdrPair = Equ t6 :: AddrHdrPair a b -> b :==: HeaderOf (AddressOf b) t6 AddrHdrPair = Equ Matt _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Thomas DuBuisson
Thomas DuBuisson:
> 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? There are no type-level invariants, like your type axiom, at the moment, although there is active work in this area http://www.cs.kuleuven.be/~toms/Research/papers/plpv2009_draft.pdf -- Type Invariants for Haskell, T. Schrijvers, L.-J. Guillemette, S. Monnier. Accepted at PLPV 2009. However, there is a simple solution to your problem. To enforce a side condition on the type instances of two separate families, you need to bundle the families as associated types into a class. Then, you can impose side conditions by way of super class constraints. In your example, that *should* work as follows -- GHC currently doesn't accept this, due to superclass equalities not being fully implemented, but we'll solve this in a second step: > class (HeaderOf a ~ h, AddressOf h ~ a) => Protocol h a where > type AddressOf h > type HeaderOf a > > -- Valid: > instance Protocol IPv4Header IPv4 where > type AddressOf IPv4Header = IPv4 > type HeaderOf IPv4 = IPv4Header > > -- Invalid > instance Protocol AppHeader AppAddress where > type AddressOf AppHeader = AppAddress > type HeaderOf AppAddress = [AppHeader] Superclass equalities are currently only partially implemented and GHC rejects them for this reason. However, your application doesn't require the full power of superclass equalities and can be realised with normal type classes: > class EQ a b > instance EQ a a > > class (EQ (HeaderOf a) h, EQ (AddressOf h) a) => Protocol h a where > type AddressOf h > type HeaderOf a > > -- Valid: > instance Protocol IPv4Header IPv4 where > type AddressOf IPv4Header = IPv4 > type HeaderOf IPv4 = IPv4Header > > -- Invalid > instance Protocol AppHeader AppAddress where > type AddressOf AppHeader = AppAddress > type HeaderOf AppAddress = [AppHeader] With this definition, the invalid definition is rejected with the message > /Users/chak/Code/haskell/main.hs:34:9: > No instance for (EQ [AppHeader] AppHeader) > arising from the superclasses of an instance declaration > at /Users/chak/Code/haskell/main.hs:34:9-37 > Possible fix: > add an instance declaration for (EQ [AppHeader] AppHeader) > In the instance declaration for `Protocol AppHeader AppAddress' Manuel _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |