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
