[Haskell-cafe] There's nothing wrong with infinite types!

[ajb at spamcop.net]

G'day all.

Quoting Stefan O'Rear <stefanor at cox.net>:

> I for one took that as a challenge, and have implemented a type
> inference engine for infinite types.

Very nice!  But there's plenty wrong with infinite types...

The fact is that infinite types are almost never what you want.
In the few situations where it is (usually in data structures), using
"newtype" usually isn't a huge imposition.

What you end up with instead is a bunch of programs that are obviously
wrong becoming well-typed.  Consider the following program:

  search p [] = error "not found"
  search p (x:xs)
    | p x       = x
    | otherwise = search p xs

Let's mutate the "otherwise" case with some common and some not-so-common
bugs:

  search p [] = error "not found"
  search p (x:xs)
    | p x       = x
    | otherwise = xs

  search p [] = error "not found"
  search p (x:xs)
    | p x = x
    | otherwise = search p

  search p [] = error "not found"
  search p (x:xs)
    | p x = x
    | otherwise = search xs

  search p [] = error "not found"
  search p (x:xs)
    | p x = x
    | otherwise = search

  search p [] = error "not found"
  search p (x:xs)
    | p x = x
    | otherwise = p

How many of these buggy versions would be type-correct if Haskell allowed
infinite types?

I'll wait while you go and check with your type checked.

...

Are you surprised?  I was.  Just about every dumb change I could think
of making to the "otherwise" case resulted in what would be a type-
correct function, if we allowed infinite types!

It wouldn't be so bad if it were unusual cases, but a lot of common
programmer mistakes (like leaving arguments off a recursive function
call) are only caught because of the occurs check.  Catching programmer
mistakes is one of the reasons why people like Haskell so much.  Given
that we have a servicable workaround (newtype), it would be a mistake to
allow types like this.

Cheers,
Andrew Bromage