Infinite types

[Jeffrey A. Scofield]

camarao at dcc.ufmg.br wrote:

> > Say I have the following function, ... :
> >
> >     f n () = (n, f (n + 1))
> > ...
> > I have two questions:
> >
> > 1.  How can I tell from the Haskell 98 Revised Report that this
> >     function isn't allowed?  The discussions of typing in the Report
> >     generally defer to the ``standard Hindley-Milner analysis.''
> 
> In your example, if we assume that "f" has type, say, "a->()->(a,b)", for
> some "a","b", then it is used, in its own definition, with type
> "a->b".

This is true, but things typecheck OK as long as

    b = () -> (a, b)

This is the so-called infinite type that I'm asking about.

(You can get the above definition of f to typecheck and work as
expected in Ocaml if you use the -rectypes flag mentioned in another
message.  So there's nothing inherently absurd about the definition
of f.  (Also, I just transcribed it from Pierce!))

> In the Hindley-Damas/Milner type system, there is no "polymorphic
> recursion": a variable being defined may not be used polymorphically
> inside its own definition. In other words, for typing its own definition, a
> variable is assumed to have a simple (non-quantified) type.
>
> Even in the Milner-Mycroft type system, where we have polymorphic
> recursion (a variable may be used polymorphically in its own definition),
> this expression could not be typed, because (informally speaking) a
> polymorphic type may only be instantiated, and "a->b" is not (cannot
> be) an instance of "a->()->(a,b)", for any "a","b".

As long as you allow infinite types, there is no polymorphic recursion
(as I understand it).

I'm definitely not arguing that these types should be allowed
in Haskell.  I'm wondering how to tell, as a relative newcomer to
Haskell, that they aren't allowed.  Possibly the answer is that
these types are not allowed by the standard Hindley-Milner analysis
and that I just need to read the papers cited in the Haskell Report.
I was hoping to avoid this because reading such papers is very hard!

I guess I'm also pointing out that I (as a newcomer) can't easily
tell just from the Report that these types are forbidden in Haskell.
In other words, I can't easily tell which recursive types are OK and
which aren't.  For whatever this is worth.

(As I say, the restriction on type synonym declarations is very
suggestive, but it really doesn't seem to apply to all types in a
module, just to type synonyms.)

Regards,

Jeff Scofield