Module typing
Description
Pure, identity-parametric typing rules for residual expressions.
The rules in this module know dimensions, scalar/tensor shape, and spatial
support, but nothing about source spans, graph paths, syntax, or storage.
Compilers and semantic validators supply their own identity type and map a
TypeViolation to the diagnostic location owned by their layer.
Structs§
- Expression
Type - Complete static type of one residual-expression value.
- Typed
Residual - One fully inferred residual DAG.
Enums§
- Root
Contract - Meaning assigned to the roots of one typed expression DAG.
- Spatial
Support - Exact spatial support carried by an expression value.
- Type
Violation - Pure typing failure, retaining identities without choosing diagnostics.
- Typed
Residual Error - One local failure while inferring a
TypedResidual.
Functions§
- additive
- Add or subtract two typed expressions.
- coordinate
- Type one Cartesian coordinate in the Relation scope.
- divergence
- Type a physical-space divergence.
- divide
- Divide by one typed scalar expression.
- gradient
- Type a physical-space gradient.
- isotropic_
lift - Type an isotropic lift whose tensor extent comes solely from volume support.
- multiply
- Multiply two typed expressions using scalar-times-tensor v0 semantics.
- normal
- Type an outward-normal contraction.
- power
- Raise one scalar expression to an integer power.
- residual
- Check one residual root against its Relation scope.
- scalar_
root - Check one activation root, which must remain an invariant scalar.
- sine
- Type a sine application.
- symmetric_
part - Type the symmetric part of an exact square Cartesian tensor.
- time_
derivative - Divide a dimension by time for a Field derivative.
- trace
- Type a boundary trace.