> 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
