Re: Writing a counter function

On Sun, 30 Jun 2002, Jon Cast wrote:

Mark Carroll wrote:

...

On Sat, 29 Jun 2002, Samuel E. Moelius III wrote: (snip)

...

Here's another not-exactly-what-you-wanted solution. :) (snip)

...

Do any of the experimental extensions to Haskell allow a what-he-wanted solution? I couldn't arrange one in H98 without something having an infinitely-recursive type signature.

That's because the problem requires an infinitely-recursive type.

Consider Haskell:

self-apply f = f f

The *typing algorithm* (the thing that didn't complain in Lisp) proceeds roughly as follows:

f is applied to at least one argument, so f must have type a -> b. Therefore, f's argument (f) must have type a. So, we conclude:

f :: a -> b f :: a

But f can only have one type, so we set its types equal:

a = a -> b

This is clearly recursive, right?

...

so I'm wondering if it could be at all sane for Haskell to allow such stuff

Sure. All it has to do is:

1. Create its own newtype in response to such things as `self-apply' above.

2. Ensure that

self-apply f = f f

and

self-apply' g = g g

have the same type. I would *love* to hear ideas on how to do that, but it's difficult.

It isn't particularly hard to implement this. Haskell typecheckers use unification to match types up; the only difference is that a graph unification algorithm would be needed instead. Such algorithms exist --- the only real difference is you have to remember what you're unifying to avoid falling into a loop when unifying graphs with cycles. The idea of adding this to Haskell has been proposed several times, but never implemented. And the reason for THAT is that it would make type errors significantly harder to understand. Consider f x y = if x==0 then y else f (x-1) (where I "forgot" the second parameter in the recursive call). We expect this to be a type error, and indeed it is --- BECAUSE recursive types are not allowed. If they were, this definition would be well-typed, with the type f :: Num a => a -> b where b = b -> b You wouldn't get an error message unless you tried to CALL f, and perhaps not even then. For example, f 1 2 :: Num b => b where b = b -> b is well-typed! So you would probably eventually, somewhere else in the program, see an error message of the form ERROR - Illegal Haskell 98 class constraint in inferred type *** Type : Num b => b where b = b -> b This is enough to scare most people off the idea. Think of all the times you've seen the error message unification would give infinite type It's not the most common kind of type error, but it does happen regularly, at least to me. In every such case, the type error would be deferred in the way I describe. If I remember rightly, OCaml allows type recursion of this sort, but restricts it to object types precisely to avoid these problems. John Hughes