Infinite types
Jeffrey A. Scofield
jeff at dhitechnologies.com
Mon Dec 8 12:42:46 EST 2003
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
More information about the Haskell-Cafe
mailing list