Instrumented dynamics

Kennedy argues (WMM 2008) that instrumenting runtime values with their units is "cheating", on the grounds that it makes type soundness trivial. That objection has force for F#, which erases units, so an instrumented semantics would not model the language he shipped.

It does not have force for a core calculus, and the reason is worth stating. Runtime units alone would merely relocate the checking to the runtime. But paired with a theorem that erasure preserves results, they establish something the erased semantics cannot state on its own: that the instrumentation is unnecessary. That is precisely the content of "units are static", a slogan easy to assert and, before these files, unproved.

So there are three things, and they are complementary rather than competing:

	proves
instrumented dynamics + unit_soundness_total	the dynamic unit checks never fire on well-typed terms
eeval_erase (LambdaS.Erasure)	dropping units does not change the numbers
scaling parametricity, i.e. invariance of results under a change of units (LambdaS.Fundamental)	units have observable meaning

Kennedy did the third column. This file defines the instrumented evaluator; its soundness lives in LambdaS.Soundness and LambdaS.Normalization, and erasure in LambdaS.Erasure; all three are stated at the whole language.

structure LambdaS.Meas (R B : Type) : Type

A runtime measurement: a magnitude together with the unit it is measured in. This is the OOPSLA'04 notion of a measurement as a value.

• mag : R
• unit : UExp B 0

Environments

Evaluation has three environments, and they are the same idea three times over: a value for each value variable, a ground unit for each unit variable, and a ground dimension for each dimension variable.

Units are looked up, never substituted. Substituting a unit into a term during evaluation would be compile-time work done at runtime, and it would also force the evaluator to live only at the closed scope: a term under a unit binder could not be evaluated at all without first eliminating the binder. With an environment, eval is defined at every scope, which is what makes the ordinary induction principles apply to it.

@[reducible, inline]

abbrev LambdaS.UEnv (B : Type) (k : ℕ) : Type

A ground unit for each unit variable in scope.

Equations

• LambdaS.UEnv B k = (Fin k → LambdaS.UExp B 0)

@[reducible, inline]

abbrev LambdaS.DEnv (D : Type) (j : ℕ) : Type

A ground dimension for each dimension variable in scope.

Equations

• LambdaS.DEnv D j = (Fin j → LambdaS.DExp D 0)

inductive LambdaS.Val (R B D : Type) : Type

A runtime value: a measurement, a vector over a space, a linear map between spaces, or a closure.

Vectors and matrices carry their spaces, not a unit per entry. That is not an optimization: LambdaS.Map proves the units of a linear map are rank-one, entry (j,i) carrying δ_W(j)/δ_V(i), so an n×m map needs n+m units rather than nm. After type checking the numeric payload is a plain array, which is what makes a BLAS kernel usable underneath without any per-entry tagging.

Closures package the scope they were built at, along with all three environments, so a value is always ground even when the term it came from was not.

• scalar {R B D : Type} : Meas R B → Val R B D
• vector {R B D : Type} : List R → Sp B 0 → Val R B D
• matrix {R B D : Type} : List (List R) → Sp B 0 → Sp B 0 → Val R B D
• closure {R B D : Type} {j k : ℕ} : Ty B D j k → Tm B D j k → List (Val R B D) → UEnv B k → DEnv D j → Val R B D
• uclos {R B D : Type} {j k : ℕ} : DExp D j → Tm B D j (k + 1) → List (Val R B D) → UEnv B k → DEnv D j → Val R B D
• dclos {R B D : Type} {j k : ℕ} : Tm B D (j + 1) k → List (Val R B D) → UEnv B k → DEnv D j → Val R B D

def LambdaS.dotp {R : Type} [Num R] (a b : List R) : R

The dot product an application of a linear map performs.

Forwards to Num.dot, which the Float carrier overrides with the native kernel, so this is the point where a compiled Λs program crosses into C.

Equations

• LambdaS.dotp a b = LambdaS.Num.dot a b

def LambdaS.colOf {R : Type} [Num R] (N : List (List R)) (i : ℕ) : List R

Column i of a matrix, padded with zero.

Equations

• LambdaS.colOf N i = List.map (fun (r : List R) => r[i]?.getD (LambdaS.Num.ofRat 0)) N

@[irreducible]

def LambdaS.eval {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {R : Type} [Num R] (cf : UExp B 0 → UExp B 0 → R) : ℕ → (j k : ℕ) → UEnv B k → DEnv D j → List (Val R B D) → Tm B D j k → Option (Val R B D)

Instrumented evaluation. Values carry their units, and the evaluator is partial: adding mismatched units, taking log of a dimensioned quantity, and applying a linear map to a vector of the wrong space all get stuck.

Those stuck states are the whole point. unit_soundness_total says they are unreachable from a well-typed term.

Fuel is consumed only where a closure body is entered, which is the only place the recursion leaves the term. Nothing else spends it, so first-order arithmetic evaluates at every bound including zero.

Data may arrive through the environment or be built by the introduction forms: vnil/vcons assemble a vector value one scalar at a time, and mnil/mcons assemble a matrix one row at a time, with mnil grounding its annotated column space so even a rowless matrix value knows its width. Like the other introduction forms (mul building a product unit, lam building a closure), they check nothing: the dynamic unit checks live at the eliminations, where a mismatch would corrupt the arithmetic. A literal whose scalars name units via ucon sits outside the invariance theory for exactly the reason LambdaS.Fundamental gives about unit constants.

Equations

• One or more equations did not get rendered due to their size.
• LambdaS.eval cf x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ (LambdaS.Tm.var n) = x✝[n]?
• LambdaS.eval cf x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ (LambdaS.Tm.lam τ b) = some (LambdaS.Val.closure τ b x✝ x✝² x✝¹)
• LambdaS.eval cf x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ (LambdaS.Tm.ulam d b) = some (LambdaS.Val.uclos d b x✝ x✝² x✝¹)
• LambdaS.eval cf x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ b.dlam = some (LambdaS.Val.dclos b x✝ x✝² x✝¹)
• LambdaS.eval cf 0 x✝⁴ x✝³ x✝² x✝¹ x✝ (a.app a_1) = none
• LambdaS.eval cf 0 x✝⁴ x✝³ x✝² x✝¹ x✝ (a.uapp a_1) = none
• LambdaS.eval cf 0 x✝⁴ x✝³ x✝² x✝¹ x✝ (a.dapp a_1) = none
• LambdaS.eval cf x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ (LambdaS.Tm.lit q) = some (LambdaS.Val.scalar { mag := LambdaS.Num.ofRat q, unit := 1 })
• LambdaS.eval cf x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ (LambdaS.Tm.ucon u) = some (LambdaS.Val.scalar { mag := LambdaS.Num.ofRat 1, unit := LambdaS.substU x✝² u })
• LambdaS.eval cf x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ LambdaS.Tm.vnil = some (LambdaS.Val.vector [] [])
• LambdaS.eval cf x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ (LambdaS.Tm.mnil V) = some (LambdaS.Val.matrix [] (List.map (LambdaS.substU x✝²) V) [])

@[reducible, inline]

abbrev LambdaS.evalC {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {R : Type} [Num R] (cf : UExp B 0 → UExp B 0 → R) (n : ℕ) (ρ : List (Val R B D)) (e : Tm B D 0 0) : Option (Val R B D)

Evaluation of a closed term, with all three environments empty.

Equations

• LambdaS.evalC cf n ρ e = LambdaS.eval cf n 0 0 (LambdaS.nilU B) (LambdaS.nilU D) ρ e

The I/O boundary: measurements whose unit arrives at runtime

A measurement read from a file carries a unit name, resolved against the declared system to a UExp B 0. What arrives is a Meas, and using it in typed code means committing to a unit: a checked cast.

That cast is the whole content of a dimension-typed value ∃u:d. Q u, and it is deliberately not a type former. At runtime such a value is the pair (magnitude, factor): the magnitude, and the dictionary a bounded quantifier would have been instantiated with. Once the unit name is resolved that pair is exactly a Meas. Keeping it here rather than in Ty leaves every type in Λs erasable, and confines the trust to one partial function, whose partiality is the trust boundary, since nothing checks that a name off a disk denotes a declared unit.

noncomputable def LambdaS.asUnit {B D : Type} [Fintype B] [Fintype D] [DecidableEq D] [UnitSys B D] (Δ : DCtx D 0 0) (ψ : Scaling B 0) (x : Meas ℝ B) (μ : UExp B 0) : Option ℝ

The checked cast. Read a measurement at a demanded unit: convert if the dimensions agree, fail if they do not.

Option rather than a runtime error, so the boundary is visible in the type.

Equations

• LambdaS.asUnit Δ ψ x μ = if LambdaS.SameDim Δ x.unit μ then some (x.mag * LambdaS.conv ψ x.unit μ) else none

theorem LambdaS.asUnit_preserves {B D : Type} [Fintype B] [Fintype D] [DecidableEq D] [UnitSys B D] {Δ : DCtx D 0 0} {ψ : Scaling B 0} {x : Meas ℝ B} {μ : UExp B 0} {m : ℝ} (h : asUnit Δ ψ x μ = some m) : ψ.scale μ * m = ψ.scale x.unit * x.mag

The cast preserves the quantity. When it succeeds, the number it returns denotes the same physical quantity read in the demanded unit.

This is what makes the boundary safe on the inside: everything past asUnit is ordinary typed code with a correct magnitude.

theorem LambdaS.asUnit_eq_none {B D : Type} [Fintype B] [Fintype D] [DecidableEq D] [UnitSys B D] {Δ : DCtx D 0 0} {ψ : Scaling B 0} {x : Meas ℝ B} {μ : UExp B 0} (h : ¬SameDim Δ x.unit μ) : asUnit Δ ψ x μ = none

The cast rejects a dimension mismatch. Reading a duration as a length fails rather than silently scaling: the Mars Climate Orbiter failure at the one place in Λs where it could still occur.

theorem LambdaS.asUnit_eq_eval_convert {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {Δ : DCtx D 0 0} {ψ : Scaling B 0} {a : Tm B D 0 0} {x : Meas ℝ B} {v : UExp B 0} {fuel : ℕ} (ha : evalC (conv ψ) fuel [] a = some (Val.scalar x)) (hΔ : Δ = DCtx.nil D) : evalC (conv ψ) fuel [] (a.convert x.unit v) = Option.map (fun (m : ℝ) => Val.scalar { mag := m, unit := v }) (asUnit Δ ψ x v)

The cast agrees with the calculus: casting to μ is what convert computes, so the boundary operation is not a second, unverified conversion path.

What has to be passed at runtime

The target unit μ of a cast is itself often read from I/O, so it too is a runtime value, which raises the question of what a compiler actually has to carry. The answer splits cleanly in two, and the split is the difference between the dimension check and the arithmetic.

The arithmetic needs only the factor. Past the dimension check the unit expression is not observable: the cast is computed from the magnitude and ψ.scale, so two measurements with the same magnitude and the same scale factor cast identically whatever units they name. That pair (magnitude and factor) is exactly the dictionary a bounded quantifier is instantiated with, which is why ∃u:d. Q u needs no type former to be implementable.

The check needs the unit itself. SameDim is a statement about exponent vectors and cannot be recovered from a single real number: two units of different dimensions can share a scale factor. So a runtime unit must be carried as data up to the check, and may be discarded after it.

noncomputable def LambdaS.Meas.dict {B : Type} [Fintype B] (ψ : Scaling B 0) (x : Meas ℝ B) : ℝ × ℝ

The runtime dictionary of a measurement: its magnitude and the scale factor of its unit. This is what a compiler passes when instantiating a bounded unit quantifier at a unit known only at runtime.

Equations

• LambdaS.Meas.dict ψ x = (x.mag, ψ.scale x.unit)

theorem LambdaS.asUnit_eq_dict {B D : Type} [Fintype B] [Fintype D] [DecidableEq D] [UnitSys B D] {Δ : DCtx D 0 0} {ψ : Scaling B 0} {x : Meas ℝ B} {μ : UExp B 0} (h : SameDim Δ x.unit μ) : asUnit Δ ψ x μ = some ((Meas.dict ψ x).1 * (Meas.dict ψ x).2 / ψ.scale μ)

The cast is computed from the dictionary. Once the dimension check has passed the unit expression plays no further part: the answer is the magnitude times its own factor over the target's.

theorem LambdaS.asUnit_dict_determined {B D : Type} [Fintype B] [Fintype D] [DecidableEq D] [UnitSys B D] {Δ : DCtx D 0 0} {ψ : Scaling B 0} {x y : Meas ℝ B} {μ : UExp B 0} (hd : Meas.dict ψ x = Meas.dict ψ y) (hx : SameDim Δ x.unit μ) (hy : SameDim Δ y.unit μ) : asUnit Δ ψ x μ = asUnit Δ ψ y μ

The dictionary determines the answer. Two measurements agreeing on magnitude and scale factor cast to the same number, whatever units they name.

This is the precise sense in which the unit need not survive past the check; and, read the other way, the precise sense in which it must survive up to it, since SameDim is not a function of the scale factor.