On Sat, Sep 20, 2008 at 1:12 PM, Anatoly Yakovenko <aeyakovenko@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@Elem1 = Left l findMax l@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@zednenem.com> <http://www.eyrie.org/~zednenem/>