🐫 Songs of the OCaml Compiler Part II: A Design Tour

This is Part II of a series on learning OCaml by writing a Paxos simulator. We build on Part I’s abstract grammar and witness how subsystems take shape from it — guided, as it turns out, by the OCaml compiler I’m sure the magical source within the compiler is the underlying Hindley-Milner Type system which expects the programmer to exercise clearer type-discipline in exchange for superior inference capabilities that feel like an extension to the programmer’s own mind. I’ve put up a few words about what that experience has been like here <TODO: add reference to part 3 where we reflect on the experience of working with the compiler> itself.

Written primarily for a technical audience A little programming experience goes a long way. I won’t focus heavily on syntax – OCaml’s consistency makes it readable. For code-examples, I describe intent wherever possible so that unfamiliar syntax never gets in the way. Part II gets more involved in places where the type system is the point, but non-technical readers can gloss over those sections without losing the thread. , this series can be read in different orders – see the cover post for suggested reading paths. By prioritising intuition over a pedantic focus on syntax, I’m hoping that a more general audience may find this useful There are some early signs of usefulness (see Part III’s) <TODO link to appropriate part in Part 3 for this>. Please reach out for comments <TODO link to part 3 for RFC> as well.

From Forces to Forms: the Emergence of Subsystems #

Part I ended before any code was written so that when the first let statement appeared, the system’s shape was already half-decided by deliberating on the forces at play – this was by design. What follows is an account of the other half: the three places where the OCaml compiler itself influenced my design, and what I learned from listening to it.

A Quick Primer on the Paxos Protocol #

4 Layers of Responsibility #

These forces encouraged me to see the implementation as having the following concrete layers of responsibility:

These aren’t equal in weight: the Node Logic layer carries the Paxos protocol itself and is where most of the interesting type-system work lives. The other three are the infrastructure harnesses that make the system observable and controllable. The boundaries emerged from the grammar constraints, not from OCaml conventions – so this is just my way of reacting to the forces at play here.

The Big Picture Map #

The architecture map below outlines my simulator’s design – it’s my way of consolidating structures and some rules of thumb in a diagram Clicking on various parts of the diagram will lead you directly to the code. . I recommend reading it top-to-bottom in two passes: first, ignoring the details and trying to understand the layers that the diagram shows and then zooming in layer-by-layer. Each layer zooms closer to the Node and the last section shows how to make a Node.

To prime us for the design pressure stories that come after, I'll draw attention the OCaml specifics (e.g. functors like Make_node) will be explained in each section; for now, treat this as a signpost of where we’re headed and the following diagram as the overall map of what was implemented to a couple of things:

TODO: [ polish ] with the new phrasing and flair applied to the 3 design pressures, consider if there’s better ways to prime / sign-post them from within this table.

TODO: [ polish ] the description of the pressures likely needs to be tightened

This is the form that the grammar ended up taking. The map feels orderly from here: there are clean layers, named boundaries and the functor arrows show how we compose our structs. This orderliness took some iterating. What the map doesn’t show are the moments where the compiler refused to accept what I had written. Understanding why it refused changed how I thought about the design.

Design Pressures #

These moments are the focus of the rest of this post. We start small by describing some newbie snags these are just common misconceptions / missteps since we’re learning something fresh – I’d like to think of it as the tax we pay as newbies faced when wiring up the subsystems using functor-based dependency injection. It will show how the compiler’s feedback and cautions helped identify some fundamental blind-spots in my understanding of the type system. We then progress to how state-machine invariants had to be managed – and how, when I reached for GADTs to codify them, the compiler pushed back and tempered my ambition in certain cases. Finally, we see the pattern of keeping clean mutation-boundaries as an example of how the collaborative relationship between the programmer and the compiler leads to thinking in its grammar anyway – even if the compiler has nothing to say.

These moments started off as noise – type errors that I couldn’t immediately explain and constraints that felt arbitrary – and they gradually acquired a melody. Three movements, three design pressures.

Functor-based Dependency Injection: Decoupling Subsystems at Compile-Time #

We’ve seen that the combined node (center of the architecture map) has its own State, is bound to a Bus for communication purposes and relies on Storage for having the ability to recover from failures. Central to these is the idea of a “value” that the system achieves consensus on, which all these modules need to play nice with. So we define it as an abstract type behind a module signature (Value.S) — any module that satisfies Value.S can be swapped in without us having to rewrite anything. A byte-string today, perhaps a MIDI note tomorrow to make nodes that literally sing not entirely a joke — the consensus logic is completely agnostic to what’s being agreed upon. A leadership lease, a configuration delta, an audio sample: the protocol doesn’t care. , or more practically, a heterogeneous product type — consensus value AND a leadership-lease so the cluster knows which node to follow.

This is a classic case of parametric polymorphism Parametric polymorphism means: write the logic once, and it works for any type — the parameter fills in the blank. A list that sorts any comparable element, a bus that carries any message type, a consensus protocol that works for any agreed-upon value. The word “parametric” here signals that the abstraction is over a type parameter, not over specific values. that we want: the logic for achieving consensus has to be abstracted over the type of payload that we’re achieving consensus over. We just need the same V.t (value type) to flow through the different modules consistently. This seems straightforward: the ML ML as in Meta-Language. It’s a whole family of programming languages out of which OCaml is a member -world commonly uses parameterised modules as a building block for structure and composition of swappable-logic. This fits our need for injecting this payload dependency and it’s how we end up with the Make_node functor.

# Python: injection happens at runtime -- V and Bus are passed as objects
class Node:
    def __init__(self, value_module, bus_module):
        self.value = value_module
        self.bus   = bus_module

    def propose(self, v):
        serialized = self.value.serialize(v)  # runtime dispatch: dict lookup
        self.bus.publish(serialized)          # runtime dispatch: dict lookup

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18

module Make_node (V : Value.S) (Bus : Event_bus.S) : (* << functor >> with 2 parameters: V and Bus*)
S with module V = V with module Bus = Bus = struct
  module V = V
  module Bus = Bus
  module State = Make_node_state (V)
  module Storage = Make_file_storage (State)
  (*...*)
  type t = {
      id : Types.node_id;
      alias : string;
      config : config;
      mutable state : State.role_state;
      subs : topic_to_sub_handle_to_bus_registry;
      logger : Logger.t;
      storage : Storage.t ref;
    }
 (*...*)
end

The Simulator calls Make_node, and that’s also where the Bus module type is concretised. In the snippet below, the partition type shows us the actual type of the bus here.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

module Simulator : Runtime.S = struct
  module V = Value_string.Value_string
  module B = Event_bus (* [1]: the concrete Bus module*)
  module N = Node.Make_node (V) (B) (* [2]: functor application -- the same V and same B get injected to yield the concrete module N which satisfies the Node signature (Node.S) *)
  (*...*)
  (*[3] partition type is a product type, we can see the type for bus here*)
  type partition = {
      id : partition_id;
      mutable member_node_ids : int_set;
      bus : V.t Message.t B.t; (* B.t is polymorphic: type 'a t.
                               Here we instantiate as (V.t Message.t) B.t,
                               i.e. a bus carrying payloads of type Message.t
                               (the 'a param). V.t is the "value" we're achieving consensus on. *)
    }
  (*[4] we rely on routines for partition-creation*)
  let create_partition sim id =
    let bus =
      B.create
        ~log_level:(sim |> logger_of |> Logger.get_level)
        ~payload_to_string:(V.sexp_of_t |> Message.to_string)
        ()
    in
    { id; member_node_ids = Set.empty (module Int); bus }
    (*...*)
end

The bus creation signature (B.create) makes the polymorphism explicit:

1
2
3
4
5
6
7
8
9

(* so that the payload (messages) can have a string representation *)
type 'a payload_serialiser = 'a -> string

(* creation routine *)
val create :
  ?log_level:Log_level.t ->
  payload_to_string:'a payload_serialiser ->
  unit ->
  'a t

Things look right. V.t appears to flow correctly: Value_string.Value_string.t is string under the hood and the B.create signature is polymorphic in 'a – the bus doesn’t care what it carries, as long as we supply a serialiser for logging the payload.

So we should be also be able to implement the create function like so \(\ldots\) right?

1
2
3
4
5
6
7
8

let create_partition sim id =
  let bus =
    B.create
      ~payload_to_string:(fun msg ->
        Sexplib.Sexp.to_string (Message.sexp_of_t Base.String.sexp_of_t msg))
      ()
  in
  { id; member_node_ids = Set.empty (module Int); bus }

Newbie Snag: Understanding Nominal Typing #

File "lib/simulator.ml", line 189, characters 52-55:
189 |     { id; member_node_ids = Set.empty (module Int); bus }
                                                          ^^^
Error: The value bus has type string Message.t B.t
       but an expression was expected of type V.t Message.t B.t
       Type string is not compatible with type V.t
Had 1 error, waiting for filesystem changes...

This is the first proper newbie snag I faced. Without the fundamentals, this is extremely annoying because it’s hard to connect the dots. The newbie thinking would likely be that technically, at the concrete level we should have already satisfied the type of payload_to_string, it should have work because Value_string.Value_string.t is string. The implicit assumption being that surely OCaml can handle structural typing (e.g. like in TypeScript), not nominal typing?

If we listen carefully, the error message is already guiding us: type string Message.t B.t and type V.t Message.t B.t are not the same i.e. the two types don’t unify.

The fix is simple, we just have to respect the module boundaries and use V’s serialiser (V.sexp_of_t):

let bus =
    B.create
-      ~payload_to_string:(fun msg ->
-        Sexplib.Sexp.to_string (Message.sexp_of_t Base.String.sexp_of_t msg))
+      ~payload_to_string:(V.sexp_of_t |> Message.to_string)
      ()
  in

This was an unfortunate time-sink. The optimist in me would be appreciative of the fact that the OCaml compiler is strict and principled – it encourages us to respect interface boundaries. So, it becomes a matter of perspective whether the compiler is admonishing us or singing a cautionary note the compiler as critic before it becomes collaborator — this is the first bar of that melody .

The second snag was in the same neighbourhood — the module signature boundary — but more architectural in its consequences.

Newbie Snag: Destructive Substitution #

During an earlier refactor, I had extracted Acceptor_record and Node_state as separate functors (before they were eventually collapsed back into Make_node). The intent felt clean: Acceptor_record depends on Value, so it should be its own Make_acceptor_record(V); Node_state depends on Acceptor_record, so Make_node_state(A : Acceptor_record.S) should naturally reach through to A.V for the value type. To keep the output signature tidy, I used destructive substitution (:=) when writing the Acceptor_record signature:

module Make_acceptor_record (V : Value.S) :
  S with module V := V = struct
  (* ... *)
end

and tried to access the V within the concrete Acceptor_record, A like so:

module Make_node_state (A : Acceptor_record.S) : S = struct
  module V = A.V   (* ⛔️ compiler error: A has no member V *)
  (*...*)
end

The compiler outright refused, saying that “A had no V within it”. From my newbie-lens, this made no sense: V was plainly declared within Acceptor_record.

Turns out, the diagnosis is this: := works by erasing. with module V := V removes V from the output signature entirely. The path A.V no longer exists because there is no V to reach through to. Hence, the term “destructive”.

The fix was to switch to a plain sharing constraint:

- S with module V := V = struct
+ S with module V = V = struct

A.V is now accessible downstream because V remains in the output signature (Acceptor_record.S), its identity is pinned to the functor argument, A.

Takeaways #

The meta-lesson here is less about syntax and more about what module signatures actually are: access-control boundaries, not just type hints. Erasing a path is a meaningful act — one that the := syntax makes easy to do accidentally.

(* Internal node types *)
type assertion = V.t Types.paxos_assertion_state [@@deriving sexp]
type promise   = assertion option [@@deriving sexp]

(* Boilerplate converters: internal ↔ message-layer *)
let paxos_assertion_of_assertion (a : assertion) : V.t Types.paxos_assertion_state =
  { proposal = a.proposal; value = a.value }

let assertion_of_paxos_assertion (paxos_a : V.t Types.paxos_assertion_state) : assertion =
  { proposal = paxos_a.proposal; value = paxos_a.value }

let promise_of_paxos_promise (paxos_p : V.t Types.paxos_promise) : promise = (* ... *)

- type assertion = V.t Types.paxos_assertion_state [@@deriving sexp]
+ type assertion [@@deriving sexp]

We now advance to a deeper pressure: one that asks how much the type system can actually guarantee about a state machine.

Enforcing State Machine Invariants: to GADT or not to GADT? #

Earlier in the quick primer for the Paxos Protocol, we saw the happy case where 3 different nodes coordinated to achieve consensus. There’s a whole world of edge-cases to deliberate on if we went with that approach — so we shift our attention to representing the protocol’s wisdom via Finite State Machines (FSMs) Just like the adage earlier about the Python language and its reliance on lookup tables, here’s another one about Computer Science / Programming in that “All Programming Philosophies are about State” or, “everything is just a state machine”. Some interesting reads on this if you’re not familiar with what State Machines are about: old blog post by Shopify on why every developer should be force-fed state machines. Coming from the Elixir world, the GenServer abstraction is a beautiful pattern that is implicitly an FSM – see more elixir-discourse on FSM use-cases here. Sound FSMs make concurrency problems so much simpler to wrap our human-brains around! .

A Node Wears 3 Hats at the Same Time #

A node maintains 3 sub-states simultaneously: Proposer, Acceptor, Learner. Drawing out their FSMs before deep-diving into their logic forces us to be clear about a few things: which states are truly distinct versus merely named differently, which transitions carry side-effects (e.g. persistence, message-dispatch) versus pure state-changes, and which transitions should be impossible. The last category makes FSMs a powerful design and analysis tool for protocol implementations: if we can enumerate the illegal transitions, we can start asking whether the type system can prevent them at compile time rather than at runtime.

The Proposer FSM is the most complex of the 3 — six states for v0, the Aborted state is actually just a shim. It’s not critical to the flow yet because we omit retry mechanisms in v0. , two quorum decision gates, and a simulation-control state that will cause us trouble shortly \(\ldots\)

What immediately stands out to us from the Proposer state-diagram is that the current version of this FSM actually has 2 categories of states that are represented:

This means that as it currently stands, the simulation-level states (Blue-coloured states) and the protocol-level states (Green-coloured states) are in the same sum-type A sum type (also called a tagged union or discriminated union) is a type that can be exactly one of several named alternatives. In OCaml, these alternatives are called variants. If you come from TypeScript, think of a discriminated union; from Rust, an enum with data; from Java/Kotlin, a sealed class hierarchy. The key property being: a match expression over a sum type is exhaustive – the compiler warns you if you forget a case. A product type, mentioned earlier, is the complement: a type that holds several values simultaneously (a record or tuple). So, Sum = “one of these”; product = “all of these together”. . Therefore, our type-system can’t distinguish “active protocol state” from “simulation inactive state” since they’re all siblings in one flat variant. This affects how we make guarantees that the system won’t have illegal state transitions, which is fundamental to many of the protocol invariants An invariant is a property that must always hold true, no matter what path the system takes. For our Paxos FSM, one invariant is: “a quorum check only happens when the proposer is in WaitingForPromises or ProposerAccepting.” Another: “a node may only broadcast Decided if it has actually reached a decision.” Violating invariants goes beyond just producing wrong answers, it actually makes a protocol’s safety-guarantees meaningless. The question is whether we enforce these invariants via runtime checks (hoping the programmer got it right) or via the type system (making it impossible for anyone to get wrong when writing the source code) .

A great place to see this happening is when we’re making decisions on what to do next based on whether a quorum has been reached. These correspond to the two quorum-gates (orange-coloured diamond nodes) that we see in the diagram. Both these decision-points rely on the same predicate function, is_quorum_reached. We know that the node only calls this predicate function when it’s in 2 possible Proposer states: WaitingForPromises OR ProposerAccepting – all other entry-points coming from all other states are illegal. So how can we guarantee that we meet this invariant?

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15

  (** Quorum predicate for both phase 1 and phase 2 of paxos.

      NOTE: This runtime check exists because proposer_state includes both
      active and inactive variants. A GADT-typed view layer
      (active_proposer_state) would eliminate this branch entirely.*)
  let is_quorum_reached cluster_size rs =
    match Proposer |> get_role rs with
    | WaitingForPromises wfp ->
        wfp |> is_quorum_reached_on_promise_wait cluster_size
    | ProposerAccepting pa ->
        pa |> is_quorum_reached_on_proposer_accepting_wait cluster_size
    | _ ->           (* <== wildcard-arm *)
        failwith
          "is_quorum_reached called on non-proposer state (must be \
           WaitingForPromises or ProposerAccepting)"

Our current solution is to use a wildcard arm that invokes a failwith — our hands are forced at the moment to rely on runtime checks. This failwith approach works because the program does the right thing at runtime if the call-sites are correct.

If someone – including a future version of us – adds a new call to is_quorum_reached from a handler that processes Idle nodes, the compiler won’t object. The program would compile, the tests would pass (unless we wrote one for that exact path), and the bug would hide until a specific scenario triggers it at runtime. For a consensus protocol, that’s a silent correctness violation. We’re leaving safety on the table that the compiler could be providing for free. By the way, we risk this at other places too:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16

  let announce_decision
      ({ id; alias; logger; state = { proposer; _ }; _ } as t : t) ~msg_id ~time
      decided_assertion =
    match proposer with
    | State.Decided _decided_val ->
        Logger.log_announce_decided_action ~id ~alias
          ~assertion:(decided_assertion |> assertion_to_string)
          logger;
        let msg =
          Message.make_decided ~msg_id ~time ~from:id ~decided_assertion
        in
        let bus = bus_for_topic t Types.Coordination in
        ((Types.Coordination, None), msg) |> Bus.enqueue bus ~alias
    | _ ->
        failwith
          "a node can only announce what it has learned when it has decided "

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

  (** Represents the act of a node driving the first step of the paxos process
      (asking for permission). This means that the node's state as a Proposer
      will change from [ Idle ] to [ Peparing ], as we create the message then
      dispatch it. Once done dispatching, the node will change its state to
      [ WaitingForPromises ], marking it ready to receive responses (both grants
      and nacks) for that proposal.

      As such, every paxos process (i.e. an attempt to assert a value and seek
      consensus) can be uniquely identified via its [proposal_id] *)
  let propose ~msg_id ~time ~bus ~assertion
      ({ id; alias; logger; state = { proposer; _ }; _ } as t) =
    match proposer with
    | State.Idle ->
        Logger.log_proposal_action ~id ~alias
          ~assertion:(assertion |> assertion_to_string)
          logger;
        assertion |> State.Preparing
        |> transition_role_state t time State.Proposer;
        let msg =
          Message.make_permission_request ~msg_id ~from:id ~assertion ~time
        in
        ((Types.Coordination, None), msg) |> Bus.enqueue bus ~alias;
        { assertion; promises_received = []; nacks_received = [] }
        |> State.WaitingForPromises
        |> transition_role_state t time State.Proposer
    | _ -> failwith "we can only propose if we are currently idle"

There’s something interesting in is_quorum_reached that may already help us \(\ldots\)

GADTs to the rescue? #

The get_role function-call within is_quorum_reached is fascinating and compels us to look at its signature.

let get_role : type a. role_state -> a role_selector -> a

This invites us to inspect the machinery here to understand how it works. type a in the signature of get_role is a locally-abstract type read: placeholder type that exists within this function (get_role) only. This type variable (a) is progressively refined as we pattern-match on the role_selector. Read more here. . It introduces a type variable (a) that is scoped to this function (get_role) which the compiler refines on each branch of There’s an OCaml forum post that goes through some misconceptions around this role_selector. This means that the compiler learns which specific type a is by looking at which constructor matched. role_selector is our Generalised Algebraic Data Type (GADT) here.

179
180
181
182
183
184
185
186
187
188

(** GADT to encode which role and its sub-state type This encodes the
    association between a constructor (Proposer, Acceptor, Learner) and its
    precise sub-state type. *)
type _ role_selector =
  | Proposer : proposer_state role_selector
  | Acceptor : acceptor_state role_selector
  | Learner  : learner_state role_selector
  (* each arm follows the pattern:
  | <constructor> : <return_type> role_selector
  *)

Each constructor carries its return type in its signature, that’s why we can say that the GADT indexes the type parameter. This means that if the pattern-matching triggers on Proposer, then the compiler will know that a = proposer_state — Proposer is the variant that produces proposer_state. This indexing mechanism is useful to select amongst the different states (proposer_state, acceptor_state, learner_state).

The signature for Node_state shows how all six proposer states – including ProposerInactive – live in one flat variant, which is precisely the structure the GADT indexes over:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40

(** Part of the Node_state signature, showing how
    the FSM states within Proposer State can be built-up*)
module type S = sig
  (*...*)
  type waiting_for_promise_state = {
    assertion : assertion;
    promises_received : promise list;
    nacks_received : nack list;
  }
  [@@deriving sexp, yojson]

  (** State for a proposer actively collecting Phase 1 responses. *)
  type proposer_accepting_state = {
    assertion : assertion;
    acks : Types.node_id list;
    nacks_received : nack list;
  }
  [@@deriving sexp, yojson]

  (** States for the proposer role. *)
  type proposer_state =
    | ProposerInactive
        (** Node is unavailable; proposer cannot act until restored. *)
    | Idle  (** Proposer is available and may initiate Phase 1. *)
    | Preparing of assertion  (** Proposer has begun Phase 1. *)
    | WaitingForPromises of waiting_for_promise_state
        (** Proposer is waiting for a quorum of Phase 1 responses. *)
    | ProposerAccepting of proposer_accepting_state
        (** Proposer has entered Phase 2 and is collecting acceptances. *)
    | Decided of V.t  (** Proposer has reached a chosen value. *)
  [@@deriving sexp, yojson]

  type role_state = {
    proposer : proposer_state;
    acceptor : acceptor_state;
    learner : learner_state;
  }
  [@@deriving sexp, yojson]
  (*...*)
end

The usefulness of this indexing is clearer when we see the signature of set_role, the write complement to get_role’s read operation.

let set_role : type a. role_state -> a role_selector -> a -> role_state

Since the third argument to this function ( a ) is constrained by the role_selector, the compiler will forbid us from passing the wrong role. We won’t be able to pass an acceptor_state when the selector says Proposer. GADTs are shaping up to be the antidote to our earlier problem where we were looking for compile-time assurances so that we could do better than “correct by programmer discipline”. With this, an entire class of “wrong role” bugs are avoided at compile time.

In fact, we actually use it for our transition_role_state where we can see it all coming together.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18

  (** Polymorphic transition function for role state. This is a classic
    GADT-indexed update, which is entirely side-effect focused.*)
  let transition_role_state ({ id; alias; logger; state; storage; _ } as node)
      time (type a) (sel : a State.role_selector) (new_substate : a) =
    let new_state = new_substate |> State.set_role state sel in
    Logger.node_state_change ~node_id:id ~alias logger
      ~old_state:(state |> State.state_to_str)
      ~new_state:(new_state |> State.state_to_str);
    node.state <- new_state;
    let updated_storage =
      match node.state |> Storage.persist_snapshot !storage time with
      | Ok updated_storage -> updated_storage
      | Error e ->
          Stdio.eprintf "Warning: failed to persist snapshot: %s\n%!"
            (Error.to_string_hum e);
          !(node.storage)
    in
    node.storage := updated_storage

Every state transition in the entire system flows through this one function. The GADT ensures that the selector and the new substate agree on which role is being updated. It prevents us from accidentally transitioning the proposer state with an acceptor state. This is a genuine compile-time enforcement of types and it’s already helping us.

Though it solves the “wrong role” class of errors, it doesn’t really solve the “wrong state within a role” class of errors. is_quorum_reached still accepts ANY proposer_state (including Idle, ProposerInactive) because currently the GADT indexes over roles and not over states within a role. The _ in role_selector means “we don’t need to name the type parameter at this point – there exists a type parameter here, but we’re not going to bother naming it”. It helps us track More precisely, _ is an anonymous type parameter. Each GADT constructor instantiates it with a specific concrete type (proposer_state, acceptor_state, learner_state). This is called type indexing: the parameter serves as a compile-time tag. Pattern-matching on it introduces local type equalities that are valid within each branch. the sub-state type (e.g. acceptor_state vs learner_state). However, it doesn’t constrain which variant within that substate is allowed – so we can still call operations like is_quorum_reached on Idle or ProposerInactive nodes.

The Serialisation Wall & Knowing the Tradeoff-Surface #

So, the natural move is to add in more GADTs, right? The idea practically writes itself. We saw the role_selector GADT prevent “wrong role” bugs. The natural next step is to introduce an active_proposer_state GADT that only admits WaitingForPromises and ProposerAccepting – making it structurally impossible to call is_quorum_reached on Idle or ProposerInactive nodes. The failwith arms then disappear. The compiler catches the rest. Clean, green, state-machine.

Except, our state types carry a pre-processor annotation As seen in the highlighted lines of the Node_state signature above, @@deriving@@ is an OCaml preprocessor attribute (metaprogramming in OCaml that does AST-to-AST transformations) that auto-generates boilerplate code. Think “code that writes code”: telling the compiler “emit serialization functions for this type” saves us writing dozens of lines of sexp_of_ and of_yojson by hand. ([@@deriving sexp, yojson]) – they’re serialisable. At every state transition, we persist a snapshot to storage. This enables the simulator to dump, reload, diff, and replay node state at any point in time. That’s a fundamental capability of the simulator as a teaching tool.

type active_proposer_state =
  | WaitingForPromises
  | ProposerAccepting  (* every arm produces active_proposer_state *)

type _ active_proposer_state =
  | WaitingForPromises : waiting_for_promise_state -> waiting_for_promise_state active_proposer_state
  | ProposerAccepting : proposer_accepting_state -> proposer_accepting_state active_proposer_state

The compiler knows about it too – attempting to slap [@@deriving sexp] on our hypothetical active_proposer_state GADT would produce a build error. This is the compiler scolding us again, but this time, the scolding is pointing at a deeper design tension.

Pushing ahead with a full GADT encoding of the proposer states would mean writing custom serialisers, maintaining a parallel “erased” representation for storage, and updating both layers every time the state machine evolves. Every new constructor would require updating the GADT, the erased representation, the serialiser, the deserialiser, and the pattern matches that assumed exhaustiveness – five coordinated changes where the compiler can’t help us across the erased boundary. The burden of the impossible-case failwith we wanted to eliminate from the FSM handling just migrates to the serialisation logic – if we do this, we’d just be relocating the problem, not removing it. That’s the Serialisation Wall we face but we need not climb it.

type proposer_state =
  | ProposerInactive | Idle
  | Preparing of assertion
  | WaitingForPromises of waiting_for_promise_state
  | ProposerAccepting of proposer_accepting_state
  | Decided of V.t
[@@deriving sexp, yojson]

type _ active_proposer_state =
  | WaitingForPromises :
      waiting_for_promise_state -> waiting_for_promise_state active_proposer_state
  | ProposerAccepting :
      proposer_accepting_state -> proposer_accepting_state active_proposer_state

let active_proposer_of : proposer_state -> _ active_proposer_state option = function
  | WaitingForPromises w -> Some (WaitingForPromises w)
  | ProposerAccepting p -> Some (ProposerAccepting p)
  | _ -> None

let is_quorum_reached_active ~cluster_size
    (state : _ active_proposer_state) : quorum_result =
  match state with
  | WaitingForPromises wfp ->
      is_quorum_reached_on_promise_wait cluster_size wfp
  | ProposerAccepting pa ->
      is_quorum_reached_on_proposer_accepting_wait cluster_size pa

The failwith calls stay. They’re documented, they’re tested The test-suites for this project have covered the fundamental areas to protect. For this, this section within test_fsml.ml TODO: permalink to test failwith/is_quorum_reached section , and the two-layer escape hatch is designed for when the state machine stabilises a bit more.

Emerging Patterns: Clarity from Clean Mutation-Boundaries #

So far, the design pressures were driven by the compiler speaking – errors, warnings and build-failures that forced us to reconsider our design. Now, we arrive at a case where the compiler has nothing to say. And yet, instinctively, we find ourselves inheriting its discipline and idioms to judge clearer code-paths that give us clarity in places where the compiler can’t directly assist.

Let’s look at transition_role_state again — we had side-stepped the side-effects to focus on the GADT-indexed dispatch previously:

If we swap out the lens of type-level correctness with one for discipline-level correctness, we start seeing the clarity within this flow of data. Every protocol handler (e.g. propose) computes a new substate purely and then delegates to this sole function for the side-effects. A single-point for all stateful effects of transitions means that it’s a clear mutation-boundary — it wasn’t planned from the beginning, it emerged.

Actors in Charge of Their Own Mailboxes #

We’ve been following the Actor Model of computation to represent logical units within our system. Each node owns its state exclusively and talks to others only through messages — a pattern we prescribed back in the Design Grammar in Part I.

Coming from the world of Elixir/Erlang, this concurrency-model is instinctive for me. We have processes (GenServers) with mailboxes, message passing, and isolation by default there. That instinct carries over Coming from Elixir, where GenServer gives you process-isolated mailboxes with selective receive and supervision for free, the instinct to build a per-node inbox was natural. The pattern was sound and it worked – but OCaml’s single-threaded (self-imposed v0 implementation constraint), functor-composed world offered little runtime support for the abstraction, so the coupling that Erlang’s runtime hides became visible in this OCaml codebase. : so the natural first-reach for an earlier version of the implementation was to give each node (Actor) a mailbox and let messages accumulate.

Here’s the rough shape of how it worked:

For this design, we notice that mutations get distributed across layers — every segment of the pipeline has mutations. This means three different functions \(\Rightarrow\) three different mutation-sites. There’s no single place where we can see “what happens when state changes”. Also, the lifecycle of an inbox is spread over multiple places.

The concurrency model is correct here. The inbox-pattern also works, but it doesn’t have the snap-together feel it would have had if it were a simple design.

Chaos Naturally Converges into Clarity #

The FSM restructuring that was made in response to the compiler’s guidance for the previous pressure actually improved more than just type-safety. It unlocked new code-paths for us. Thanks to the layered, role-based substates, each FSM state can now carry its own accumulated data. We saw this earlier within waiting_for_promise_state (part of the Proposer state). There, we now hold promises_received and nacks_received (both, as an ordered list of promises/nacks) as part of that substate record. The stateful inbox gets sidelined into a redundant, parallel accumulator.

With the inbox now gone, where do the side-effects go?

Once the pure computation (assembling of new substate at handlers like propose ) is separated from the effectful execution (mutation, logging, persistence), we automagically see a clear mutation-boundary forming. All the side-effects naturally converge on transition_role_state.

Once the boundary between pure and effectful code was visible, conventions naturally cascaded from it – in how we name things, how we construct them, and how we guard entry to state-dependent logic.

(* Pure assembly — no mutation, deterministic from arguments *)
let make_permission_request ~msg_id ~time ~from ~assertion =
  {meta= make_meta msg_id time Types.Coordination; from; assertion}

(* Resource allocation — creates fresh mutable bus, initialises set *)
let create_partition id =
  let bus = B.create ~payload_to_string:(...) in
  {id; member_node_ids= Set.empty (module Int); bus}

module type Has_spec = sig
  type t
  type spec [@@deriving sexp, yojson]

  val of_spec : spec -> t
end

module type S = sig
  module V : Value.S
  module Bus : Event_bus.S
  module State : Node_state.S
  module Storage : Storage.S with type snapshot_payload = State.role_state

  type t

  include Has_spec with type t := t (* 🔥 DESTRUCTIVE! 🔥 *)

  (*...*)
end

module Make_node (V : Value.S) (Bus : Event_bus.S) :
  S with module V = V with module Bus = Bus = struct
  (*...*)

  (**Shape of the static config for Node *)
  type spec = {
    node_id : int;
    node_alias : string;
    topic_strs : string list;
    initial_cluster_size : int;
    initial_state : string option; [@default None] [@yojson_drop_default]
    storage_config : string option; [@default None] [@yojson_drop_default]
  }
  [@@deriving sexp, yojson]

  (*...*)

  (** Hydration routine*)
  let of_spec { node_id; node_alias; topic_strs; initial_cluster_size; _ } =
    let default_state = State.init_state () in
    let config =
      {
        runtime = { cluster_size = ref initial_cluster_size };
        roles =
          [ "Acceptor"; "Learner"; "Proposer" ]
          |> List.filter_map ~f:role_of_str;
        topics = topic_strs |> List.filter_map ~f:Types.topic_of_str;
      }
    in
    {
      id = node_id;
      alias = node_alias;
      state = default_state;
      config;
      subs = Hashtbl.Poly.create ();
      storage = ref (Storage.create ~alias:node_alias ());
      logger = Logger.create Stdlib.__MODULE__ ();
    }

  (*...*)

  (** De-hydration routine*)
  let to_spec { id = node_id; alias = node_alias; config; _ } =
    {
      node_id;
      node_alias;
      topic_strs = config.topics |> List.map ~f:Types.topic_to_str;
      initial_cluster_size = !(config.runtime.cluster_size);
      initial_state = None;
      storage_config = None;
    }

  (*...*)
end

let with_active ~node ~ignore_reason f =
  if node.state |> State.is_inactive then ignore_reason |> noop_ignore node
  else f ()

  let handle_coordination node msg =
    with_active ~node
      ~ignore_reason:
        "inactive right now and can't be reached to get coordinated..."
    @@ fun () ->
    log_flow ~routine:Stdlib.__FUNCTION__ ~msg:"...coordination is happening"
      node;
    match msg |> Message.proposal_id_of with
    | None -> ()
    | Some _proposal_id -> (
        match msg with
        | Message.Coordination (PermissionRequest pr) ->
            pr |> handle_permission_request node
        | Message.Coordination (PermissionGranted pg) ->
            pg |> handle_permission_granted node
        | Message.Coordination (Suggestion s) -> s |> handle_suggestion node
        | Message.Coordination (Accepted a) -> a |> handle_accepted node
        | Message.Coordination (Nack n) -> n |> handle_nack node
        | Message.Coordination (Decided d) -> d |> handle_decided node
        | _ ->
            failwith
              "We can only coordinate if we receive a coordination message.")

def requires_active(func):
    """ A decorator-based precondition guard"""
    def wrapper(node, *args, **kwargs):
        if node.is_inactive():
            log(f"{node.alias}: inactive, ignoring")
            return
        return func(node, *args, **kwargs)
    return wrapper

@requires_active # <--- applying that decorator
def handle_coordination(node, msg):
    # business logic assumes node is active
    ...

These aren’t any compiler-rules that we’re obliged to follow — they’re just extrapolations that we arrive at ourselves because they give us more of that satisfactory snap-together feel when we implement them.

In the Absence of the Compiler, We Hum its Tunes #

What’s fascinating is that the type system doesn't enforce any of the things In fact, OCaml has no effect system i.e. there’s no annotation that says “this function is pure” or “side-effects live here”. Also — and this is something that blew my mind as a newbie into this language — OCaml is actually a general-purpose language. For example, we can use the power of Classes, Objects, First-class Modules (packed), Mixins, Inheritance \(\ldots\) levers you’d typically find in the OOP-world. Not to forget, imperative programming levers are also available. we just went through — e.g. nothing will stop someone from writing a create_* function that actually is pure, or a make_* function that allocates a mutable ref.

Yet, the discipline holds because of the compiler’s influence on our way of thinking. “What’s the shape of that struct, the direction of data-flow, the signature of that function, is it immutable or are we writing imperative logic in that area \(\ldots\) " – these are the threads of thought that makes the patterns feel natural, self-evident and emergent.

What started as noise – type errors we didn’t yet understand, constraints that felt arbitrary – became a teacher’s voice we learned to trust. And what that voice left behind, once the specific errors were resolved and the specific constraints were satisfied, was a habit of thought: a preference for explicit boundaries, a sensitivity to where mutation lives, a belief that the names we give things should carry the weight of the architecture.

Closer #