Hello,
On Wed, Jun 15, 2011 at 10:49 AM, <dm-list-haskell-pr...@scs.stanford.edu>wrote:
> At Wed, 15 Jun 2011 10:10:14 -0700,
> Iavor Diatchki wrote:
> >
> > Hello,
> >
> > On Wed, Jun 15, 2011 at 12:25 AM, Simon Peyton-Jones <
> simo...@microsoft.com>
> > wrote:
> >
> > | > class C a b | a -> b where
> > | > foo :: a -> b
> > | > foo = error "Yo dawg."
> > | >
> > | > instance C a b where
> >
> > Wait. What about
> > instance C [a] [b]
> >
> > No, those two are not different, the instance "C [a] [b]" should also be
> > rejected because it violates the functional dependency.
>
> But now you are going to end up rejecting programs like this:
>
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE FunctionalDependencies #-}
> {-# LANGUAGE UndecidableInstances #-}
>
> class C a b | a -> b
> class D a b | a -> b
> instance (D a b) => C [a] [b]
>
> And a lot of useful code (including HList) depends on being able to do
> things like the above.
Nope, this program will not be rejected because "b" is in the FD closure of
"a". This stuff used to work a few GHC releases back, and I think that
this is the algorithm used by Hugs.
A functional dependency on a class imposes a constraint on the valid class
instances (in a similar fashion to adding super-class constraints to a
class). In general, checking this invariant may be hard, so it is fine for
implementations to be "incomplete" (i.e., reject some programs that do
satisfy the invariant or, perhaps, fail to terminate in the process). OTOH,
I think that if an implementation accepts a program that violates the
invariant, then this is a bug in the implementation.
>
> > The general rule defining an FD on a class like "C" is the following
> logical
> > statement:
> > "forall a b1 b2. (C a b1, C a b2) => (b1 = b2)"
>
> And in fact b1 and b2 are equal, up to alpha-conversion. They are
> both just free type variables.
No, this was intended to be a more "semantic" property. Here it is in
English:
For any three ground types "a", "b1", and "b2", if we can prove that both "C
a b1" and "C a b2" hold, then "b1" and "b2" must be the same type. The
theory of functional dependencies comes from databases. In that context, a
class corresponds to the schema for a database table (i.e., what columns
there are, and with what types). An instance corresponds to a rule that
adds row(s) to the table. With this in mind, the rule that I wrote above
exactly corresponds to the notion of a functional dependency on a database
table.
-Iavor
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
