>> 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? _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
