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

[apfelmus]

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 
principle reads

   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