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
