Weak polymorphism

On the occasion, the type inferred by OCaml contains polymorphic variables that read '_weak1, '_weak2, etc. The goal of this lecture note is to sketch the reason why.

Polymorphic type variables, revisited

In Week 04, the chapter about Polymorphic types articulated how once a proof tree has been constructed to infer a type, the unconstrained type names are made polymorphic.

Interlude

Anton: How about we infer the type of fun x -> x in the empty type environment?

Alfrothul: It has been a while, but let’s get started, picking t0 as the name of the putative type:

. |- fun x -> x : t0

Anton: We have no other choice but applying the FUN rule, which means that t0 must denote a function type, let’s say t1 -> t2, picking t1 as the name of the domain and t2 as the name of the co-domain.

Pablito: Let me make a note of that: t0 = t1 -> t2.

Anton: Thanks. Now for applying the FUN rule:

    (x : t1), . |- x : t2
FUN ---------------------
    . |- fun x -> x : t0

Alfrothul: We have no other choice but applying the LOOKUP_FOUND rule, which means that t1 and t2 must be the same.

Pablito: Let me make a note of that: t1 = t2.

Alfrothul: Thanks. Now for applying the LOOKUP_FOUND rule:

LOOKUP_FOUND ---------------------
             (x : t1), . |- x : t2
         FUN ---------------------
             . |- fun x -> x : t0

Anton: Our tree is now complete.

Pablito: So let’s look at the constraints we gathered on the way:

t0 = t1 -> t2

t1 = t2

Alfrothul: Well, solving these constraints, the type we were looking for, i.e., t0, is t1 -> t1.

Loki: Or t2 -> t2.

Anton: True. But either way, t1 – or t2, as you suggest – is unconstrained, so it is generalized into a type variable and the type of fun x -> x is 'a -> 'a.

Pablito: OCaml concurs:

# fun x -> x;;
- : 'a -> 'a = <fun>
#

Weakly polymorphic type variables

On some occasions, OCaml doesn’t know enough yet to infer the monomorphic type of a function, and it signals that by using a “weak type variable” in a type until it knows for sure. For example:

# let foo x y = x + 1;;
val foo : int -> 'a -> int = <fun>
# let x1 = foo 1;;
val x1 : '_weak2 -> int = <fun>
# let x2 = foo 2;;
val x2 : '_weak2 -> int = <fun>
#

The first time this second argument is supplied, this type becomes known, and is memoized in the type, which goes from “weakly polymorphic” to monomorphic:

# x1 "hello";;
- : int = 2
# x1;;
- : string -> int = <fun>
#

The type of the other instance of foo, however, is still unresolved:

# x2;;
- : '_weak2 -> int = <fun>
#

Let us apply this other instance to a value of another type:

# x2 true;;
- : int = 3
# x2;;
- : bool -> int = <fun>
#

Henceforth the type of each instance of foo is monomorphic.

Version

Created [18 Sep 2022]