[Haskell-cafe] Re: Type-Marking finite/infinte lists?

[apfelmus]

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