# [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,

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

```