collecting requirements for FDs

[Ross Paterson]

On Wed, Apr 12, 2006 at 03:57:31PM +0100, Henrik Nilsson wrote:
> Here are some classes from Yampa/earlier versions of FRP.

The instances are probably more important, especially instances that
violate the following restriction (from the original description
of FDs, christened the "coverage condition" in the FD-CHR paper):
any type variable occurring in a range argument must also occur in a
domain argument.  The following (from mtl) satisfies this condition
(and is therefore boring):

	class (Monoid w, Monad m) => MonadWriter w m | m -> w

	instance (Monoid w, Monad m) => MonadWriter w (WriterT w m)

(because w occurs in WriterT w m) but this (also from mtl) does not:

	instance (Error e, MonadWriter w m) => MonadWriter w (ErrorT e m)

Here w is determined by ErrorT e m, via the FD on the context.  GHC and
Hugs use this laxer notion of dependency, but it has emerged that this
system is not well-behaved, so it has been proposed that we use some
intermediate conditions on instances.  One possibility is:

	Instances must either satisfy the coverage condition, or
	1) the functional dependency must be full, i.e. involve all
	   arguments of the class, and
	2) the range arguments of an instance must be distinct type
	   variables determined by domain variables, but not occurring
	   elsewhere in the instance head.

That's pretty clunky, but it handles the mtl instances.  Does it
permit enough of the uses people want?

> class (Floating a, VectorSpace v a) =>
>       AffineSpace p v a | p -> v, v -> a where
>     origin   :: p
>     (.+^)    :: p -> v -> p
>     (.-^)    :: p -> v -> p
>     (.-.)    :: p -> p -> v
>     distance :: p -> p -> a

The dependencies here are not full, so this is likely to be problematic.
Presumably you can't split the class because you want the default
definition of distance to use (.-.) and norm.

> FRPCore.lhs:  class RunningIn a b i | a -> i where
> FRPTask.lhs:> class MsgTaskMap mt m nt n | mt -> m, nt -> n where

Ditto