OCaml Locals, Modes, and Submoding

In the previous videos we looked at local parameters, then local variables and return values. This time I want to step back from writing functions and look at the theory that helps us understand how locals and globals interact. Local and global are called modes.

A mode is somewhat like a type, although there are differences. Every OCaml expression has a type: 5 has type int, while a larger expression might have type string list option. Every variable also has a type because it stands for an expression, which is evaluated to a value before it is stored. Similarly, every expression and every variable has a mode.

For example, in `let local_ x = "hello"`, the annotation forces x into local mode, and the expression `"hello"` is local too. The code compiles. I can suppress the unused-variable warning while experimenting.

If I introduce y, there is no corresponding annotation I can put on that variable to say that I want it to be global. Instead, I can define `mark_global : 'a -> unit` to ignore its argument. Its parameter is not marked local, so calling `mark_global y` forces y to be global through inference.

If I then write `let y = x` and pass y to `mark_global`, the compiler reports that the value escapes its region. The use of y requires a global value, while the locally declared x flows into it. Local values cannot escape, and allowing one to flow into a global value would give it a way to escape indirectly.

The actual program happens to be safe: `mark_global` simply ignores its argument. But its type does not promise that it will not store the argument somewhere. The compiler relies on the function's type, so it must reject the call even though the binding itself is not at the end of the region.

Now suppose y is global and I write `let local_ z = y`. This compiles. The `mark_global y` call can be farther down in the program and still determine y's mode, just as a distant use can affect inferred types. A global annotation would be convenient for this demonstration, although we generally do not need one.

Why can a global y flow into local z? Global is a submode of local, written `global < local`. As with assigning a subtype to a supertype, a global expression can be used in a local context. Local says the value does not escape; treating a global value locally says this use of it will not escape, which is safe.

The reverse does not work. Think of global as having the capability to escape. We may voluntarily give up a capability when we use a global value locally, but turning a local value into a global one would invent a capability it did not have. I find the ordering a little counterintuitive because global sounds bigger than local, yet we write global less than local.

Modes also interact with functions. I can define `mark_local : local_ 'a -> unit`, again with an implementation that ignores its argument. Calling it with the local x, the global y, or the local z all works. Passing y is fine because a global value can be used in a local context.

The local annotation on the parameter means that the parameter does not escape. It is a promise made by the function's implementation, not a requirement that callers provide a value originally declared local. A caller can pass either a local or a global value.

That promise limits the implementation: for example, storing the parameter in a reference is rejected as an escape. Even if I immediately ignore the reference, the escape analysis is not clever enough to accept this case. It may therefore make sense to mark parameters local wherever possible; I will discuss locality inference in a later video.

This is a difference from an ordinary type annotation on a function, which describes both the implementation and a requirement at use sites. Because of submoding, a local parameter imposes no meaningful restriction on whether the caller's value was global or local. My `mark_local` example is essentially just `ignore`.

There is another detail about modes and function types. Each side of an arrow can be local or global, giving four arrow types: `string -> string`, `local_ string -> string`, `string -> local_ string`, and `local_ string -> local_ string`. The case with a local input and a global output requires more care in its implementation.

These are four different types, with no subtyping relationship between them, although OCaml can perform some conversions in certain situations. To show the distinction, I put a function in a reference whose declared contents have type `string -> string`. A reference to the matching function works, but references to the other function types produce errors. The reference prevents conversions that the compiler might otherwise apply.

The key ideas are that modes describe every expression and variable, and that submoding lets any global value be treated as local, but not the other way around. We can annotate the input and output modes of a function arrow.

It is useful to remember that `local_ string` is not an independent type. The `local_` annotation is really describing the arrow. In a theoretical notation we might instead use four different arrow symbols; the concrete syntax places the word `local_` beside the input or output. I will return to these topics in a future video.