intertwingly

Most type systems force a bet. Programmers pay in annotations; compilers pay in inference effort; the language designer picks where to set the dial. Today Roundhouse declined to set it.

The Goldilocks Zone

Hindley-Milner — the algorithm behind ML, OCaml, and Haskell's core — is the gold standard for principal-type inference. Within its expressible subset (parametric polymorphism, no subtyping, no unions), it produces a most-general type for every expression with no annotations and a guarantee of termination. That's the Goldilocks zone.

Step outside it and the floor drops. Subtyping, intersections, higher-rank polymorphism — all push inference into undecidable territory. You can have more expressive or you can have fully inferred; the literature has spent forty years showing you mostly can't have both.

Real languages settle. Rust demands type signatures on function parameters — annotations are the price of staying tractable past HM. TypeScript and Python infer locally and lean on annotations at boundaries. Crystal runs whole-program propagation that's theoretically undecidable but terminates fast enough on real code, and the user pays the bill in compile time. Each language picked a point.

The decision

Today Roundhouse landed Ty::Untyped as a first-class type — not an error state, not a sentinel, not a metavariable. A type the analyzer can assign and every downstream stage can consume.

The idea isn't novel. RBS, Ruby's official type-signature language, has untyped as the gradual escape. TypeScript's any does the same job. Sorbet calls it T.untyped. Hack distinguishes dynamic from mixed, and that split matches one we made independently. We're not inventing the gradual hatch; we're making it the IR's load-bearing primitive instead of a user annotation.

What's distinctive is what the IR can do once Untyped is first-class. The analyzer always succeeds — if it can't pin a type, it produces Untyped and the program is well-typed by definition. The Goldilocks question ("did inference find a principal type?") gets replaced by a measurement ("how much of the program is concrete versus Untyped versus inference-gap, and is that mix acceptable for this target?").

Var versus Untyped

Two unknowns are not the same unknown.

Ty::Untyped is author-signed: someone — the user via RBS sidecar, the framework runtime via its own annotations — declared the type unknown. It propagates through expressions the way TypeScript's any does. It's a choice, not a failure.

Ty::Var is the inference gap: the analyzer couldn't pin a type, full stop. It's either a bug in the inferencer or evidence of a Ruby pattern the analyzer hasn't learned to read. Var should drive toward zero; that's what "the inferencer got better" means.

Most gradual-typing systems collapse the two. Roundhouse splits them. The split makes inference progress measurable — every closed Var is the inferencer learning; every Untyped site is bounded by what got authored. A test in CI today asserts zero Var in the framework runtime. A second test counts Untyped sites and tightens its ceiling as the runtime gets sharper. Neither test could exist if the two were one type.

Four axes deferred

Once Untyped is first-class, "how strict should the compiler be?" has multiple answers, not one. We declined to pick:

• Code category. The framework runtime is roundhouse-authored; it can be held to a stricter bar than user-authored Rails app code. Same compiler, different expectations.
• Target language. Rust requires interface-level commitment — you can't ship a struct field of type any. TypeScript propagates any cheaply. Elixir is gradual at runtime. The same Untyped value has different downstream costs depending on which emitter consumes it.
• Pipeline stage. Ingest, lower, type, emit each know different things. Diagnostics can be tagged with stage-of-origin and provenance, and downstream stages can promote or demote them.
• User configuration. A flag like TypeScript's strict or a per-file pragma like Sorbet's # typed: is design space we left open. Probably a small set of named presets rather than dozens of knobs, when we get there.

None of these is settled. All of them are available because the IR carries Untyped instead of treating "I don't know" as a compile error.

Why this is coherent for us

Most gradual-hatch designs put the hatch in the source language — the user writes T.untyped or : any. Roundhouse puts it in the intermediate representation between Ruby in and target out. That's a transpiler-shaped repurposing of an idea that's mostly lived in type checkers.

It works because we author both ends. The framework runtime is roundhouse-written Ruby; we can rewrite a method to be more typeable when that's cheaper than teaching the inferencer. User code is inference-only by design — "no RBS required" is the external promise. We can demand strictness from ourselves; we only guide users. The split bet is coherent because the authors are different.

A type checker for an existing language can't do this. Sorbet can't rewrite Ruby's standard library to be more inferrable. Crystal couldn't do it without becoming a different language. Roundhouse can, because the runtime is the project's, not the user's.

The cost ladder

Where do errors land if the compiler is too lax?

• At roundhouse transpile time. Best — clear attribution to a Ruby source line.
• At target compile time (rustc, tsc with strict). Acceptable — needs a map-back to the Ruby source, but the program never runs broken.
• At target runtime (JS exception, Python TypeError, Elixir FunctionClauseError). Worst — production failure, no compile-time guarantee.

The strictness knob controls how far down this ladder issues are allowed to fall. The asymmetry matters: for some targets the downstream catches are sound (rustc, tsc) and roundhouse can be more permissive without putting users at risk. For others — vanilla JavaScript, Elixir, Python without mypy — roundhouse is the only line of defense before runtime, and it has to stay strict.

A uniform strictness bar over-protects users with strong target compilers and under-serves users emitting to weak ones. The four-axis framing is partly a correction for that. Correctness for dynamic targets was the previous post in this thread; this one is the corollary about how strict to be when the targets disagree about what they'll catch downstream.

A bet about deferring bets

Languages commit to a single position on the burden-versus-inference tradeoff because they have to ship a single experience to a single audience. A multi-target transpiler doesn't. The audiences differ, the targets differ, the code categories differ. A single bet would be the wrong shape for the problem.

Eleven days from first commit; two days to add Spinel as a seventh target. At that pace, deferring decisions is cheaper than picking wrong, and the instrumentation — Bar A and Bar B trackers, the roundhouse-check CLI, per-target compare scripts — measures the consequences continuously. When the right defaults reveal themselves, they will. Until then, the IR carries the optionality.

Ty::Untyped is the bet that defers the other bets. It says: the IR's job is to faithfully represent what's known and what isn't, and per-target rules decide what's acceptable. We don't have to pick the dial today. We may never have to pick a single dial at all.

Roundhouse is open source: dual-licensed MIT / Apache-2.0. Issues and discussion welcome.