[Haskell-cafe] Quantification in Instance Contexts

[Andras Slemmer]

Think about what you're asking from the compiler. If it sees a (Path a c)
constraint it would have to magically guess whether there is an
intermediate type b for which (Path a b) and (Path b c), which is
impossible.

Logic programming relies on the closed world assumption, meaning that if a
statement cannot be proven within the closed world we are working in then
it is false. Haskell typeclasses don't work like this; there is no closed
world of types, so the compiler cannot "refute" a constraint.

In prolog you'd have something like this:
path(A,C) :- path(A,B), path(B,C).
(havent used prolog for a while so syntax might be off)

If you translate this to first order logic you'd have:
\forall A,C.(path(A,C) <- \exists B.(path(A,B)^path(B,C)))

It is the existential that is emulated with the cwa and cannot be emulated
in haskell's typesystem.


On 25 June 2014 07:00, Julian Arni <jkarni at gmail.com> wrote:

> Alas, no. I tried to simplify the use case, but in fact the structure is a
> DAG, and each node may have multiple parents. So neither "a -> b" nor "b ->
> a" hold.
>
>
> On Wed, Jun 25, 2014 at 3:06 PM, adam vogt <vogt.adam at gmail.com> wrote:
>
>> Hi Julian,
>>
>> Does each child have only one parent? In other words, is a larger
>> "tree" still accepted if you use:
>>
>> class Child1 a b bool | a b -> bool, b -> a
>>
>> instead of your Child.
>>
>> Regards,
>> Adam
>>
>>
>> On Wed, Jun 25, 2014 at 5:46 AM, Julian K. Arni <jkarni at gmail.com> wrote:
>> > 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
>> > _______________________________________________
>> > Haskell-Cafe mailing list
>> > Haskell-Cafe at haskell.org
>> > http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140625/1801a17e/attachment.html>