Re: [Caml-list] simple typing question

[Pierre Weis <pierre.weis@inria.fr>]

[...]
> I *almost* understand.  I understand the need for restrictions with
> polymorphic references.  The stated rule is that for
> 
>   let name = expr1 ...
> 
>   The type of expr1 is generalized when expr1 is a function, an identifier
>   or a constant. Otherwise the identifier name is not polymorphic (type
>   variables are not generalized).
> 
> And later it's stated that when expr1 is "map (function x -> x)" it's an
> application, so it isn't generalized.  However, it's an application that
> evaluates to a function, so it seems like it would meet the stated
> criteria.

No, it does not meet the criterium, since this criterium is ``expr1 is
a function, an identifier, or a constant'', which is evidently
syntactical in nature. Note that the words are ``expr1 is'', not
``expr1 seems to be'', ``expr1 could be considered as'', ``expr1 has a
type that is'', or whatever; hence, the criterium is NOT ``when expr1
EVALUATES to a function, an identifier, or a constant''; it could not
be since this modified rule would have no meaning at all (just
consider that no Caml expression can evaluate to an identifier, and
that all Caml expressions evaluate to constants or functions!).

Furthermore, the FAQ explicitely states afterwards that
"map (function x -> x)" is not a function, but an application!

>  Also, I'm not sure why such a restrictive rule is needed.  If
> expr1 doesn't manipulate references, why can't it be generalized?  Sorry to
> belabor this.

You are perfectly right. This rule is not needed.

More generally, you may find a lot of cases where an expression is not
generalized when it could be: you just discovered that the Caml type
system has some limitations. Hence, it is an interesting research
topic to overcome these limitations. In particular, we would be very
interesting at learning a more lenient typing discipline for
references (and more generally mutable values), if you could find a
new one that avoids the need for the drastic restriction we are now
using. It is an interesting (but extremely difficult) subject to look
at.

For a deeper discussion about the necessity for a special rule for let
in presence of mutable values, see for instance:

http://pauillac.inria.fr/~xleroy/publi/polymorphic-assignment.dvi.gz

The paper is rather old and the proposed solution has been abandoned,
but the examples given there, and the discussion about polymorphic
typing of mutable values are still inspiring, I think.

Best regards,

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis/


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners