Neil Mitchell wrote:
data ConsT a data NilT
data List a t where Cons :: a -> List a b -> List a (ConsT b) Nil :: List a NilT
Stefan O'Rear wrote:
data VarList a = forall t. VarList (List a t)
fromListV :: [a] -> VarList a fromListV [] = VarList Nil fromListV (x:xs) = case fromListV xs of VarList xs' -> VarList (Cons x xs')
fromListC :: [a] -> (forall t. List a t -> r) -> r fromListC [] fn = fn Nil fromListC (x:xs) fn = fromListC xs (\sl -> fn (Cons x sl))
I noticed that fromListV and fromListC always force traversal of the input list. I made various attempts to modify them to preserve laziness, but this always resulted in a type error. For example:
fromListV (x:xs) = case fromListV xs of ~(VarList l) -> VarList (Cons x l)
Couldn't match the rigid variable `a' against the rigid variable `a1' `a' is bound by the type signature for `fromListV' `a1' is bound by the pattern for `VarList' at gadt-list.hs:33:42-50 Expected type: List a b Inferred type: List a1 t In the second argument of `Cons', namely `l' In the first argument of `VarList', namely `(Cons x l)' I guess the strict traversal of the input list is inevitable, considering that the concrete type of any (List a t) depends on the length of the list (even when hidden behind an existential).