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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
