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?