# [Haskell-cafe] Re: Type-Marking finite/infinte lists?

apfelmus apfelmus at quantentunnel.de
Tue Sep 18 05:31:51 EDT 2007

```Bas van Dijk wrote:
> Roberto Zunino wrote:
>>
>> data Z
>> data S n
>> data List a len where
>>    Nil :: List a Z
>>    Cons:: a -> List a len -> List a (S len)
>>
>
> The other day I was playing with exactly this GADT. See: http://hpaste.org/2707
>
> My aim was to define a function like 'concat' in terms of 'foldr' but
> I was unable to do so. Can this be done?

Not with the standard foldr you mimic. I mean, in reality, foldr is
(almost) the induction principle for natural numbers! Given a property
p  that you want to prove for all natural numbers  n , the induction

induction :: forall p .
(forall n . p n -> p (S n)) -- induction step
-> p Z                         -- induction base
-> (forall n . p n)            -- it holds!

Similarly, the right type of foldr is

foldr :: forall b a .
-> (forall n . a -> b n -> b (S n))
-> b Z
-> (forall n . List a n -> b n)

or without the superfluous foralls

foldr :: (forall n . a -> b n -> b (S n)) -> b Z -> List a n -> b n

The implementation is exactly the same

foldr _ z Nil         = z
foldr f z (Cons x xs) = f x (foldr f z xs)

Put differently, you just add the length parameter to b.

For concat, we have to set

b n = List a (Sum n m)

Given only  List a (Sum n m), the Haskell type checker can't figure out
that it is of the form  b n  for some type constructor  b  . The
solution is to introduce a newtype to guide it

newtype PlusList a m n = In { out :: List a (Sum n m) }

so that we now have b = (PlusList a m) and we can write

concat :: forall a m n . List a n -> List a m -> List a (Sum n m)
concat xs ys = out (foldr f z xs)
where
f :: a -> PlusList a m n -> PlusList a m (S n)
f x b = In (cons x (out b))
z :: PlusList a m Z
z = In ys

I didn't test this code, but it should work ;)

> Also I was unable to define the function 'fromList :: [a] -> ListN a
> n'. This makes sense of course because statically the size of the list
> is unknown. However maybe existential quantification can help but I'm
> not sure how.

The return type of  fromList  can't be

fromList :: [a] -> List a n

since that's syntactic sugar for

fromList :: forall n . [a] -> List a n

i.e. given a list, fromList  returns one that has all possible lengths
n. Rather, the type should be

fromList :: [a] -> (exists n . List a n)

i.e. there exists a length which the returned list has. (Exercise: why
is  (exists n . [a] -> List a n)  wrong?)

The data type  ListFinite  from my other message on this thread does the
existential quantification you want. With

nil  :: ListFinite a
nil  = IsFinite (Nil)

cons :: a -> ListFinite a -> ListFinite a
cons x (IsFinite xs) = IsFinite (Cons x xs)

we can write

fromList :: [a] -> ListFinite a
fromList []     = nil
fromList (x:xs) = cons x (fromList xs)

Regards,
apfelmus

```