# 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 `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!