/!\\ This page is out-dated now that GADTs are in place. We should
probably rename it and tidy it up with the new syntax

--------------

The current definition of a patch doesn't take into account the
*context* of that patch. So commute et al. will allow you to
operate on patches that don't have compatible contexts, resulting
in bizarre and difficult-to-locate errors.

Wouldn't it be nice if the type system would catch these errors?
Let's give it a go.

We have our patch type, ``p``. Give it two new type arguments, a
and b, representing the starting and ending contexts. We call these
**phantom** type arguments because they're not used in the
definition of the type ``p``. So we don't ever have to worry about
instantiating them. Now let's look at the type of commute:

::

    commute :: p a b -> p b c -> Maybe (p a d, p d c)

The problem with this definition is that the type variables b and d
in commute are **universal**, which means that they can be *any*
type, even equal! Not really what we wanted.

What we want is some way to represent to the type system that the
result of commute uses a *new* context different from the other
contexts. For this, we use **existential types**. These represent
cases where the type system knows that a certain type variable
contains *some* type, but certainly isn't valid for *all* types, as
the definition above implies.

We use a generalized abstract data type (GADT) to build these
existential types:

::

    data Commutation p a c where
        (:.) :: p a b -> p b c -> Commutation p a c
    
    commute :: Commutation p a c -> Maybe (Commutation p a c)

Notice that the result of the constructor ``(:.)`` doesn't mention
``b``. Since it's a constructor, we can use it to unpack the
commutation:

::

    (a :. b) :: Commutation x z
    (b' :. a') <- commute (a :. b)

What are the types of ``a'`` and ``b'``? Well, we know that
``(b' :. a')`` is of type ``Commutation x z``. So it must have been
built from two types ``p x y`` and ``p y z``, where ``y`` is
*unknown*. This is the existential part of things: we know that
``y`` *exists*, but we don't know what it is. That's important --
we can't, for example, build ``(b' :. a)`` because the type system
can't guarantee that the types for ``b'`` and ``a`` are compatible.
In fact, they're probably not.

We can even define sequences of these patches, with chains of
existential types linking them:

::

    data PatchSeq p a b where
        Nil  :: PatchSeq p a a
        U    :: p a b -> PatchSeq p a b
        (:-) :: PatchSeq p a b -> PatchSeq p b c -> PatchSeq p a c

Note that the type variable ``b`` in the ``(:-)`` constructor is
properly existential.

How does all this help? Well, let's take, for example, part of the
definition of ``commute`` on ``PatchSeq``s:

::

    commute ((ps1 :- ps2) :. p)
        = do p'  :. ps1' <- commute (ps1 :. p)
             p'' :. ps2' <- commute (ps2 :. p')
             return (p'' :. (ps1' :- ps2'))

Looks reasonable, right? It would certainly type check under the
old definition of patches. But the new definition catches the
error: ``ps1``'s ending context is equal to **``ps2``**'s starting
context, not ``p``'s!

--------------

`CategoryDevelopers <CategoryDevelopers>`_