Feb 7, 2024, 10:54 AM ETLecture, Tutorial

Inferring Locality in OCaml | OCaml Unboxed

Jane Street

Watch on YouTube →

The OCaml compiler employs inference to determine whether local variables and parameters should be treated as "global" or "local," resolving ambiguities that arise when values do not explicitly escape or are not annotated.
Inferred local parameters are preferred because "local" is a supertype of "global," allowing a function accepting local arguments to also accept global ones, thereby maximizing permissiveness.
Inferred return values generally default to "global" to avoid imposing escaping constraints on the caller, which would otherwise prevent usage in contexts requiring global values (e.g., standard library I/O).
The compiler uses an internal alloc mode (e.g., mode var, global, local) which can be inspected via the -dtypedtree flag to debug type inference decisions, though this output is intended for compiler debugging rather than routine use.
When no signature (.mli file) exists for a module, the compiler performs a defaulting step that removes all local underscores from inferred types to prevent strange behaviors in projects lacking explicit signatures.
Inference allows a function with an inferred local return type to be assigned to a variable expecting a global return type, but not vice versa; adding a local requirement to a return type imposes stricter constraints on the caller that the implementation cannot retroactively satisfy.
Integers (int) represent a significant exception to the locality system because they are "immediates" (stored without pointers) and can "mode cross," meaning a local int can be safely treated as a global value even if stored in a reference or passed to a function.
To utilize the "mode crossing" feature for integers, an explicit type annotation is required; relying solely on inference to deduce that a value is an int is currently insufficient to trigger the safety check.
The community is developing improvements to provide finer-grained control over what types can "mode cross," potentially allowing safety constraints on non-pointer types beyond just int.
Function types can be converted if the conversion adds requirements on the caller (e.g., a global return value can be treated as local if the caller promises not to let it escape) but cannot remove requirements from the implementation (e.g., a function must explicitly promise not to let a parameter escape before being used in a context requiring that promise).
Workarounds such as function expansion (e.g., fun x -> h x) are sometimes necessary to bypass rejection of type conversions where the implementation implicitly satisfies a requirement that the type signature explicitly demands.
The "local" allocation discipline was introduced at Jane Street to enable stack-based allocation for certain data, reducing heap usage and garbage collection overhead compared to the default heap allocation.
Current standard library functions often lack awareness of the local mode, frequently forcing values to be treated as global during operations, which complicates demonstration and usage of locality in everyday code.
Explicit local annotations are not required for variables that do not escape, as the compiler's inference engine generally defaults to the most efficient local allocation when possible.