Re: [Caml-list] simple typing question

[Xavier Leroy <xavier.leroy@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 doesn't.  There is a major difference between a literal
function "fun x -> ..." and an expression that evaluates to a
function.  The latter can create and hide polymorphic references, as
shown below.

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

Because very similar expressions do manipulate references.  In
particular, consider that a (polymorphic) function can "hide" a
(polymorphic) reference.  For instance:

# let make_toggle () =
    let r = ref [] in fun x -> let old = !r in r := x; old
val make_toggle : unit -> 'a -> 'a list = <fun>

The result of make_toggle() is a function with type _a list -> _a list
that returns the argument that it received the last time it was called.

# let f = make_toggle();;
val f : '_a list -> '_a list = <fun>

# f [1;2;3];;
- : int list = []
# f [4;5;6];;
- : int list = [1; 2; 3]

Now, consider what happens if we were to generalize '_a in the type of f:

# let f = make_toggle();;
val f : 'a list -> 'a list = <fun>

# f [1;2;3];;
- : int list = []
# f ["hello"; "world"];;
- : string list = [1; 2; 3]    <--- crash! (wrong value for the type)

The gist of this example is that "make_toggle()" looks a lot like
"List.map (fun x -> x)" :  both are function applications that return
a function from '_a list to '_a list.  Yet, one is safe to generalize
and not the other.

No reasonably simple type system can distinguish both examples.  Many
have been proposed -- this was a hot research topic in the 1980-1993
time frame, and I even did my PhD on this very topic -- but none was
found to be really usable in practice.  The value restriction on
polymorphism (i.e. what Caml implements) is far from perfect, but is
the "least bad" of the known solutions.

- Xavier Leroy

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