<div dir="ltr">Ultimately this is the wrong forum for this discussion as neither type equalities nor functional dependencies are in Haskell' at this time.</div><div class="gmail_extra"><br><br><div class="gmail_quote">
On Wed, May 1, 2013 at 7:04 PM, AntC <span dir="ltr"><<a href="mailto:anthony_clayden@clear.net.nz" target="_blank">anthony_clayden@clear.net.nz</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
> Martin Sulzmann <martin.sulzmann@...> writes:<br>
<div class="im"><br>
> > On Wed, May 1, 2013 at 11:13 AM, AntC <anthony_clayden@...> wrote:<br>
> ><br>
> > I want to replace FD's with Equality Constraints.<br>
><br>
> Ok, that's the bit I've missed, but then I argue that you can't fully<br>
> encode FDs.<br>
><br>
> Consider again the 'Sum' example.<br>
><br>
> In the FD world:<br>
><br>
> Sum x y z1, Sum x y z2 ==> z1 ~ z2<br>
><br>
> enforced by<br>
><br>
> Sum x y z | x y -> z<br>
<br>
</div>I'm still not sure you've 'got' it. The class has 2 FD's. Oleg put:<br>
<div class="im">> > ><br>
> > > class Sum x y z | x y -> z, x z -> y<br>
> > ><br>
<br>
><br>
</div><div class="im">> In my TF encoding, we find a similar derivation step<br>
><br>
> SumF1 x y ~ z1, SumF1 x y ~ z2 ==> z1 ~ z2<br>
><br>
<br>
</div>But you haven't captured the FD from {result, arg1} -> arg2.<br>
In the TF example you first posted, you expressed that with an explicit<br>
equality constraint. (I won't repeat yours, because it wasn't to do with<br>
Peano Arith.)<br>
<div class="im"><br>
<br>
> So, you're asking can we translate/express FDs using GHC intermediate<br>
> language with plain type equations only?<br>
<br>
</div>No, not asking, but stating; and not talking about the intermediate<br>
language, but the surface language.<br>
<br>
Could I respectfully suggest you re-read the OP.<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
<br>
_______________________________________________<br>
Haskell-prime mailing list<br>
<a href="mailto:Haskell-prime@haskell.org">Haskell-prime@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-prime" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-prime</a><br>
</div></div></blockquote></div><br></div>