[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
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
More information about the Haskell-Cafe
mailing list