12.13 — Lambda calculus, ROP, Haskell / F# / OCaml, monads#

Ocarina invents nothing on the theoretical front. It applies: from Alonzo Church’s lambda calculus (1936) to Eugenio Moggi’s (1989) and Philip Wadler’s (1992-95) monads, formalized as Railway Oriented Programming by Scott Wlaschin (2014).

1. Lambda calculus (Church, 1936)#

Definition#

Lambda calculus (λ-calculus) is a formal system invented by Alonzo Church (1903-1995) to study computability.

Why it’s foundational#

1. 1936: Church proves λ-calculus is Turing-complete (Turing publishes his machine in 1937). Church-Turing thesis: anything mechanically computable can be expressed in λ-calculus.
2. Alan Turing was Church’s doctoral student at Princeton (PhD, 1938).
3. λ-calculus is simpler than the Turing machine: only 3 constructions. Everything else — integers, booleans, data structures — is encoded with those 3 bricks (Church encoding).

Typed lambda calculus (Church, 1940)#

Church added types in 1940 (simply typed lambda calculus, STLC) to forbid self-application paradoxes (λx.x x). Each variable has a type, and function application is only allowed if types match.

It’s the direct ancestor of types in Haskell, OCaml, F#, TypeScript, Python, Rust, etc.

Curry-Howard (1934-1969)#

Haskell Curry observed the connection in 1934 (refined in 1958) and William Howard extended it in 1969:

A typed program is a mathematical proof.
A type is a proposition.
The type-checker is a proof checker.

That’s the Curry-Howard isomorphism: if code compiles under strict typing, it is mathematically correct along the dimensions encoded by the types.

Hence mypy --strict in Ocarina: it’s not an obsession, it’s not autism, it’s the application of the Curry-Howard theorem in an industrial setting.

2. ML (1973 to today)#

Robin Milner and ML (Edinburgh, 1973)#

Robin Milner (1934-2010, Turing Award 1991) designed ML (Meta Language) at Edinburgh as a language for automated proofs (Edinburgh LCF — Logic for Computable Functions).

• Hindley-Milner type system: complete type inference without annotations. The compiler guesses (infers) all types.
• Pattern matching: match x with | Cons (h, t) -> ... | Nil -> ....
• Parametric polymorphism: 'a list (list of anything).
• Functions as first-class values: passing a function as an argument.

ML genealogy#

                      ML (Edinburgh, 1973)
                               │
             ┌─────────────────┼────────────────────┐
             │                 │                    │
             v                 v                    v
      Standard ML             Caml              Lazy ML
      (Milner, 1983)       (INRIA, 1985)     (Chalmers, ~1984)      SASL, KRC (Turner)
             │                 │                    │                       │
     ┌───────┤                 v                    │                       v
     │       │             Caml Light               │                    Miranda
   SML/NJ    │             (INRIA, 1990)            │                (Turner, 1985)
(Bell Labs & │                 │                    │                       │
 Princeton,  └──> Alice ML     │                    └───────────────────────┤
   1987)        (Saarland,     │                                            v
                  2000)        v                                         Haskell
                             OCaml                                 (SPJ, Wadler, 1990)
                       (Leroy, INRIA, 1996)                                 │
                               └────────────────────────────────────────────┤
                                                                            v
                                                                           F#
                                                                    (Don Syme, 2005)
                                                                            │
                                                                            │
                                                                           […]
                                                                            │
                                                                            │
                                                                            v
                                                               Railway Oriented Programming
                                                                (Wlaschin, NDC London, 2014)
                                                                            │
                                                                            v
                                                                 ┌───────────────────────┐
                                                                 │        Ocarina        │
                                                                 │    Casanova (2026)    │
                                                                 │  Python 3.14 · mypy   │
                                                                 │  Result[T]            │
                                                                 │  ChainRunner · fold   │
                                                                 │  action chain state   │
                                                                 └───────────────────────┘

Note: some indicated dates correspond to design start.

First public release/implementation dates:

• ML → 1979
• Standard ML → 1990
• Caml → 1987

Haskell#

• Type classes (Wadler & Blott, How to make ad-hoc polymorphism less ad hoc, POPL, 1989), ancestor of Rust traits, Python Protocols, Go interfaces.
• Monads as a structure for representing effects (Wadler, 1992-95).
• Lazy evaluation by default, a feature almost unique to Haskell.

OCaml (1996)#

F# (2005)#

F# is heavily inspired by OCaml, adapted to the .NET ecosystem with syntax more accessible to C# devs. It’s in the F# community that Scott Wlaschin would formalize ROP.

Also, F* (2011, Microsoft Research & Inria) is F#’s academic cousin: same ML syntax, but oriented toward formal verification with dependent types — it can automatically generate F# or OCaml code from a formally verified program.

3. Monads#

Definition#

A monad is a parameterized type M[T] (a generic container) together with two operations obeying three laws:

1. Left identity: return(x) >>= f ≡ f(x)
2. Right identity: m >>= return ≡ m
3. Associativity: (m >>= f) >>= g ≡ m >>= (λx. f(x) >>= g)

Note: monads are sometimes presented as design patterns. The comparison isn’t entirely wrong — they do structure composition well — but it’s reductive. Monads are mathematical abstractions with formal laws, while design patterns are informal recipes without guarantees.

Famous monads#

Leibniz (1714)#

The term monad comes from Gottfried Wilhelm Leibniz (Monadology, 1714), from Greek μονάς (monos, “one, unique”). Leibniz defines the monad as “a simple substance, without parts”, the metaphysical atom of the world. Mac Lane reused the term for category theory. There is no conceptual lineage between the Leibnizian monad and the category-theoretic monad: Mac Lane borrowed the term for its etymological sense.

Eugenio Moggi (1989-91)#

Eugenio Moggi published in 1989 “Computational lambda-calculus and monads” (LICS). He imported monads from category theory (Godement, 1958) into language semantics. Before Moggi, monads were an abstract construction. After Moggi, it became the standard for formalizing side effects.

Philip Wadler (1990-95)#

Philip Wadler (then at Glasgow, later Edinburgh) popularized monads in Haskell:

• "Comprehending Monads" (presented 1990, published 1992)
• "The essence of functional programming" (POPL, 1992)
• "Monads for functional programming" (1992/1995)

Wadler showed how to write code that looks imperative — a sequence of operations, state, IO — while remaining pure thanks to monads. That’s the pedagogical innovation that anchored monads in Haskell practice.

4. Railway Oriented Programming (ROP) — Scott Wlaschin, 2014#

Context#

Scott Wlaschin, author of fsharpforfunandprofit.com and of the book Domain Modeling Made Functional (Pragmatic Bookshelf, 2018).

In 2014, at NDC London, he gave the talk "Railway Oriented Programming" — video on Vimeo, transcript on F# for Fun and Profit.

Pitch#

Most code looks like a railway with one track. Success goes through. Failure throws an exception, jumping off the rails.

Let me show you the two-track railway. Success on one track. Failure on the other. No exception. Every step decides which track to use. The composition is automatic.

Note: the pitch above is a paraphrase, not a direct quote.

In operational terms, it’s the Either monad rebranded with a visual metaphor.

Diagram#

        ╔═══════╗    ╔═══════╗    ╔═══════╗
in ────>║ step1 ║───>║ step2 ║───>║ step3 ║────> success ─┐
        ╠═══════╣    ╠═══════╣    ╠═══════╣               ├──► result
        ║       ║───>║       ║───>║       ║────> failure ─┘
        ╚═══════╝    ╚═══════╝    ╚═══════╝

Each step is a function T → Result[U]. Composition is mechanical: as long as it’s success, you continue. At the first failure, you switch to the lower rail and short-circuit every subsequent step.

Underlying theory#

Either monad:

data Either a b = Left a | Right b

• Right = success (upper rail).
• Left = failure (lower rail).
• >>= (bind) = the function that chains by short-circuiting on Left.

This is identical to Result[T] in Ocarina:

Result[T] = Ok[T] | Fail

Industrial adoption#

5. How Ocarina implements it#

Lambda calculus → closures#

Ocarina uses closures systematically where classic OOP would use inheritance or dependency injection.

A closure is a λ-abstraction with environment capture: λx.λy.M partially applied to N yields λy.M[N/x], a function that captures N in its environment.

def my_scenario(driver: WebDriver, logger: ILogger) -> Scenario:
    page = MyPage(driver=driver)

    return Scenario(
        # logger is captured in a closure, not "injected"
        setup=lambda: seed_test_user(logger=logger),
        teardown=lambda: delete_test_user(logger=logger),
        test_chain=[...],
    )

That’s IoC by closure, not by injection — lambda calculus at work.

Hindley-Milner → mypy strict + PEP 695#

class ActionChain[T]:
    def then(
        self, action_or_start: Action[T] | ActionStart[T]
    ) -> ActionStart[T] | NeutralActionStart[T]:
        ...

@final
class ValidationStartBlock[T]:
    def assert_that(
        self, predicate: Predicate[T], *, msg: str | None = None
    ) -> ValidationAssertBlock[T]:
        predicate = _with_msg(predicate, msg, self._name)
        self._chain.add_assertion(self._value, predicate, self._name)
        return ValidationAssertBlock(
            self._value, self._chain, self._name, last_predicate=predicate
        )

def then[U](
    self, new_value: U, *, name: str | None = None
) -> ValidationStartBlock[U]:
    return ValidationStartBlock(new_value, self._chain, name)

PEP 695 (Python 3.12+) introduces the [T, U] syntax.

Type tests#

Ocarina ships a dedicated test suite for types (test_types.yml).

Success cases confirm that mypy infers correctly, e.g. that T is preserved from ActionStart through to ActionChain:

- case: generic_type_preserved_through_chain
  main: |
    chain = ActionStart(lambda: Ok("hello")).failure(lambda e: None).success(lambda: None).execute()
    reveal_type(chain)  # N: Revealed type is .*ActionChain\[.*str.*\]

Failure cases verify that mypy does reject what should be rejected — that an incompatible predicate or a wrongly signed handler produces an error:

- case: incompatible_predicate_type
  main: |
    validate(1234).assert_that(is_email)
  out: |
    main:4: error: .* incompatible type .*

- case: execute_on_action_start_not_allowed
  main: |
    ActionStart(lambda: Ok(42)).execute()
  out: |
    main:4: error: .* has no attribute "execute".*

The runtime doesn’t check types (it’s STATIC typing!). mypy does. Type tests verify that mypy does its job both ways: that it accepts what’s valid and that it refuses what isn’t.

Either / Result → ROP#

Ocarina’s core is literally ROP:

• Result[T] = Ok[T] | Fail, that’s the Either monad.
• ChainRunner[T], that’s >>= composition.
• action chain state, that’s the state machine implementing the success-rail / failure-rail dichotomy.
• neutral, Wlaschin’s convention: a failure rail keeps going as if unchanged to the end (equivalent of the Left e traversing binds without evaluating).

F# computation expressions → ChainRunner / chain_actions / drive_page#

F# has computation expressions (result { … }), Haskell has do-notation — both expose bind/>>=.

ChainRunner[T] + chain_actions are inspired by the same idea (lazy sequentiality, short-circuit on failure), with a manual API. drive_page in ocarina-example is its direct semantic alias — it calls chain_actions identically:

# ocarina/opinionated/dsl/drive_page.py
def drive_page(
    first: ActionSuccess[TPOM], *rest: ActionSuccess[TPOM]
) -> ChainRunner[TPOM]:
    return chain_actions(first, *rest)

Which in real use in ocarina-example:

# tests/scenarios/dashboard/access/happy_paths.py
return [
    drive_page(
        act(on_dashboard_login_page, open_dashboard_login_page)
        .failure(just_log_error("Failed to open the dashboard login page..."))
        .success(just_log_success("Opened the dashboard login page!")),
        act(on_dashboard_login_page, verify_dashboard_login_page)
        .failure(log_error_with_current_url("Failed to verify the dashboard login page..."))
        .success(log_success_with_current_url_and_take_screenshot("Verified!")),
    ),
    drive_page(
        act(on_dashboard_welcome_page, verify_dashboard_welcome_page)
        .failure(log_error_with_current_url("Failed to verify the welcome page..."))
        .success(log_success_with_current_url_and_take_screenshot("Verified!")),
    ),
]

The short-circuit is explicit in the reducer of chain_actions — if a drive_page fails, the next ones don’t execute:

# ocarina/dsl/testing_with_railway/chain_actions.py
def reducer(chain: ActionChain[T], step: ActionSuccess[T]) -> ActionChain[T]:
    if chain.has_failed():
        return chain  # short-circuit — subsequent steps don't execute
    return (
        chain.then(step.__action__)
        .failure(step.__failure_handler__)
        .success(step.__success_handler__)
        .execute()
    )

match_page belongs to the same lazy family — it returns a ChainRunner whose _thunk() only evaluates conditions and runs the matching branch at .run() time, exactly like chain_actions. What distinguishes it is the nature of composition: conditional rather than sequential, and it can nest. In ocarina-example, it’s used to navigate pages with non-deterministic state (A/B tests, random banners, anti-bots):

# tests/scenarios/randomness/level_4/walkthrough.py
return [
    open_madness_random_page,
    match_page(
        branches=[
            when(check_that_madness.is_cors_page, name="is_cors_page",
                 then=go_from_cors_page_to_homepage),
            when(check_that_madness.is_bastia_page, name="is_bastia_page",
                 then=[
                     go_from_this_is_bastia_page_to_random_dsed_page,
                     match_page(
                         branches=[
                             when(check_that_dsed_result.is_bsod_page,
                                  name="is_bsod_page", then=[bsod_dead_end]),
                             when(check_that_dsed_result.is_ids_bypassed_page,
                                  name="is_ids_bypassed_page",
                                  then=go_from_ids_bypassed_page_to_homepage),
                         ],
                     ),
                 ]),
        ],
    ),
]

The difference with F#/Haskell: in result { let! x = fetch(); let! y = parse(x) }, the compiler generates the bind automatically. In Ocarina, every step wires its handlers manually — .failure() / .success() — and chain_actions / drive_page do the reduce explicitly. Same intent of sequentiality with short-circuit, but not the same mechanism.

Note: Python having neither do-notation nor computation expressions, Ocarina doesn’t implement a generalized bind. The manual fluent API (.failure() / .success() / .execute()) is the natural choice in this context: it stays readable without theoretical infrastructure, and is sufficient for a test framework’s needs.

Pure across all of ISTQB, impure across POMs#

The orchestration, scenario / suite / campaign / cycle declarations are pure and implement the formal definitions functional testers are used to (ISTQB).

POMs, meanwhile, remain present to fit what software-test automators are themselves used to, rather than trying to “shine” by imposing abstractions no one understands.

Holy Book (chapter “First feedbacks”):

And me, I’m not here for prestige. Nor for profit.
I’m here for our community.

To get there, the question was never to “shine” more than the others.
Nor is it actually a real challenge.
The question was simply: what do I really need?

6. Conclusions#

The Holy Book doesn’t say “ROP”, “monad”, “Curry-Howard" — but it applies each of these concepts. And its implicit argument is:

1. The theory has been available for 90 years (Church, 1936).
2. The e2e test industry retained nothing of it. Cypress, Playwright, Robot Framework — none does ROP, none has mypy --strict, none is formal.
3. Ocarina applies it in a tangible setting for functional testers (Python, ISTQB).

The shift Ocarina represents (see 08-ocarina-in-testing-industry.md) isn’t an invention — it’s a redistribution of mature theory toward a domain that ignored it.

That’s Graham’s posture in Beating the Averages: take a mature academic idea industry hasn’t retained, and turn it into a tangible advantage in a deliverable.

7. Rabbit hole — fragments of a journey#

… So fuck that little mouse ‘Cause I’m an Albatraoz (Whoo!)

• Algebra - Functions
• What is group theory
• The purest coding style, where bugs are near impossible
• The State monad in TypeScript, with Giuseppe Maggiore
• Maths, Python, artificial neural networks from scratch
• But what is a GPT? A visual intro to Transformers
• Writing My Own Database From Scratch