Anatoly Yakovenko aeyakovenko at gmail.com
Sat Sep 20 05:46:53 EDT 2008

```I dont remember where i saw it, but i think someone had an example of
a list whose type is the maximum element in the list.  I've been
trying to reproduce that with GADT's.

data One = One
data Two = Two
data Three = Three

data MaxList t where
Elem1 :: MaxList One
Elem2 :: MaxList Two
ML1Cons1 :: MaxList One -> MaxList One -> MaxList One
ML1Cons2 :: MaxList One -> MaxList Two -> MaxList Two
ML2Cons1 :: MaxList Two -> MaxList One -> MaxList Two
ML2Cons2 :: MaxList Two -> MaxList Two -> MaxList Two

a = ML2Cons2 Elem2 \$ ML2Cons1 Elem2 \$ ML1Cons1 Elem1 \$ Elem1

so one problem is the tedium of defining a cons for each possible
combination.  The other problem is that i cant define a usefull tail
that makes any sense.

mlTail :: MaxList Two -> MaxList t
mlTail (ML2Cons2 a b) = b
mlTail (ML2Cons1 a b) = b

this one doesn't work, and probably because there is nothing that i
could do with the return value.

mlTail :: MaxList Two -> MaxList Two
mlTail (ML2Cons2 a b) = b
mlTail (ML2Cons1 a b) = b  --wont compile because b is a MaxList One

will only work for lists that only contain Two's, which is not what i
want either.  So is this somehow possible?

Thanks
```