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

Ken Shan wrote:

I think the rule you're looking for is the following: Don't equate a type variable with something that contains that type variable. This is known as the "occurs check". This rule prohibits "equi-recursive" types like "b" above, but not "iso-recursive" types like

data List a = Nil | Cons a (List a)

because the type "List a" is merely isomorphic to something containing "List a", but not equal to it.

Thanks, this is great. I understand (more or less) about equi- vs. iso-recursion from Pierce. The point (I assume) is that there is a natural distinction between the two cases, so that the restriction on infinite types (but not all recursive types) falls out fairly naturally from the Hindley-Milner analysis. (Thanks to everybody who responded.) Regards, Jeff Scofield Seattle

Jeremy Shaw wrote:

There is a thread on comp.lang.functional that talks about why haskell does not support recursive types:

http://groups.google.com/groups?q=ocaml+rectypes&hl=en&lr=lang_en&ie=UTF-8&oe=UTF-8&safe=off&selm=8giqpt%24oee%241%40rivesaltes.inria.fr&rnum=1

(searching for 'ocaml rectypes' on google groups turns up a number of useful threads about the joys and dangers of allowing recursive types).

I hadn't yet gotten around to wondering about the tradeoffs, but now that you mention it these are interesting references. Thanks. (Also, if I want to play around with the examples in Pierce, I can use ocaml -rectypes. Thanks for pointing this out.) Regards, Jeff Scofield