[Haskell-cafe] Re: having fun with GADT's
Reiner Pope
reiner.pope at gmail.com
Sat Sep 20 09:34:01 EDT 2008
Anatoly Yakovenko <aeyakovenko <at> gmail.com> writes:
>
> 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.
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.
>
> 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.
Reiner
More information about the Haskell-Cafe
mailing list