Modules that disappear at runtime

My favorite four lines in 1SubML are in the code generator, and they are all anticlimaxes. A checked coercion compiles to its inner expression. An identity witness becomes the JavaScript function id, newtype wrap and unwrap both point at that same id, and a type alias compiles to nothing at all.

ast::Expr::Coerce(e) => compile(ctx, &e.expr)?,ast::Expr::Identity(..) => js::var("id".to_string()),fn compile_newtype(ctx: &mut Context<'_>, def: &NewtypeDef) {    // Enum constructors keep runtime tags above this point.    ctx.set_binding(def.name, js::var("id".to_string()));    ctx.set_binding(def.name2, js::var("id".to_string()));}TypeAlias(..) => {}

A backend this sparse is the receipt for a checker that already did the work. Before code generation, 1SubML has verified structural subtyping, higher-rank polymorphism, existential members, and identity evidence — the JavaScript receives only the records and functions that survived the proofs.

A module is an existential record#

What earns that erasure a whole essay is which feature it swallows: modules. The project's counter example writes a module signature as a record type whose member type s hides the state representation behind the operations that use it.

alias Counter = {    type s;    new: s;    increment: (s, int) -> s;    get: s -> int;};let simple_counter = ({    new = 0;    increment = fun (n, inc) -> n + inc;    get = fun n -> n;} :> Counter);let step_counter = ({    new = {val=0; steps=0};    increment = fun ({val; steps}, inc) ->        {val=val + inc; steps=steps+1};    get = fun c -> c.val;} :> Counter);

simple_counter picks int for s; step_counter picks a record that also counts its steps. Sealing either with :> Counter checks the fields and takes the representation private, while the runtime value stays an ordinary record. No functor language, no separate module layer — an ordinary if can choose your module.

Opening the package with mod C = ctr gives the hidden type a stable local name, which is what lets count_to call C.increment on C.new without knowing what either is. It also locks a door you want locked: a state born in simple_counter cannot be handed to step_counter.increment, even though both modules satisfy Counter.

let count_to = fun (ctr: Counter, target) -> (    mod C = ctr;    let rec go = fun state ->        if C.get state >= target then C.get state        else go (C.increment (state, 1));    go C.new);mod C: Counter =    if choose_simple then simple_counter else step_counter;print count_to (C, 5);

The checker pays for the erasure#

None of this comes free — the complexity moved uphill into type comparison. 1SubML represents polymorphic structure with implicit spine constructors: free pieces become variance-annotated parameters, structurally identical skeletons share one spine, and the checker trims unused parameters before building any of it.

The same economy produces a => b, a type inhabited only by pure identity functions. Possessing such a value is evidence that the source type subtypes the target, so the checker consumes the fact and the backend emits id — or skips the call entirely when it can.

Erasure does have limits, and they are the sensible ones. The backend deletes only what existed to convince the checker.

The small backend sharpens the claim#

At commit 1a89506 the honest label is still experimental: a small standard library, acyclic imports, JavaScript as the one user-facing backend. The repository claims a worst-case polynomial type checker and, in the same guide, admits approximate exhaustiveness errors on pathological pattern trees. Whether the checker holds up in anger is nothing I can settle by reading the source.

The playground is the right closing demonstration anyway. It compiles the counter modules and their typed evaluator into a JavaScript string and then runs eval(compiled) — and in the gap between those two calls, the signatures, coercions, aliases, and witnesses have already done their work and vanished.