[Haskell-cafe] Re: having fun with GADT's

[David Menendez]

On Sat, Sep 20, 2008 at 1:12 PM, Anatoly Yakovenko
<aeyakovenko at gmail.com> wrote:
>
>> 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.

Since MaxList is a GADT, you can always look inside to specialize the
parameter. In fact, with this particular definition, you just have to
look at the outermost constructor.

findMax :: MaxList n -> Either (MaxList One) (MaxList Two)
findMax l at Elem1 = Left l
findMax l at Elem2 = Right l
findMax l@(ML1Cons1 _ _) = Left l
findMax l@(ML1Cons2 _ _) = Right l
findMax l@(ML2Cons1 _ _) = Right l
findMax l@(ML2Cons2 _ _) = Right l

>> 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:
[...]
> Thanks, that's really cool.  Is there a way to keep  a tight upper
> bound on the list using this method?

One way is to use a witnesses to prove that the head of the list is
either the maximum element, or less than (or equal) to the maximum
element.


data MaxList n where
    Nil  :: MaxList Z
    ConsMax :: LE n a -> Nat a -> MaxList n -> MaxList a
    ConsLE  :: LE a n -> Nat a -> MaxList n -> MaxList n

cons :: Nat a -> MaxList b -> (forall n. MaxList n -> ans) -> ans
cons a as f = case cmp a (maximum as) of
    Left le -> f (ConsLE le a as)
    Right le -> f (ConsMax le a as)

mlTail :: MaxList a -> (forall b. MaxList b -> ans) -> ans
mlTail (ConsMax _ _ as) f = f as
mlTail (ConsLE _ _ as)  f = f as

There are at least three ways to define LE, which have different
trade-offs in terms of usability and space efficiency. One way is to
encode both numbers,

data LE a b where
    ZLE :: Nat b -> LE Z b
    SLE :: LE a b -> LE (S a) (S b)

cmp :: Nat a -> Nat b -> Either (LE a b) (LE b a)
cmp Z b = Left (ZLE b)
cmp a Z = Right (ZLE a)
cmp (S a) (S b) = either (Left . SLE) (Right . SLE) (cmp a b)

maximum :: MaxList n -> Nat n
maximum Nil = Z
maximum (ConsMax _ n _) = n
maximum (ConsLE le _ _) = greater le

greater :: LE a b -> Nat b
greater (ZLE b) = b
greater (SLE l) = S (greater l)

lesser :: LE a b -> Nat a
lesser (ZLE b) = Z
lesser (SLE l) = S (lesser l)


Alternatively, you can encode the difference between a and b,

data LE a b where
    Eq :: LE a a
    Lt :: LE a b -> LE a (S b)

cmp :: Nat a -> Nat b -> Either (LE a b) (LE b a)
cmp Z Z     = Left Eq
cmp Z (S b) = Left (Lt (zle b))
cmp (S a) Z = Right (Lt (zle a))
cmp (S a) (S b) = either (Left . sle) (Right . sle) (cmp a b)

zle :: Nat a -> LE Z a
zle Z = Eq
zle (S n) = Lt (zle n)

sle :: LE a b -> LE (S a) (S b)
sle Eq = Eq
sle (Lt l) = Lt (sle l)
-- Since only the types change, it should be safe to
-- replace sle with unsafeCoerce. In that case, the
-- final equation for cmp can just be
--    cmp (S a) (S b) = unsafeCoerce (cmp a b)

maximum :: MaxList n -> Nat n
maximum Nil = Z
maximum (ConsMax _ n _) = n
maximum (ConsLE le a _) = greater le a

greater :: LE a b -> Nat a -> Nat b
greater Eq     n = n
greater (Lt l) n = S (greater l n)

lesser :: LE a b -> Nat b -> Nat a
lesser Eq     n     = n
lesser (Lt l) (S n) = lesser l n

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>