Types as constraints — interactive demo

When we refine Any → string → Email → VerifiedEmail, we do not primarily add information. We forbid interpretations. That forbidding is the interesting part — for programming languages, and for any system that claims to “know” something about the world.

Interactive · Type refinement

What does this type forbid?

Current typeAny

Precision

Almost nothing is ruled out. Meaning is unconstrained.

Still allowed

42
"hello"
null
{ x: 1 }
() => {}

Forbidden

Nothing yet

Drag the dial. Refinement is mostly subtraction — each step deletes interpretations.

A judgment $\Gamma \vdash t : A$ says that under assumptions $\Gamma$ , term $t$ inhabits type $A$ . Refinement tightens $A$ :

\texttt{Any} \supset \texttt{string} \supset \texttt{Email} \supset \texttt{VerifiedEmail}

Each step deletes interpretations. That is the epistemic content of a type.

This page is a layout probe: GIF cards on the index, an embedded client widget, and KaTeX in the same reading flow. Replace the dummy copy with a real essay when ready.