Anatoly Yakovenko aeyakovenko at gmail.com
Sat Sep 20 13:12:51 EDT 2008

```>> 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.
>
> Your problem in this example is that the t in "MaxList t" is universally
> quantified when it needs to be existentially quantified. The following
> definition encodes the existential quantification as a rank-2 type:
>
> mlTail :: MaxList n -> (forall t. MaxList t -> a) -> a
> mlTail (ML1Cons1 h t) f = f t
> mlTail (ML1Cons2 h t) f = f t
> mlTail (ML2Cons1 h t) f = f t
> mlTail (ML2Cons2 h t) f = f t
>
> It works with the rest of your code unmodified.

how do i define (forall t. MaxList t -> a)?  It seems like i just
pushed the problem somewhere else.

>> 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?
>
> This example here suggests that you are happy merely with a (not necessarily
> tight) upper bound on the list elements. The following code solves your problem
> in this case, using only type unification and not fundeps or TFs:
>
> data Nat a where
>    Z :: Nat a
>    S :: Nat a -> Nat (S a)
>
> data Z
> data S a
>
> n00 = Z
> n01 = S n00
> n02 = S n01
> n03 = S n02
> n04 = S n03
>
> data MaxList t where
>   Nil :: MaxList a
>   Cons :: Nat a -> MaxList a -> MaxList a
>
> a = Cons n02 \$ Cons n02 \$ Cons n01 \$ Nil
> --- ":t a" gives "forall a. MaxList (S (S a))" which tells you exactly
> --- what you want: elements are at least 2.
>
> mlTail :: forall t. MaxList t -> MaxList t
> mlTail (Cons h t) = t
> --- unfortunately, you lose information here if the first
> --- element is larger than the rest.

Thanks, that's really cool.  Is there a way to keep  a tight upper
bound on the list using this method?
```