[Haskell-cafe] Safe lists with GADT's

[Stefan O'Rear]

On Mon, Feb 26, 2007 at 03:42:56PM +1000, Matthew Brecknell wrote:
> 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).
> 
I can't find it now, but there was a post saying this couldn't be done
because system fc is strict in type arguments, such as bound by forall t.