<div dir="ltr"><div><div><div><div><div><div><div>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.<br>
</div><br>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.<br>
<br></div>In prolog you'd have something like this:<br></div>path(A,C) :- path(A,B), path(B,C).<br></div>(havent used prolog for a while so syntax might be off)<br><br></div>If you translate this to first order logic you'd have:<br>
</div>\forall A,C.(path(A,C) <- \exists B.(path(A,B)^path(B,C)))<br><br></div>It is the existential that is emulated with the cwa and cannot be emulated in haskell's typesystem.<br></div><div class="gmail_extra"><br>
<br><div class="gmail_quote">On 25 June 2014 07:00, Julian Arni <span dir="ltr"><<a href="mailto:jkarni@gmail.com" target="_blank">jkarni@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">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.<br></div><div class="HOEnZb">
<div class="h5"><div class="gmail_extra">
<br><br><div class="gmail_quote">On Wed, Jun 25, 2014 at 3:06 PM, adam vogt <span dir="ltr"><<a href="mailto:vogt.adam@gmail.com" target="_blank">vogt.adam@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi Julian,<br>
<br>
Does each child have only one parent? In other words, is a larger<br>
"tree" still accepted if you use:<br>
<br>
class Child1 a b bool | a b -> bool, b -> a<br>
<br>
instead of your Child.<br>
<br>
Regards,<br>
Adam<br>
<div><div><br>
<br>
On Wed, Jun 25, 2014 at 5:46 AM, Julian K. Arni <<a href="mailto:jkarni@gmail.com" target="_blank">jkarni@gmail.com</a>> wrote:<br>
> Hi Cafe,<br>
><br>
> I'm playing around with simple logic-programming at the type level. For<br>
> instance, encoding trees:<br>
><br>
>>> {-# LANGUAGE MultiParamTypeClasses<br>
>>> , FunctionalDependencies<br>
>>> , FlexibleInstances<br>
>>> , UndecidableInstances<br>
>>> , FlexibleContexts<br>
>>> , OverlappingInstances #-}<br>
>>> {-# OPTIONS_GHC -fcontext-stack=100 #-}<br>
>>><br>
>>><br>
>>> -- *A<br>
>>> -- / \<br>
>>> -- B* *C<br>
>>> -- |<br>
>>> -- D*<br>
>>><br>
>>><br>
>>> data A<br>
>>> data B<br>
>>> data C<br>
>>> data D<br>
>>> class Child a b bool | a b -> bool<br>
>>> instance Child A B TrueT<br>
>>> instance Child B D TrueT<br>
>>> instance Child B C TrueT<br>
>>> class Path a b bool | a b -> bool<br>
><br>
> Now the following obviously doesn't work (never mind for now that 'Path' needs<br>
> a recursive definition, and that this is really just 'Grandchild'):<br>
><br>
>>> instance (Child a b TrueT, Child b c TrueT) => Path a c TrueT<br>
><br>
> Because 'b' is ambiguous. Fair enough. But I can't directly use a fundep,<br>
> because 'b' *is* in fact ambiguous. What I want to tell the compiler is that<br>
> it's really okay, since the RHS side (and any possible 'where' expressions)<br>
> doesn't depend on what is instantiated for 'b'.<br>
><br>
> I know I could switch to a class 'Children a bs bool' and encode all children<br>
> of as a type-level list, and then have a fundep between 'a' and 'bs'. That's<br>
> not a *bad* solution: it does give a good sense of the intention. But it's not<br>
> very extensible; really I'd rather be using something like 'forall'<br>
> - something, I would guess, along the lines of:<br>
><br>
>>> instance forall a c. (forall b. (Child a b TrueT, Child b c TrueT)) => Path<br>
>>> a c TrueT<br>
><br>
> That, however, fails with:<br>
><br>
> Malformed instance head: (forall b.<br>
> (Child a b TrueT, Child b c TrueT))<br>
> -> Path a c TrueT<br>
> In the instance declaration for ‘Path a c TrueT’<br>
><br>
><br>
> So: is there a way (presumably with 'forall') of telling the compiler that the<br>
> ambiguous type 'b' actually won't "leak through" to the RHS, so stop bugging me<br>
> about ambiguity?<br>
><br>
> Thanks,<br>
> Julian<br>
</div></div>> _______________________________________________<br>
> Haskell-Cafe mailing list<br>
> <a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br></div>
</div></div><br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br></div>