Ideas/GADTPlan

—categories: Development …


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 PatchSeqs:

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!