Weak Polymorphism in OCaml

Question

I am a little confused about weak polymorphism in OCaml.

Please see the following snippet, where I define a function remember:

let remember x =
   let cache = ref None in
      match !cache with
       | Some y -> y
       | None -> cache := Some x; x
;;

The compiler can infer the polymorphic type 'a -> 'a, and cache is used locally.

But when I modify the above code into

let remember =
   let cache = ref None in
    (fun x ->  match !cache with
         | Some y -> y
         | None -> cache := Some x; x)
;;

the compiler infers the weakly polymorphic type '_a -> '_a, also, it seems that cache is shared across invocations of remember.

Why does the compiler infer a weakly polymorphic type here and why is cache shared?

What is more, if I change the code again

let remember x =
   let cache = ref None in
    (fun z ->  match !cache with
         | Some y -> z
         | None -> cache := Some x; x)
;;

the compiler infers the polymorphic type 'a -> 'a -> 'a and cache becomes locally used. Why is this the case?

Outleap

Answer 1

let remember =
 let cache = ref None in
  (fun x ->  match !cache with
       | Some y -> y
       | None -> cache := Some x; x)
;;

Here cache is closed over by the returned function. But at the point where we declare cache, we have no information on what the type will be; it'll be determined by whatever the type of x is and cache is created when remember is defined.

But since this is a closure we can do something like this:

> remember 1
  1

Now it's clear that cache : int option ref since we've actually stored something in it. Since there's only ever one cache, remember can only ever store one type.

In the next one, you close over 2 things, x and cache. Since we create a new cache ref with each invocation of remember the type can be fully polymorphic again. The reason the type isn't weakly polymorphic is because we know that we're going to store x in it and we have xs type at the time when cache is created.

Greater

I guess that you meant that cache has type int option ref and not ref (None int). – Battlefield

Answer 2

This seems to do with value restriction. Full value restriction (as in SML) would reject your code altogether. Weakly polymorphic types are described in the paper "Relaxing the Value Restriction" by Jacques Garrigue, which I admittedly just stumbled upon after reading your question:

http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf

The fact that cache is shared across invocations should be obvious if you have a correct mental model of what ML code means. You are defining two values, remember and cache. Nesting simply makes the scope of cache private to the block.

Myology

Answer 3

let remember x =
   let cache = ref None in
      match !cache with
       | Some y -> y
       | None -> cache := Some x; x


let remember x =
   let cache = ref None in
    (fun z ->  match !cache with
         | Some y -> z
         | None -> cache := Some x; x)

In the above two versions, remember is a "direct" function, every time you call it like remember 1, it will initialise cache to ref None, isn't it? So actually, it does not remember anything, the cache is not shared between any remember calls.

---

In the other version:

let remember =
   let cache = ref None in
    (fun x ->  match !cache with
         | Some y -> y
         | None -> cache := Some x; x)

it is different. remember is still a function for sure, however, the real part that defines its content is (fun x -> match ...). It includes cache and cache is initialised once and will be only once. So cache is shared between the future remember call.

Chere

Your 'other version' just solves the code that kept me thinking most of yesterday's afternoon! – Jube