camarao@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