Every judgement, drawn as a proof
FJ's type system is small enough that its checker does not just accept or reject a program — it can show you the entire derivation for any expression you build, the way a paper would print it, and it never lets one unfinished socket paint the rest of the program red.
The type checker
fjTypeChecker.ts implements FJ's typing rules directly: T-Var,
T-Field, T-Invk, T-New, and the three cast rules,
alongside class and field well-formedness and FJ's override rule. Subtyping is
nominal — class B is a subtype of A exactly when
it declares extends A, transitively, with Object at the root.
| Rule | Judges |
|---|---|
T-Var |
A variable, including this, looked up in Γ |
T-Field |
e.f — the field's declared type on e's class |
T-Invk |
e.m(ē) — the method's return type, with each argument
checked against its parameter type |
T-New |
new C(ē) — typed C, with each argument
checked against the matching field's type |
T-UCast |
An upcast — the target is a supertype of the source. Always safe. |
T-DCast |
A downcast — the target is a subtype of the source. Safe if the runtime class actually matches; a stuck cast if it doesn't. |
T-SCast |
A “stupid” cast — source and target are unrelated. Type-checks anyway, with a warning; see Problems below. |
The override rule is stricter than it might look coming from ordinary Java: FJ has no overloading and no covariant returns, so an overriding method must match the inherited signature exactly — same parameter types, same return type, in the same order. There is exactly one legal signature for a given method name once a superclass has declared it.
An empty socket types as a first-class Hole, in the style of the Hazel language.
A hole is consistent with everything, so it never cascades into the rest of the program:
finish one field and leave a method body empty, and the field still checks cleanly while the
empty method reports exactly one problem, not a wall of them. The whole workspace re-checks
on every edit, and this is what makes that tolerable rather than noisy.
The Typing tab
The FJ Inspector's Typing tab renders a genuine natural-deduction proof tree for any
expression: premises over a rule bar over a conclusion, each node showing the judgement
Γ ⊢ e : C and the rule that produced it. Every node is clickable, and
clicking one selects and centres the block it is about.
T-New
types the fresh B; T-SCast then types the cast to the unrelated
A, flagged with a warning rather than a hard failure.Loading Stupid cast and building it produces exactly this two-line derivation:
∅ ⊢ new B() : B (T-New)
------------------------------------
∅ ⊢ (A) new B() : A (T-SCast)Read bottom-up as usual: the conclusion is (A) new B() : A, justified by
T-SCast, whose single premise — new B() : B, justified by
T-New — sits above the bar. Nothing about the tree hides that this is a cast
between unrelated classes; the warning that goes with it lives in the Problems tab, not in the
derivation.
The Problems tab
The bottom dock's Problems tab surfaces the same checker's diagnostics as a clickable list, and the same offending blocks get in-canvas warning-triangle icons. Loading and building Stupid cast produces exactly one entry: “Stupid cast: (A) applied to unrelated type B always fails at run time (T-SCast).”
That entry is shown as a warning, not an error. The program still type-checks
and still runs — a stupid cast is a distinct, permitted rule in FJ's own type system, not
a type error, and the Problems tab is honest about that distinction rather than flattening every
diagnostic into red. What actually happens when you run it — a
ClassCastException, not a crash — is the subject of
Semantics § Stuck-but-safe casts.