v6 Types: static guarantees for a dynamic VM

Explain structural type contracts and their deliberate limits.
Classify lexical arrow syntax separately from type checking.
Predict accepted programs that still need runtime checks.

1 / 6

Readiness

Pass the v5 integration gate and distinguish runtime values from static facts.

2 / 6

Worked reconstruction

fn head(xs: array<number>) -> number { return xs[0]; }
let value=head([4,5]);

The lexer emits ordinary identifier tokens for number and array, punctuation for :/</>, and one ARROW token for ->. The parser builds a function type with one array parameter and number return. Analysis checks that the array argument's elements and returned indexed value fit the signature. Runtime still performs the actual index operation. Calling head([]) in a context where the array type is known is statically meaningful but fails bounds at runtime.

3 / 6

Diagnose before implementing

A learner says “analysis passed, so head([]) cannot fail” and changes the VM to omit bounds checks. What property did type checking establish, and what property did it not establish?

4 / 6

Independent transfer

Compare let x:number=nil;, let x:number=true;, and a function returning number with an empty body. Predict analysis and runtime obligations separately. Then tokenize fn()->number and x - > y to test adjacency.

5 / 6

Carry forward

Carry precise type shapes and a limits table into v6 parsing. Keep accepted-but-runtime-failing examples alongside newly rejected examples so static guarantees are neither understated nor overstated.

6 / 6