v6 Types: static guarantees for a dynamic VM

v6 adds a front-end type system while retaining the dynamic VM. It can reject many invalid operands and calls earlier, but it is not a proof that accepted programs cannot fail. This checker has no all-path return analysis, nil-safety proof, bounds proof, or flow-sensitive narrowing.

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.

Type shapes and assignability

Types are number, bool, string, nil, array, map<K,V>, and fn(P1,...)->R. Match non-nil types structurally; an array's element type and both a map's key/value types matter. There is no generic type-variable inference or function variance rule. The internal unknown type helps limit cascading errors; it is not a source type spelling.

Nil is assignable to every type in this educational checker. Therefore let x:number=nil; x+1; can pass analysis and fail runtime arithmetic. A function declared to return number can fall off its body; the VM then returns nil, because the analyzer checks explicit returns but does not prove coverage. Do not promise the guarantees of a sound non-null typed language.

Inference boundaries

Local declarations can infer a type from an initializer. Function parameters and return types require explicit syntax. Exported variables require explicit annotations so a module interface is available before checking consumers. Empty collection literals need an expected collection type, supplied by an annotated declaration or typed call/return context. This implementation does not propagate a target type into a plain assignment RHS; that boundary is examined in the semantic module.

The lexer change is small but precise: -> wins over minus when adjacent, while - > remains two tokens. Do not classify every type-like word as a new keyword; number/bool/string/array/map remain identifier tokens interpreted by the type parser. nil and fn retain their existing keyword token kinds.

Debugging lab

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?

Compare your diagnosis after attempting the lab

It can establish the expected element type, not the existence of element 0. Empty arrays remain possible. The dynamic VM must retain bounds, nil, arithmetic, and actual call checks outside the checker’s guarantees.

Transfer task

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.

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.

Build program-lexer-v6. Keep a before/after trace of one failing test. Use the checkpoint to diagnose specific skills; passing it does not replace implementing and testing the artifact.