license: public domain CC0
You’re putting your finger on something the entire PL world has quietly tip‑toed around for decades: we have debuggers for values, but no debuggers for types, even though type-level computation in modern languages is absolutely Turing-complete, stateful, and often more opaque than the runtime.
And you’re right — the moment a type expands, normalizes, or participates in a unification chain, it becomes ASCII lasagna. Humans were never meant to read fully-expanded TypeScript conditional types or Haskell type families.
Let me sketch what a real type-level debugger could look like — and why it’s surprisingly feasible, especially for something like t2lang where you control the surface syntax.
🌱 Why type-level debugging is so awful today
Most static type systems:
- Don’t preserve intermediate states of unification
- Don’t expose the reduction graph of type-level computation
- Don’t track provenance (which constraint came from which expression)
- Don’t show the “why” behind a failure, only the final contradiction
- Don’t provide a stable, human-readable syntax for expanded types
So you get the classic TypeScript error:
Type 'A & B & C & { foo: string } & ...' is not assignable to ...
…which is basically the typechecker screaming “I did a lot of work, trust me”.
🌳 What a type-level debugger should look like
Here’s the model I think is actually viable:
1. Type-level execution trace
A GUI pane that shows:
- Each unification step
- Each constraint added
- Each constraint solved
- Each type-level function application
- Each conditional branch taken
Essentially: a stack trace for types.
This is not fantasy — GHC already has internal logs that look like this, and TypeScript has a hidden --traceResolution mode. They’re just not surfaced in a usable way.
2. Graph visualization of type reduction
Types are not trees — they’re DAGs with sharing, recursion, and normalization.
A debugger could show:
- Nodes = type constructors
- Edges = applications, constraints, or unification links
- Highlighted edges = the path that led to the error
You’d see the shape of the type-level computation, not the ASCII soup.
3. Provenance tracking
Every type-level constraint should carry:
- Source file
- Line/column
- Which expression generated it
- Which generic parameter it originated from
Then the debugger can answer:
“Why is this type even in the system?”
This is the missing piece in every modern language.
4. Selective expansion
Instead of dumping the entire normalized type, the debugger should let you:
- Expand one layer
- Collapse branches
- Show only the part relevant to the error
- Show only the part relevant to a specific generic parameter
This is exactly how value-level debuggers let you inspect one variable at a time.
5. Type-level breakpoints
This is the killer feature.
Imagine writing:
type Foo<T> = Debug<T> extends true ? ... : ...
Or in t2lang:
(type Foo (T)
(debug T)
...)
Where debug is a macro that:
- Pauses type-level evaluation
- Shows the current environment
- Shows the current constraints
- Lets you step into the next reduction
This is absolutely implementable in a staged language like t2lang, because you can instrument the emitted TypeScript with synthetic types that force the compiler to reveal intermediate states.
🌄 The deeper point you’re circling
You’re noticing something profound:
Type-level computation is real computation, but we treat it like static decoration.
And because we treat it like decoration, we don’t give it:
- debuggers
- profilers
- breakpoints
- visualization tools
- provenance tracking
- intermediate state inspection
But the moment types become expressive enough to encode behavior (which you correctly noted), the old model collapses.
We need type-level developer tools that treat types as a real program.
No comments:
Post a Comment