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

[Stefan O'Rear]

I'm sure anyone who's used Haskell for any significant length of time
has received this error message:

Occurs check: cannot construct the infinite type: t = t -> t1

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

Expr> s
(a -> b -> c) -> (a -> b) -> a -> c
Expr> skk
a -> a
Expr> s(skk)(skk)
(fix a . (a -> b))
Expr>

Points of interest:

* There are NO error conditions. it-unifier can assign a type to every
syntactically valid expression of combinatory logic.

* Typechecking is guaranteed to terminate in a linear number of steps,
an (apparently) stronger guarantee than that provided by DHM.

* (Mostly theoretical, since it-unify does not yet support sums or
products): Fixpoint types subsume declared recursive datatypes.
e.g: type List a = fix l . Either () (a,l)

darcs get http://members.cox.net/stefanor/fixtypes/

[a***@spamcop.net]

G'day all.

Post by Stefan O'Rear
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