[Haskell-cafe] Re: Type-Marking finite/infinte lists?
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
Re: [Haskell-cafe] Re: Type-Marking finite/infinte lists?
On 9/18/07, apfelmus [EMAIL PROTECTED] wrote: ...in reality, foldr is (almost) the induction principle for natural numbers! Oh yes, nice observation! Afpelmus, thanks for your thorough answers! regards, Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Type-Marking finite/infinte lists?
Roberto Zunino wrote: apfelmus wrote: cons:: a - List e f a - List Nonempty f a But unfortunately, finiteness is a special property that the type system cannot guarantee. The above type signature for cons doesn't work since the following would type check bad :: a - List Nonempty Finite a bad x = let xs = cons x xs in xs In other words, Haskell's type system doesn't detect infinite recursion. I thought this was possible with GADTs (is it?): Interesting, it probably is. See below. data Z data S n data List a len where Nil :: List a Z Cons:: a - List a len - List a (S len) Then, bad (adapted from above) does not typecheck. Note that you're doing more than forcing your lists to be finite, you force them to be of a particular size. For instance, a list of type List a (S (S (S Z))) is guaranteed to have exactly 3 elements. That's why bad x = let xs = cons x xs in xs doesn't type check: the lhs has one more element than the rhs. As soon as you try to hide the finiteness proof (= count of elements in the list) away via existential quantification data ListFinite a where IsFinite :: List a len - ListFinite a the bad function reappears and type checks cons :: a - ListFinite a - ListFinite a cons x (IsFinite xs) = IsFinite (Cons x xs) bad :: a - ListFinite a bad x = let xs = cons x xs in xs But there is a major difference now: bad is not an infinite list, it's _|_. That's because cons is now strict in the second argument, i.e. it really does check whether the second argument matches the constructor IsFinite which means that there's a proof that xs is finite. That's good news, it seems to be that everything of type ListFinite is finite modulo _|_s. I don't have a proof, though. Of course, we can have a _|_ in every position, like cons 1 (cons 2 (IsFinite undefined)) which corresponds to 1 : 2 : _|_ Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-Marking finite/infinte lists?
On 9/17/07, Roberto Zunino [EMAIL PROTECTED] wrote: I thought this was possible with GADTs (is it?): data Z data S n data List a len where Nil :: List a Z Cons:: a - List a len - List a (S len) Slightly related: 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? 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. regards, Bas P.S. I also asked this on #haskell but I had to go away; Maybe I missed the answer... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Type-Marking finite/infinte lists?
David Menendez wrote: Joachim Breitner wrote: today while mowing the lawn, I thought how to statically prevent some problems with infinte lists. I was wondering if it is possible to somehow mark a list as one of finite/infinite/unknown and to mark list-processing functions as whether they can handle infinte lists. One possibility would be to have some phantom markers in the list type. For example, newtype List isEmpty isFinite a = MarkList [a] data Finite data Infinite data Empty data Nonempty data Unknown Yes, phantom types are what Joachim wants. For more about phantom types, see also http://haskell.org/haskellwiki/Phantom_type Ralf Hinze. Fun with Phantom Types. http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf Another possibility for working with infinite lists would be a new data type data InfList a = a : InfList a (also called Stream but this name is quite overloaded.) cons:: a - List e f a - List Nonempty f a But unfortunately, finiteness is a special property that the type system cannot guarantee. The above type signature for cons doesn't work since the following would type check bad :: a - List Nonempty Finite a bad x = let xs = cons x xs in xs In other words, Haskell's type system doesn't detect infinite recursion. (But there are type systems like System F or that of Epigram that disallow general recursion.) As a variation, we can use rank-2 types instead of Unknown; e.g. tail :: List Nonempty f a - (forall e. List e f a - w) - w filter :: (a - Bool) - List e f a - (forall e. List e f a - w) - w That's probably best explained in terms of the existential quantor tail :: List Nonempty f a - (exists e. List e f a) filter :: (a - Bool) - List e f a - (exists e. List e f a) In other words, tail takes a nonempty list and returns one that has an emptiness e but that's all we know. Existential quantification is not first-class in Haskell, so you can either use a data type data Box100 f b c = forall a . Box100 (f a b c) tail :: List Nonempty f a - Box100 List f a or encode it via the isomorphism exists e . expr e = forall w . (forall e . expr e - w) - w Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-Marking finite/infinte lists?
On 9/16/07, apfelmus [EMAIL PROTECTED] wrote: But unfortunately, finiteness is a special property that the type system cannot guarantee. The above type signature for cons doesn't work since the following would type check bad :: a - List Nonempty Finite a bad x = let xs = cons x xs in xs In other words, Haskell's type system doesn't detect infinite recursion. Exactly. Haskell allows free unrestrained recursion, and this is the source of the problem. Instead we could limit ourselves to structural recursion and then we can guarantee that even if we write recursive code, the results will always be finite. For details there's Turner's paper on Total Functional Programming: http://www.cs.mdx.ac.uk/staffpages/dat/sblp1.pdf -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
