Ultimately this is the wrong forum for this discussion as neither type
equalities nor functional dependencies are in Haskell' at this time.
On Wed, May 1, 2013 at 7:04 PM, AntC <anthony_clay...@clear.net.nz> wrote:
> > 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
>
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
