[Haskell] The two-class trick

[oleg at pobox.com]

The two-class trick helps us indirectly write desirable
multi-parameter classes with functional dependencies or
overlapping. The example below happens to have both. The example
illustrates that an attempt to write desired instances directly runs
into problems of bad overlapping or violations of functional
dependencies. The trick lets us get around those unfortunately quite
common problems.

Many if not all problems with overlapping instances can be solved with
the general approach described in the HList paper [HList]. The paper
conjectures that the overlapping instances extension itself may be
unnecessary after all.

	The HList paper: http://www.cwi.nl/~ralf/HList/

The two-class trick still seems worth explaining because it gives an
example of turning an apparent drawback of the instance selection
algorithm to our advantage. In Haskell, class instances are chosen
based only on the syntactic shape of the type terms in
question. Specifically, instance constraints, if any, do _not_ affect
the instance selection. This fact is often considered one of the major
stumbling blocks to using Haskell overloading for ``logical
programming''. The instance selection algorithm is somewhat akin to the
selection of the appropriate function declaration clause. We can
influence the selection by adding a guard -- an arbitrary
boolean expression -- to a function clause. Alas, we cannot similarly
influence the selection of an instance by adding a constraint. If an
instance has a constraint, the latter is checked _after_ the
typechecker has selected and become committed to that instance. If
that constraint turns out unsatisfiable, the whole typechecking
fails. There is no backtracking: the typechecker does not attempt to
choose another instance.


This message is the complete code. Therefore, we need preliminaries

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
> {-# OPTIONS -fallow-overlapping-instances #-}
>
> module DelH where
>
> data HNil = HNil deriving Show
> data HCons a b = HCons a b deriving Show

A sample heterogenous list is as follows:

> l1 = HCons True $ HCons 'a' $ HCons "ab" $ HCons 'z' $ HNil

The HList paper defines infix operators that make building
heterogenous lists far more pleasant. Please see the HList paper
[HList] for much more explanations and many more operations on
heterogenous lists.


Our goal here is to write a function |hdel| that deletes the first
occurrence of an element of a given type from a given heterogeneous
list. For example,

> test1 = hdel 'x' l1

will delete the first element of the type |Char| from the list |l1|:

  *DelH> l1
  HCons True (HCons 'a' (HCons "ab" (HCons 'z' HNil)))
  *DelH> test1
  HCons True (HCons "ab" (HCons 'z' HNil))

The given list must contain at least one element of the desired type.
Otherwise, it is a type error.

We can start by writing

> class HDeleteFst e l l' | e l -> l' where
>    hdel:: e -> l -> l'

> instance HDeleteFst e (HCons e l) l where
>    hdel _ (HCons _ l) = l


At first, the code is quite straightforward: if we see the occurrence
of the desired element type in the head of |HList|, we return the tail
of the list. We are tempted to write the second case (when the desired
element type is not in the head of the list) as follows

*> instance HDeleteFst e l l' =>
*>          HDeleteFst e (HCons e' l) (HCons e' l') where
*>    hdel e (HCons e' l) = HCons e' (hdel e l)

Alas, that does not work. The most general unifier of the instances
	HDeleteFst e (HCons e l)  l
and
	HDeleteFst e (HCons e' l) (HCons e' l')
is
	e' -> e, l -> (HCons e l')

The unifier exists, therefore, the instances do overlap.  However, there
is no such substitution that, when applied to the second instance
makes it identical to the first, nor vice versa. So, the instances are
unifiable but not comparable -- and the compiler will complain.

The trick is to introduce a helper class

> class HDeleteFst' e l l' | e l -> l' where
>    hdel':: e -> l -> l'

which is in all respect similar to the first class. Now, we add a
relaying instance of |HDeleteFst|:

> instance HDeleteFst' e l l' => HDeleteFst e l l' where
>    hdel = hdel'

As we can see, the two instances of our class, 
|HDeleteFst e (HCons e l1) l1| and |HDeleteFst e l l'| still
overlap. Now, the former is strictly more specialized than the latter,
because there exists a substitution |l -> (HCons e l1), l -> l1|,
which, when applied to the general instance makes it identical to the
former instance. GHC no longer complains because now the overlapping 
instances are ordered and so the compiler can choose the right one.

We still need to add an instance for the new class |HDeleteFst'|

> instance HDeleteFst  e l l' =>
>          HDeleteFst' e (HCons e' l) (HCons e' l') where
>    hdel' e (HCons e' l) = HCons e' (hdel e l)

Modulo the substitution |HDeleteFst'| for |HDeleteFst| and
|hdel'| for |hdel|, this is precisely the instance we wanted -- but
could not write before. In writing the relaying instance of
|HDeleteFst| we specifically relied on the fact that instances are
chosen only on the syntactic shape of the type terms in question. The
constraints (in our case, |HDeleteFst' e l l'|) are checked only after
the selection is complete.