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

Joachim Breitner mail at joachim-breitner.de
Sat Sep 15 12:15:56 EDT 2007


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.

For example, it is known that a list produced by repeat or cycle is
always infinte, that foldl can’t handle infinte lists (while foldr
might). length should never be called on an infinte list, and map’s
output is infinite iff the input list is.

So the compiler might use this information to emit errors like
“line 42: program will not terminate: length applied to infinite list”
or warnings
“line 23: termination not guaranteed: foldl applied to possible infinte list”.

I guess you can’t know it for all lists (halting problem...), but for
those where it is possible, it would be nice to tell. Or am I missing

Can this be implemented using some guru type system hacking?


Joachim "nomeata" Breitner
  mail: mail at joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C
  JID: joachimbreitner at amessage.de | http://www.joachim-breitner.de/
  Debian Developer: nomeata at debian.org

More information about the Haskell-Cafe mailing list