If It Compiles, It’s Correct March 15, 2026

Caveat lector: I am very much a novice in these ideas, so it is quite possible that there’s a mistake in this post. If you detect an error, feel free to reach out! Corrections are much appreciated.

Here’s a fun puzzle: can you write a function taking two callbacks, whose type signature promises that the callbacks must only be called in alternating order? In this post, I’ll develop one solution, originally motivated by some code I was writing at work.

Something you’ll sometimes hear static typing evangelists say is that with a sufficiently expressive type system, code that compiles is usually correct. This is, of course, a rather suspicious claim, because writing correct code is famously quite difficult; it merits some further thought. What does this really mean? I suspect that many people who are not used to programming in strongly typed languages imagine that types are a way to force the callers of some interface to behave a certain way: for instance, a function like add : int -> int -> int cannot be passed a floating-point number; it must be passed an integer. The more specific the type of a function, the more restricted its callers are, and thus the more likely they are to be correct: there is much less room for error.

But dually, types also place useful restrictions on the possible implementations of such interfaces. In this case, it is more general types—especially polymorphic ones—that are the most restrictive, and therefore the most useful for enforcing correctness of compiling implementations. To give a very simple but hopefully illustrative example, think about how you would implement the signature id : 'a -> 'a.¹ Assuming no tricks in the implementation,² there’s really only one way you could possibly implement this function (up to extensional equivalence): you need to return the thing passed into the function. In that sense, it really is true that any total implementation of this function that compiles must be correct.³

It is worth pointing out that a concrete type on the function wouldn’t provide as strong of a guarantee on its behavior. For instance, consider the type mystery : int -> int. What does this function do? Even if we are promised that the implementation is total, it’s frankly very hard to know what it does from the outside; the returned value could be any integer! With a language like OCaml that allows for mutable state, the implementation could even stash a copy of the input somewhere for later use, which makes reasoning about such functions much more difficult.⁴

A parity puzzle

This is all fairly well-known at this point, but I bring this up because I recently came across a somewhat cute example of this at work, making use of new type system features introduced in the OxCaml extension to the OCaml language. In particular, OxCaml introduces uniqueness and affinity modes, which specify whether aliases to a particular value are allowed to exist anywhere else in the program. I would not describe myself as familiar with Rust, but I am told that this is similar to one of Rust’s language features; both are related to substructural type systems, and specifically to linear (or more properly, affine) types.⁵

The specific thing that prompted this thought was that I was writing a state machine that listens to a message bus (of Turn_on and Turn_off messages) and toggles its state between On and Off accordingly, invoking a callback whenever the state transitions.

One property of this state machine was that the only valid transitions were On to Off (via Turn_off) and Off to On (via Turn_on). In particular, a Turn_on message should have no effect if the state machine is already On, and likewise for the Turn_off message and the Off state.

Now it is hard to completely statically encode the correctness of this transition function in the type, but you could get a decent part of the way there if you had a way of guaranteeing that the argument with which the callback is invoked must alternate between On_to_off and Off_to_on. Is there a way to do this in the type system? Sounds tricky, but as it turns out, OxCaml modes are enough to let us do this!

The alternator function

The main idea is to parameterize the function over two witness types, which must be passed to the callback as proof that the function is currently in the appropriate state. (Or at least proof of the correct parity of callback invocations.) Since these witness types are polymorphic, the only way the state machine can fabricate these values (and hence invoke the callback) is to be given them by the caller. When coupled with the constraint that each witness can only be used once—via OxCaml modes—this is sufficient to guarantee that the callback is invoked with alternating states.

That’s all very abstract; let’s start by implementing a simpler version of what we want, which will hopefully very naturally lead to the full version. Let’s first consider the following easier problem: write the type signature of a function such that all implementations satisfy the following:

1. The function is provided two callbacks, on_even and on_odd.
2. The function calls on_even first.
3. The function alternates calls between on_even and on_odd.

Translating the ideas just mentioned above into code, we get something like this:

module Alternator = struct
  type ('even, 'odd) t =
    on_even:('even @ once unique -> 'odd @ once unique)
    -> on_odd:('odd @ once unique -> 'even @ once unique)
    -> 'even @ once unique
    -> unit
end

Notice that in order to invoke on_even, you need an 'even witness, which is immediately consumed by the call to on_even, because it is marked once. But the only place you can get such a witness is from calling on_odd with an 'odd witness, and vice versa! This guarantees the alternation of invocations; the initial 'even value allows you to start off by calling on_even. The type admits the following very cute implementation:

let rec alternator : 'even 'odd. ('even, 'odd) Alternator.t =
  fun ~on_even ~on_odd even ->
  alternator ~on_even:on_odd ~on_odd:on_even (on_even even)

Note the explicit polymorphism over 'even and 'odd; this is required to forbid the compiler from inferring the more specific type ('a, 'a) Alternator.t for the expression, if there were a bug in the implementation.⁶ If we wanted, we could hide this using a standard OCaml type trick—record fields are allowed to be explicitly polymorphic, so we can hide the universal quantification in there:

module Alternator' = struct
  type t = { f : 'even 'odd. ('even, 'odd) Alternator.t }
end

Of course, a caller need not define any special types to use for 'even and 'odd here; this is unlike a similar pattern in which you write actual abstract types Even.t and Odd.t while only exposing your own particular conversion functions. This alternation is encoded purely on the type level, and it is sufficient that the implementation type-checks; callers can use any type they like (such as unit) when actually calling the function.

Perhaps one thing to note: I’m still quite new to using OxCaml, so I’m actually not sure that this toy example requires the uniqueness mode at all; I suspect only affinity is strictly necessary. But holding unique references to affine values makes programming against them much easier, and is how I originally thought of this example, so I’ve kept the unique mode here.

Mutable references to unique values

The above basically gets us most of the way there, but if you actually tried to implement the previously-described state machine that way, you would quickly run into the problem that you’re not allowed to store mutable references to unique values in ordinary ref cells, meaning that you can’t directly include the parity proofs in your application state, making any nontrivial code difficult to write.

On the one hand, this makes sense—it’s very hard for the compiler to verify that a value is actually used uniquely, if an alias to it is stashed away somewhere.⁷ This is a typical pattern with fancy type-system features: you should expect them to make it much harder to write programs, because you’re trying to prove more complicated theorems (in the sense of the Curry–Howard correspondence between programs and proofs) to the compiler, which naturally have more complex proofs.⁸ The missing ingredient is some kind of reference cell that promises to provide unique access to its contents; getters should either require unique access to the cell or exchange its value with another, for instance.

Fortunately for us, it turns out that OxCaml provides such a thing, as part of the unique library. What we want is basically Unique.Ref, which, stripping away some type trickery not relevant to our example,⁹ has the following interface:

type 'a t
val make : 'a @ once unique -> 'a t @ unique
val get : 'a t @ unique -> 'a @ once unique
val set : 'a t -> 'a @ once unique -> unit
val exchange : 'a t @ local -> 'a @ once unique -> 'a @ once unique

How is this implemented, you might ask? If you dig into the library source code, you’ll notice that exchange has the following implementation…

let[@inline] exchange t a =
  let a' = get (Basement.Stdlib_shim.Obj.magic_unique t) in
  set t a;
  a'

But anyway, that’s not our concern. Armed with this primitive, it becomes feasible to implement the state machine described earlier, thus statically ruling out certain kinds of bugs in the implementation.

Obvious reflections

Now obviously, I did not actually ship the code above; I think the trade-off in understandability is not really worth it.¹⁰ But still, I thought it was an interesting idea, perhaps worth sharing more widely on this blog. (Plus, I promised myself that I would post more this year, and that clearly has not happened.)

If there’s any main takeaway here, it’s that while types are restrictive of what functions you can write, those same restrictions can provide surprisingly strong guarantees on the behavior of functions that type-check. In particular, OxCaml modes are sufficiently strong to let us statically ensure that a function uses its arguments in alternating ways, which is perhaps surprising to those who haven’t played with such modes yet. The art of designing good type systems, then, is arranging those restrictions in precisely the right way—admitting only the useful programs while keeping the ill-behaved ones out.

Back when I took his programming languages class, Bob Harper used to say that it was the strictures—especially types—that give rise to the expressiveness of programming languages. If you’ll forgive a bit of non-rigorous musing, I’ve always viewed this as somewhat analogous to the situation in poetry: if you read, say, a sonnet or a limerick, the artistry lies at least partly in adherence to the restriction of form; constraints inspire creativity. I think I personally don’t find free verse as compelling, just as I don’t find dynamically typed languages that compelling, even though both have taken the modern world by storm.