Equality, subtyping, and static guarantees
tulam uses strict checking: a compiled artifact must pass every required lexical, naming, type, universe, positivity, termination, coverage, coherence, effect, representation, class, target, and backend-reachability check.
Bidirectional checking
Some expressions synthesize a type; others are checked against an expected type. Expected types guide literals, constructors, existentials, higher-order arguments, and evidence selection.
value answer : Int = 42;The annotation gives the literal its checking direction. It remains a checked claim, not a conversion.
Definitional equality
Types are compared modulo permitted terminating computation and capture-avoiding substitution. Distinct opaque definitions are not unfolded merely because their implementations happen to match.
Universe cumulativity supplies directed lifting. It does not make every universe definitionally identical.
Propositional equality
=== forms a proposition in law expressions. A declared law is well typed, but declaration alone does not construct Refl or license optimizer rewriting. Proof, test, trust, and compiler-validation status are separate concerns.
Subtyping
Nominal class inheritance introduces subtyping. If Dog <: Animal, accepting a Dog where Animal is required elaborates an explicit upcast coercion. This coercion is preserved in dependent substitution.
Subtyping is not type equality. Downcasts are checked operations returning an optional result.
Structural compatibility
Open records use row constraints rather than nominal inheritance. Algebra satisfaction uses evidence rather than record shape. These relations should not be conflated simply because each can permit reuse.
Program analyses
- Positivity protects inductive definitions.
- Required termination protects type-level normalization.
- Coverage ensures closed matches handle every case.
- Coherence rejects ambiguous implicit evidence or representation defaults.
- Effect rows prevent undeclared capabilities from disappearing.
Diagnostics identify the responsible stage and stable code. Parser success is only the first step.
Implementation gaps are not alternate rules
A normatively valid program may be catalogued XFAIL at a named stage. That is an implementation gap, not evidence that the program is invalid or that a transitional syntax should enter the guide.
Common mistakes
Parser acceptance is not program validity. Keep definitional equality, subtyping, structural rows, and evidence satisfaction distinct, and do not turn a current backend failure into a new source-language restriction.
Recap
Strict compilation combines local type checking with whole-program guarantees such as positivity, termination where required, coverage, coherence, and effect closure. Diagnostics identify which contract failed.
Normative details: Language Reference §19.