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

[Joachim Breitner]

Hi,

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
something?

Can this be implemented using some guru type system hacking?


Greetings,
Joachim

-- 
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