How OCaml Infers Locality

Previously we explored local parameters, variables and return values, and the idea that local and global are modes. Now let us look at inference: how the OCaml compiler figures out the locality of values and functions.

Suppose I bind an unused x inside a function. The ordinary compiler output tells me that f has type unit to unit, but it does not tell me whether x is local or global. That distinction may become important as the program grows, even though it makes no difference in this tiny example.

For demonstration, I can pass -dtypedtree to print the compiler’s typed intermediate representation. This output is intended for compiler debugging, not everyday programming, and its format is not especially friendly. Beside x it shows an allocation mode of <modevar>: the compiler has introduced a mode variable because it does not yet know the answer.

If I return x, it escapes the function’s region, and the printed allocation mode becomes global. If instead I annotate x as local and prevent it from escaping, the output shows local. Without either constraint, the compiler makes a choice after type checking and prefers local for the allocation.

Locality provides safety properties, but the motivation for this work at Jane Street was also allocation: parts of an OCaml program can use a stack discipline rather than heap allocation that needs garbage collection. In that sense a local allocation can be preferable. I will discuss its allocation behavior further in a later video.

More generally, inference tries to be as permissive as possible. For a function parameter, local is more permissive: global is a submode of local, so a function accepting a local argument can also accept a global one. A function that ignores its argument is a simple example, although useful functions can do more.

The ordinary printed type of this function does not show a local parameter. To see what is happening, I put it in a module and give the module a signature. Both a plain parameter type and a local_ parameter type can match the same implementation.

A module signature is not used to type-check the structure itself. The compiler first infers the structure, then checks whether the result matches the signature. In this example it infers a local parameter for f, so the implementation can satisfy a signature that asks for one.

When there is no signature, as in a module without an mli file, a defaulting step removes the local_ markers from the displayed module type. This avoids surprising results in projects without interface files, although the implementation could potentially improve. The inferred implementation can still support a local argument.

The function need not merely ignore its argument. It can pass x to another function that promises not to let it escape, or manipulate it in other ways. Examples are awkward because much of the standard library does not yet support locals, and calls to those functions can force values to be global.

Why does a locally inferred parameter also match a signature without local_? A local parameter is a promise by the implementation that its argument does not escape. Module signature matching permits us to forget that promise: the inferred module type is compatible with the less demanding signature.

For return values the preference goes the other way. A global result is more useful because the caller may need it in a global context. If a function returns a local string, I cannot simply pass the result to a function that requires a global string; local values do not automatically become global.

Within Jane Street there is a globalize PPX that can convert a local value when a global one is needed, but it is not available in this example. A local annotation on a return value imposes a restriction on the caller: the caller must not let that result escape. Adding that restriction to a signature is safe.

For a parameter, local instead imposes a requirement on the function implementation. If h stores or otherwise lets its argument escape, its inferred parameter is global, and a signature requiring a local parameter fails. We may remove local from a parameter in a signature or add it to a result, but cannot generally do the reverse.

Integers are an important exception. Consider a function adding x to itself and then storing x in a reference. A local x would ordinarily be rejected because it escapes, but when x is explicitly annotated as int, the same code is accepted.

An OCaml int is an immediate value: it is represented without a pointer. Locals were designed around allocation behavior, so an immediate does not need the same pointer-lifetime discipline. We say an int can mode-cross: even a local int may be used where a global value is required, or equivalently, ints can always be treated as global.

The type annotation matters here. If the compiler learns that x is an int only through inference from addition, the mode-crossing example is not accepted. Making information flow across the expression in that way could make typing fragile, so the programmer must state somewhere that x is an int.

This is why I have used strings in the earlier examples: strings do not mode-cross. It also explains why a local int can be passed to addition even though the standard library does not generally know about locals. The int crosses modes at the call.

That leaves an awkward limitation: if I want local’s extra safety properties for an int, mode crossing prevents me from getting them. We are working on finer-grained control over which values may mode-cross. Pointer-represented values would not be safe to cross this way, but even for immediate values one might want a restriction.

Inference also permits some conversions between functions with different localities. If f returns a global string, I can use it where a function returning a local string is expected: the latter merely adds a restriction on what the caller may do with the result.

The reverse kind of promise is different. I cannot take a function that accepts a global parameter and claim after the fact that it accepts a local one: that would add a requirement on the implementation that it has not promised to meet.

Curiously, the demonstration also rejects assigning a function with a local parameter to a plain function type, even though forgetting that promise is safe. This is a limitation that may be fixed by the time you watch. An eta expansion—writing fun x -> h x instead of h—works around this particular rejection.

Eta expansion does not make the unsafe conversion work. If f never promised to accept a local argument, wrapping it in another function cannot create that promise. Some conversions between function types with different localities are safe and supported, but not all are safe.

The useful consequence is that you generally do not have to write local annotations on every term or variable. Like ordinary type inference, locality inference usually works out the necessary modes, subject to the caveats we have explored.