[Haskell-cafe] Re: Type-Marking finite/infinte lists?
apfelmus
apfelmus at quantentunnel.de
Sun Sep 16 03:46:57 EDT 2007
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
More information about the Haskell-Cafe
mailing list