[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


   Ralf Hinze. Fun with Phantom Types.

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


More information about the Haskell-Cafe mailing list