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