03.07 — Discriminated unions + TypeGuard + @final = “sealed” unions#

The combo that makes Result[T] and TestResult both typed and usable without casts.

Discriminated union#

@final
@dataclass(frozen=True)
class Ok[T](_BaseResult):
    value: T
    error: None = None

@final
@dataclass(frozen=True)
class Fail(_BaseResult):
    error: Exception = field(default_factory=lambda: Exception("Unknown error"))

type Result[T] = Ok[T] | Fail

• Two constructors: Ok[T] and Fail.
• Discriminant is the isinstance check (not a field like tag: Literal["ok", "fail"]).
• Both are @final — no possible subtype. The union is exhaustive, i.e. “sealed”.

Narrowing, TypeGuard#

def is_ok[T](result: Result[T]) -> TypeGuard[Ok[T]]:
    return isinstance(result, Ok)

def is_fail[T](result: Result[T]) -> TypeGuard[Fail]:
    return isinstance(result, Fail)

def handle_result(result: Result[int]) -> str:
    if is_ok(result):
        return f"Got: {result.value}"          # mypy: result is Ok[int], so .value exists
    if is_fail(result):
        return f"Error: {result.error}"        # mypy: result is Fail, so .error exists
    # mypy can detect this branch is unreachable (exhaustiveness)

_BaseResult#

class _BaseResult:
    error: Exception | None

This base lets you access result.error without narrowing:

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.

12.15 — Typing, ISTQB, Reinforcement Learning, probes: why AI works in Ocarina#

Why so much obsession over strict typing, formalizing every interface, alignment on ISTQB, refusing to execute an assertion without having observed? The mechanism is borrowed from Reinforcement Learning: an agent only progresses under constraint + reward signal.

1. A naked LLM is just a bad collaborator#

An LLM without a structured environment is:

• Optimistic — it assumes its code works.
• Persuasive — its output is convincing even when wrong.
• Memoryless — it forgets conventions between sessions.
• Feedbackless — it has no way to know it was wrong.
• Loves what it deems “most likely” — it drifts toward popular patterns, not correct ones.

Without an environment, an LLM is an over-confident junior dev producing code that looks right, breaks in prod, and learns nothing from the failure.