> Martin Sulzmann <martin.sulzmann@...> writes:

> > On Wed, May 1, 2013 at 11:13 AM, AntC <anthony_clayden@...> wrote:
> >
> > I want to replace FD's with Equality Constraints.
>
> Ok, that's the bit I've missed, but then I argue that you can't fully
> encode FDs.
>
> Consider again the 'Sum' example.
>
> In the FD world:
>
> Sum x y z1, Sum x y z2  ==> z1 ~ z2
>
> enforced by
>
> Sum x y z | x y -> z

I'm still not sure you've 'got' it. The class has 2 FD's. Oleg put:

> > >
> > >        class Sum x y z | x y -> z, x z -> y
> > >

>

> In my TF encoding, we find a similar derivation step
>
> SumF1 x y ~ z1, SumF1 x y ~ z2 ==> z1 ~ z2
>

But you haven't captured the FD from {result, arg1} -> arg2.
In the TF example you first posted, you expressed that with an explicit
equality constraint. (I won't repeat yours, because it wasn't to do with
Peano Arith.)

> So, you're asking can we translate/express FDs using GHC intermediate
> language with plain type equations only?

No, not asking, but stating; and not talking about the intermediate
language, but the surface language.

Could I respectfully suggest you re-read the OP.

_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime