Hi Cafe, I'm playing around with simple logic-programming at the type level. For instance, encoding trees:
{-# LANGUAGE MultiParamTypeClasses , FunctionalDependencies , FlexibleInstances , UndecidableInstances , FlexibleContexts , OverlappingInstances #-} {-# OPTIONS_GHC -fcontext-stack=100 #-}
-- *A -- / \ -- B* *C -- | -- D*
data A data B data C data D class Child a b bool | a b -> bool instance Child A B TrueT instance Child B D TrueT instance Child B C TrueT class Path a b bool | a b -> bool
Now the following obviously doesn't work (never mind for now that 'Path' needs a recursive definition, and that this is really just 'Grandchild'):
instance (Child a b TrueT, Child b c TrueT) => Path a c TrueT
Because 'b' is ambiguous. Fair enough. But I can't directly use a fundep, because 'b' *is* in fact ambiguous. What I want to tell the compiler is that it's really okay, since the RHS side (and any possible 'where' expressions) doesn't depend on what is instantiated for 'b'. I know I could switch to a class 'Children a bs bool' and encode all children of as a type-level list, and then have a fundep between 'a' and 'bs'. That's not a *bad* solution: it does give a good sense of the intention. But it's not very extensible; really I'd rather be using something like 'forall' - something, I would guess, along the lines of:
instance forall a c. (forall b. (Child a b TrueT, Child b c TrueT)) => Path a c TrueT
That, however, fails with: Malformed instance head: (forall b. (Child a b TrueT, Child b c TrueT)) -> Path a c TrueT In the instance declaration for ‘Path a c TrueT’ So: is there a way (presumably with 'forall') of telling the compiler that the ambiguous type 'b' actually won't "leak through" to the RHS, so stop bugging me about ambiguity? Thanks, Julian