Labels and the tentative solution to the MPTC Dilemma

[Ross Paterson]

On Wed, Feb 15, 2006 at 08:29:48PM -0800, oleg at pobox.com wrote:
> This message shows the (extensible polymorphic) record selection code
> that requires neither overlapping instances and not even undecidable
> instances. Therefore, it works both in GHC and Hugs. This
> constructively shows that it is possible to write less-trivial code
> using functional dependencies and multi-parameter type classes as had
> been specified by Mark P. Jones -- that is, abiding by his syntactic
> decidability constraints.  Therefore, if Haskell' standardized the
> current practice -- which is implemented _both_ by GHC and Hugs (with
> no overlapping instances, no undecidable instances), the result can
> still be useful.

I'm afraid it's worse than that: current practice lacks a foundation, and
attempts to provide one have exposed flaws (see the FunctionalDependencies
page).  FDs as specified by Mark are significantly weaker than what is
implemented by GHC and Hugs.  Even so, the original specification needs
an additional restriction to prevent some non-terminating instances.

In line with recent studies of FDs by Sulzmann et al, the CVS version
of GHC has much tighter rules (closer to the original specification).
It also has a more liberal termination condition for instances (see the
end of FlexibleInstances), but this is only partial compensation.

For example,

> class TypeEq a b c | a b -> c
> class EqL1 a c | a -> c
> class EqL2 a c | a -> c
> instance EqL1 b c => TypeEq L1 b c
> instance EqL2 b c => TypeEq L2 b c

These instances are not permitted by the original restrictions: the
third (range) argument contains a variable (c) that does not occur in
the first two (domain) arguments.  A safe relaxation has been proposed
(see end of FunctionalDependencies) and Simon favours adding it to GHC.
It is quite complex, though.

> class Select dummy label val rec | label rec -> val where
>     lookp :: dummy -> rec -> label -> val

> instance (TypeEq label l tr, ProjLabel r l, Select' tr label val r)
>     => Select () label val r where
>     lookp () r label = lookup' (typeEq label (proj'label r)) r label

This instance (and the similar one for Select') were permitted by the
original rules, under a relaxation that has since been shown to produce
non-termination in some cases (CHR paper, ex. 15).  No replacement has
been proposed, so the relaxation has been removed from the CVS version
of GHC, which thus rejects this.