## Thursday, January 11, 2007

### Type (Dis)equality

Type equality is the essential ingredient in guarded algebraic datatypes:

```data Z ; data S n ;

data ListGADT a n where
ConsListGADT :: a -> ListGADT a n -> ListGADT a (S n)

data TypeEqual a b = . . .
data ListEq a n = NilListEq (TypeEqual n Z)
| forall m . ConsListEq (TypeEqual n (S m)) a (ListEq a m)```
What new power would type disequality bring? It might prevent infinite types.
```data WrapList a = forall n . WrapList (ListGADT a n)

cons :: a -> WrapList a -> WrapList a
cons x (WrapList y) = WrapList (Cons x y)

ones = cons 1 ones```
Here, the size type inside ones is `S (S (S . . . `. That's bad. What if we wrote:
```data TypeDisEq a b where
DisEqLess :: DisEq Z (S a)
DisEqMore :: DisEq (S a) Z
DisEqInduct :: DisEq a b -> DisEq (S a) (S b)

data ListGADTDisEq a n where
Now, since the size type inside a `ListGADTDisEq` can't be one more than itself, it's finite, and we might not be able to form `ones`. Sadly, that's not true:
```data WrapListDisEq a = forall n . WrapListDisEq (ListGADTDisEq a n)