Infinite types

[Jeffrey A. 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