[Haskell-cafe] Quantification in Instance Contexts
Julian K. Arni
jkarni at gmail.com
Wed Jun 25 09:46:45 UTC 2014
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
More information about the Haskell-Cafe
mailing list