Hi, 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. For example, it is known that a list produced by repeat or cycle is always infinte, that foldl can’t handle infinte lists (while foldr might). length should never be called on an infinte list, and map’s output is infinite iff the input list is. So the compiler might use this information to emit errors like “line 42: program will not terminate: length applied to infinite list” or warnings “line 23: termination not guaranteed: foldl applied to possible infinte list”. I guess you can’t know it for all lists (halting problem...), but for those where it is possible, it would be nice to tell. Or am I missing something? Can this be implemented using some guru type system hacking? Greetings, Joachim -- Joachim "nomeata" Breitner mail: mail@joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C JID: joachimbreitner@amessage.de | http://www.joachim-breitner.de/ Debian Developer: nomeata@debian.org
On 9/15/07, Joachim Breitner
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
This is possibly non-optimal, since emptiness and finiteness are
semi-related. Specifically:
emptyIsFinite :: List Empty f a -> List Empty Finite a
infiniteIsNonempty :: List e Infinite a -> List Nonempty Infinite a
You can test whether a list is (non)empty, but not whether it's (in)finite.
nonEmpty :: List e f a -> Maybe (List Nonempty f a)
Aside from unfoldr, most operations that create lists are explicit
about whether the result is finite.
Then you can mark the properties of the common operations.
nil :: List Empty Finite a
cons :: a -> List e f a -> List Nonempty f a
repeat :: a -> List Nonempty Infinite a
tail :: List Nonempty f a -> List Unknown f a
last :: List Nonempty Finite a -> a
map :: (a -> b) -> List e f a -> List e f b
filter :: (a -> Bool) -> List e f a -> List Unknown f a
foldl :: (a -> b -> b) -> b -> List e Finite a -> b
length :: List e Finite a -> Int
unfoldr :: (a -> Maybe (b,a)) -> a -> List Unknown Unknown b
Note the type of "infiniteIsNonempty . tail".
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
The most general form of (++) would require either fundeps or type families:
(++) :: List e1 f1 a -> List e2 f2 a -> List (BothEmpty e1 e2)
(BothFinite f1 f2) a
type instance BothEmpty Empty Empty = Empty
type instance BothEmpty Empty Unknown = Unknown
type instance BothEmpty Empty Nonempty = Nonempty
type instance BothEmpty Nonempty Unknown = Nonempty
etc.
--
Dave Menendez
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
On 9/16/07, apfelmus
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
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?): 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. Probably, type classes can be exploited to the same aim. Regards, Zun.
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
On 9/17/07, Roberto Zunino
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...
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
On Sat, 15 Sep 2007, 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.
Thanks for asking this. I had the same question recently. :-) I think we should put the answers to the Wiki, Category:FAQ. (Is '2 times' frequent?)
participants (7)
-
apfelmus -
Bas van Dijk -
Dan Piponi -
David Menendez -
Henning Thielemann -
Joachim Breitner -
Roberto Zunino