### Type (Dis)equality

Type equality is the essential ingredient in guarded algebraic datatypes:

data Z ; data S n ; data ListGADT a n where NilListGADT :: ListGADT a Zero 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 onesHere, 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 NilListGADTDisEq :: ListGADTDisEq a Zero ConsListGADTDisEq :: a -> ListGADTDisEq a n -> (TypeDisEq n (S n)) -> ListGADTDisEq a (S n)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) cons' :: a -> WrapListDisEq a -> WrapListDisEq a cons' x (WrapListDisEq NilListGADTDisEq) = WrapListDisEq (ConsListGADTDisEq x Nil DisEqBase) cons' x (WrapListDisEq p@(Cons q r s)) = WrapListDisEq (ConsListGADTDisEq x p (DisEqInduct s)) ones' = cons' 1 ones'

## No comments:

Post a Comment