Writing a counter function

[John Hughes]

On Sun, 30 Jun 2002, Jon Cast wrote:

>
> Mark Carroll <mark@chaos.x-philes.com> 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