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