OCaml's let polymorphism implementation

Question

I'm confused about let polymorphism in OCaml.

Consider the following code:

A: 
let f = (fun v -> v) in
((f 3), (f true))

B:
let f = (fun v -> v) in
((fun g ->
    let f = g in
    f) f)

C:
let f = (fun v -> v) in
((fun g ->
    let f = g in
    ((f 3), (f true))) f)

For A and B, there is no problem. But for C, OCaml reports error:

Error: This expression has type bool but an expression was expected of type
         int

So for A, when evaluating ((f 3), (f true)), f's type is 'a -> 'a, for B, when evaluating let f = g in f, f's type is 'a -> 'a. But for C, when evaluating ((f 3), (f true)), f's type is int -> int.

Why C's f doesn't have type 'a -> 'a?

I have difficulty in understanding the implementation of OCaml's let polymorphism, I'll appreciate it a lot if anyone can give a concise description of it with respect to the question.

Answer 1

Your code is unnecessarily confusing because you're using the same name f for two different things in B and also two different things in C.

Inside C you have this function:

fun g -> let f = g in (f 3, f true)

Again this is unnecessarily complicated; it's the same as:

fun g -> (g 3, g true)

The reason this isn't allowed is that it only works if g is a polymorphic function. This requires rank 2 polymorphism, i.e., it requires the ability to define function parameters that are polymorphic.

I'm not exactly sure what you're trying to do, but you can have a record type whose field is a polymorphic function. You can then use this record type to define something like your function:

# type r = { f : 'a . 'a -> 'a };;
type r = { f : 'a. 'a -> 'a; }
# (fun { f = g } -> (g 3, g true)) { f = fun x -> x };;
- : int * bool = (3, true)

# let myfun { f = g } = (g 3, g true);;
val myfun : r -> int * bool = <fun>

# myfun { f = fun x -> x };;
- : int * bool = (3, true)

The downside is that you need to pack and unpack your polymorphic function.

As a side comment, your example doesn't seem very compelling, because the number of functions of type 'a -> 'a is quite limited.