Type Systems for Software Developers: One Tool, Four Ways

This is a point-in-time note to get up to speed — not on proofs, on types. The question is narrow: what does a more expressive type system buy a working programmer? The cleanest way to answer it is not a textbook but a controlled experiment we already ran.

The transform tool is one spec — a reversible codec pipeline, where the URL is the sole source of truth (reversible pipeline transforms). It has been rebuilt from that one spec four times, each in a language with a different type discipline:

All four pass the same acceptance tests against the same spec. They differ only in how much of the codec's structure they can state before the program runs. That difference is the whole subject.

The thesis in one line: the algebraic shape of a transform — whether it is an involution, a bijection, a parameterized family, or a lossy surjection — is a type, and each language lets you lift more of that shape out of runtime data and into the static type (Pierce 2002).

The spec sorts every codec into one of four patterns. Stated informally:

• Involution — f(f(x)) = x. Encoding and decoding are the same function (rot13, reverse, xor:k). Direction is irrelevant.
• Bijection — decode(encode(x)) = x, but encode ≠ decode (base64, caesar:n). Direction matters; the inverse exists.
• Parameterized — a factory make(args, direction) produces the codec (caesar:13, xor:42). The arguments are part of the identity.
• Surjection — information-destroying. No inverse (upper, strip). You can go forward but not back.

This is not documentation prose; it is a sum type. Rust writes it down directly:

pub enum CodecPattern {
    /// `f(f(x)) = x`.  Direction irrelevant.
    Involution,
    /// `decode(encode(x)) = x`, `encode ≠ decode`.
    Bijection,
    /// Factory receives `(args, direction)` → codec function.
    Parameterized,
    /// Information-destroying.  No true inverse.
    Surjection,
}

Once the taxonomy is a type, the compiler can hold you to it. The interesting move is what each language does with the surjection case — the one codec family that has no inverse — because that is where "can I reverse this?" stops being a comment and becomes a thing the type system can enforce, or fail to.

The TypeScript build types the pipeline with structural interfaces. Direction is a union; reversibility is a field:

export type Direction = "encode" | "decode";
export type ApplyDirection = "apply"; // for involutions and surjections

export interface TraceEntry {
  stepIndex: number;
  // ...
  success: boolean;
  reversible: boolean;          // <- runtime data, not a type
}

export interface PipelineResult {
  isReversible: boolean;
  firstIrreversibleStep?: number;  // <- discovered by running
}

Read the last two fields carefully. reversible and firstIrreversibleStep are results the program computes by executing the pipeline. The type PipelineResult cannot prevent you from building a pipeline that loses information; it can only report, afterward, that you did. The union "encode" | "decode" is real and useful — it rules out a misspelled direction at compile time, and the IDE autocompletes it — but the deeper invariant, "this chain round-trips," lives in a boolean.

This is the floor, and it is not nothing. Structural types are erasable (they vanish at runtime), cheap, and catch the large class of shape errors — wrong field, wrong arity, wrong direction string. What they do not catch is the property the whole tool is about. For that you need to say more.

Rust lifts the surjection case into the type. The registry entry stores encode and decode as optional functions:

pub type CodecFn =
    Box<dyn Fn(String) -> Result<String, TransformError> + Send + Sync>;

pub struct Codec {
    pub pattern: CodecPattern,
    pub has_inverse: bool,
    pub encode: Option<CodecFn>,
    pub decode: Option<CodecFn>,   // None for surjections
    pub make_fn: Option<MakeFn>,   // Some only for parameterized
}

Two type-system facts are doing work here that the TypeScript version cannot.

First, decode: Option<CodecFn> makes "this codec has no inverse" a value of a type, not a boolean flag. A surjection's decode is None. The pipeline runner must pattern-match the Option before it can call decode — the compiler will not let it forget. "Partial" is in the signature.

Second, CodecFn returns Result<String, TransformError>, not String. Failure is in the type. There is "no .unwrap() in library code" (the repo's own rule), which means the type system tracks every way a codec can fail and forces a caller to handle it. The Send + Sync bounds then make the codec map safe to share across threads — again, enforced, not hoped for.

Affine typing (each owned String has one owner, moved not aliased) is the substrate that makes the boxed closures sound. The developer payoff is concrete: the class of bug "we called decode on something that has no decode" is not a test you have to remember to write — it is a program that does not compile.

Rust can say a decode may be absent. It cannot say decode is the inverse of encode. Dafny can, because in a refinement type the law is part of the type (Jhala and Vazou 2021). The involution pattern becomes a predicate:

type String = seq<char>
type Fn = String -> String

datatype Involution = Involution(id: string, label: string, fn: Fn)

// The core algebraic property every involution must satisfy.
predicate IsInvolution(inv: Involution)
{
  forall x: String :: inv.fn(inv.fn(x)) == x
}

forall x :: inv.fn(inv.fn(x)) == x is the definition of involution, written as code the verifier checks for all inputs, not the few in a test suite. The bijection round-trip decode(encode(x)) == x becomes an ensures clause the prover must discharge.

The second, less obvious payoff is what happens when the type cannot be stated. The Dafny port is littered with markers like [SG-1], [SG-2] — "spec gaps." The character model is undefined (Unicode scalar or UTF-16 code unit?); several codecs have unstated domain preconditions (base64:d requires valid base64). The repository's discipline is explicit: "Where the spec is insufficiently precise to state a formal property, we file GitHub issues rather than write unprovable theorems." A refinement type system does not just verify what is true — it forces the imprecisions in your spec to the surface, because you cannot write the type until you resolve them. That is a design tool, not just a verification tool.

Dafny moves the law to compile time and pays in proof effort. Racket keeps the law but checks it at runtime — at the module boundary — and adds the one thing none of the others give you: blame (Findler and Felleisen 2002).

The motivating bug is real. In an earlier ClojureScript build, caesar:3:d shifted forward instead of backward. The symptom was "wrong output" — a failing end-to-end test that tells you something is wrong, somewhere. With a boundary contract, the symptom is instead:

caesar/decode: contract violation
  blame: codec 'caesar' (decode direction)
  expected: decode(encode(x)) = x
  given: a function that shifts forward instead of backward

The contract states decode(encode(x)) = x once, at the boundary of the codec module. The pipeline runner needs to know nothing about reversibility; the contract enforces it and, when it breaks, names the culprit — the codec, the direction, the violated property. This is Findler and Felleisen's insight: put the specification at the module boundary, not in the test suite, and let the runtime assign blame to the party that broke it.

For a developer the trade against Dafny is legible. Dafny: the law cannot be violated, but you pay the prover. Racket: the law can be violated, but the instant it is, you get a precise accusation instead of a debugging session.

There is a limit case to this progression. In a dependently typed language — Lean 4, Idris (Brady 2017) — types are expressive enough that they are proofs: decode(encode(x)) = x is not a contract or an ensures clause but a proposition you inhabit with a term, propositions-as-types (Wadler 2015). The boundary between "type that constrains" and "proof that obligates" disappears.

That side is its own subject and its own tutorial — see jwalsh/lean4-workshop, and the structured-proof pedagogy of Macbeth's Mechanics of Proof (Macbeth 2024) and the Lean companion to Tao's Analysis I (Tao 2022). The blueprint methodology behind large formalizations ((Buzzard and The FLT contributors 2024)) is, to a developer's eye, just a dependency graph over obligations — a build system for proofs. This note stops at the doorway on purpose: the developer payoff from types arrives well before you reach full dependent types, and most of it is collected in the four implementations above.

The progression TypeScript → Rust → Dafny → Lean is a progression in power, not a recommendation to always climb. Each step up costs: proof effort, compile times, a smaller hiring pool, a steeper on-ramp. The companion lab aygp-dr/petclinic-lab exists to measure exactly this — "the cost of over-formalization," running the same domain through TLA+, Lean 4, core.logic, and more, deliberately too wide, with a refutation log per artifact.

The engineering rule that falls out: pick the weakest type discipline that makes the bug you actually fear unrepresentable. If the fear is "wrong direction string," a union type pays for itself. If it is "we shipped a codec that cannot round-trip," you want Option in the signature (Rust) or a contract at the boundary (Racket). Only if the fear is "the inverse is subtly wrong for some inputs we will never test" do you pay for refinement or dependent types. The transform tool is small enough to show all four answers to the same question, side by side, which is the whole reason it makes a good ruler.

For a developer getting up to speed, in rough order of leverage-per-page:

• Types — Pierce, Types and Programming Languages (Pierce 2002) is the spine; read for the vocabulary (soundness, progress, preservation, structural vs nominal).
• Contracts and blame — Findler & Felleisen (Findler and Felleisen 2002); short, and directly the design of the Racket port.
• Refinement types — Jhala & Vazou (Jhala and Vazou 2021) for the FP-side framing of what Dafny's requires~/~ensures are doing.
• Dependent types, for programmers — Brady, Type-Driven Development with Idris (Brady 2017); the closest existing book to "this note, but a whole course."
• Why types can be specs — Wadler, Propositions as Types (Wadler 2015); the one-sitting essay that ties it together.
• The proof end of the spectrum — Macbeth's Mechanics of Proof (Macbeth 2024), Tao's Analysis I (Tao 2022) and its Lean companion, the FLT blueprint (Buzzard and The FLT contributors 2024), and Quanta's The Proof in the Code (Hartnett 2026) for the popular framing.

The four repositories — transform-tool (TS), transform-tool-rs (Rust), transform-tool-dafny (Dafny), transform-tool-racket (Racket) — are the lab. Read any two of them against the same spec.org and the trade-off reads itself off the diff.