Types constrain allowed operations; checking and inference do not execute the program.
By the end: Read local typing constraints and distinguish inference, runtime checks, and guarantees a type system does not provide.
Propagate the type requirements
In SmallExpr, numeric literals have type int and boolean literals type bool. A name gets the type of its environment binding. Each arithmetic operator requires integer operands and returns an integer. A tree walk can apply those rules from children to parents.
For x + 1, x is int, one is int, and + produces int. For flag + 1, flag is bool, so the same rule fails. We deliberately provide no boolean-to-integer conversion. A language with different coercion rules could accept similar spelling with a different meaning.
Derive a type from the children
A typing rule describes which combinations of expressions the language accepts. It does not describe a processor instruction. For SmallExpr addition, the premises are that the left expression has type int and the right expression has type int. If both premises hold, the conclusion is that their sum has type int. The same requirement applies to subtraction and multiplication. Unary minus has only one child to check. A literal or resolved name supplies a starting fact, so a finite tree can be checked from its leaves upward.
Consider x * (y - 2). The environment supplies int for x and int for y. The literal two also has type int. The subtraction therefore satisfies both premises and receives type int. That result supplies the right premise of multiplication, while x supplies its left premise. The root receives type int without calculating either subtraction or multiplication. Knowing that x is four and y is seven lets a separate evaluator return twenty, but those particular magnitudes are unnecessary for this typing derivation.
Integer premises establish the parent type
Schematic typing tree for x * (y - 2). Read premises upward. Positions encode parent–child structure, not values or execution time.
Now replace y with flag. Name resolution still succeeds because flag exists in the environment. Its type is bool, so flag - 2 fails the subtraction rule. There is no valid integer result type to pass upward to multiplication. The problem belongs to the inner subtraction even if the diagram also labels its containing expression as erroneous. An error on a parent can mean that a child prevented a derivation, rather than that the parent introduces a second independent mistake. This distinction helps you locate the first useful repair.
A bare flag is different. Reading a boolean is permitted, and the expression has type bool. No arithmetic operation demands an integer from it. Likewise, true and false are valid literal expressions. The checker rejects arithmetic on booleans, not booleans themselves. Substituting a declared integer for flag repairs flag - 2 by satisfying the missing premise. Adding parentheses around flag does not repair anything because parentheses change grouping, not the binding's type. Negating flag also fails because unary minus requires an integer child.
Use the type view to compare x * (y - 2), x * (flag - 2), and flag. Predict the label at every leaf before reading the root. For the second expression, identify the smallest subtree that cannot receive a valid type. The answer is flag - 2, whose left child conflicts with the rule. Then change the source to x * (y - true). The conflict moves to the other child of subtraction, but its explanation remains the same. Neither case requires trying different numeric values.
The subtraction cannot supply an integer premise
Schematic typing tree for x * (flag - 2). Gold outlines mark failed derivations, not execution events. flag resolves successfully as bool.
This local method works because SmallExpr operators have fixed requirements and the environment supplies known binding types. A richer language may overload addition, allow several numeric types, or require information from an expected result. Those policies change the rules and sometimes the direction of information flow. Do not infer them from familiar operator spelling. Here, accepting the tree establishes one precise fact about arithmetic operands under the supplied environment. It does not establish that the expression implements a useful calculation or that another language accepts it.
Checking and inference solve related questions
Checking asks whether an expression satisfies a required type. Inference derives a type or constraints from the program. A general inference engine may introduce unknown type variables and solve equalities or subtype constraints. Our lab has only two known types and local rules; it is not a general-purpose unification or subtyping engine.
Static checking happens without running the program on its actual inputs. Dynamic checks occur during execution. Languages can combine both. The presence or absence of annotations does not by itself tell you whether a language checks types statically, dynamically, or through a mixture.
Separate type information from computed values
Inference and evaluation can visit the same tree while returning different kinds of information. For x + 1, inference returns int; evaluation returns five in this editor's environment. The first answer classifies the expression, while the second calculates its value. If the environment instead contained another valid integer for x, the classification would stay int even when the result changed. The live editor fixes x at four, so this alternative environment is a reasoning example, not a setting you can adjust through its controls.
Checking adds a requirement against which to compare an expression. Suppose a separate interface requires an integer expression. Inference can first discover bool for flag, after which comparison rejects it at that interface. The expression flag is still valid on its own. A language can instead propagate the expected type downward during checking, which helps with constructs whose meaning depends on context. SmallExpr does not need that machinery. Its tree walk derives one of two types and enforces the fixed arithmetic requirements locally.
The same type can describe different results
Expression
Static type
Executed value
x + 1, editor x = 4
int
5
x + 1, hypothetical x = 9
int
10
flag, editor flag = true
bool
true
The second row is a paper environment, not an editor control. Types classify values; they do not specify a single value.
General inference often introduces an unknown type for something not yet determined. In a hypothetical arithmetic fragment u + 1, the operator imposes a constraint that u must be an integer. If another use requires that same u to be boolean, the requirements conflict. Solving such constraints is not running the program with sample values. SmallExpr does not invent a declaration or infer a binding for an unknown name u. Its lookup reports a binding error first. The constraint example describes a possible richer inference system, not an editor capability.
The implementation combines name lookup and typing in one recursive traversal. That engineering choice does not merge their logical questions. For absent + 1, lookup cannot supply a binding and therefore cannot supply its type. For flag + 1, lookup succeeds and supplies a type that the addition rule refuses. When explaining a diagnostic, ask whether the compiler failed to find the name or found it with an incompatible type. Renaming flag to an undeclared spelling merely changes the failure; it does not satisfy the arithmetic rule.
Static and dynamic also describe when evidence is obtained. Static checking reasons from a representation before ordinary execution. A dynamic operand check examines actual values as an instruction runs. This VM retains dynamic integer checks in its arithmetic operations even though the normal build path checks the source first. Such checks can catch malformed instruction sequences or misuse of internal functions. Their presence does not turn the source checker into an evaluator. Nor does omitting written annotations imply that a language has abandoned static checking.
Compare three editor inputs in order: absent + 1, flag + 1, and x + 1. Predict binding failure, typing failure, and successful integer compilation respectively. For the last input, keep two observations separate when the interface reports them. The type is int because the operands satisfy the rule; the returned value is five because execution reads four and adds one. A successful demonstration supplies both observations for this case. It is not evidence that type inference calculates results or that every syntactically valid name denotes an available value.
What each successful responsibility establishes
Source
Binding and typing evidence
Execution
absent + 1
No binding for absent
Not reached by build
flag + 1
flag found as bool; + requires int
Not reached by build
x + 1
x: int and 1: int imply result int
Reads 4 and returns 5
These are outcomes of this build path. A name being found is weaker evidence than its type satisfying an operator.
Work through the mechanism
Signed 32-bit wrapping
n is the mathematical integer result before wrapping. Here mod returns a remainder from zero through 2³² − 1, including for negative inputs. The stored result lies from −2³¹ through 2³¹ − 1. These are integer values, not physical units.
Thus 2,147,483,647 plus one becomes −2,147,483,648 under this contract. This is a semantic range example; individual literals that large exceed the editor’s separate 0–999 literal bound. The wrapping preset reaches overflow using smaller literals. Other languages may trap, use unbounded integers, or make some overflow undefined instead.
Follow the local type rules
Presets replace the whole source. Editing replaces the current calculation and resets any execution trace. Names: x = 4, y = 7, flag = true. Use ASCII - for subtraction and negation. Arithmetic is signed 32-bit wrapping; booleans are not numbers. See lesson 1 for the full grammar and editor bounds.
typing error at offset 0: Arithmetic requires int operands; bool is not coerced to int.
Tree with inferred local types
An error label means that subtree fails the local SmallExpr rules. A declared boolean alone is valid. The entered source is never passed to JavaScript eval or Function.
Expression
Name resolution
Type result
x + 1
x is declared as int
int
flag
flag is declared as bool
bool
flag + 1
flag is found
Type error
absent + 1
absent is undeclared
Binding error
Type constraints here belong to SmallExpr, not to JavaScript or C.
Read overflow as a semantic rule
The name int tells you which operations are permitted here, but its arithmetic meaning needs a separate specification. SmallExpr stores signed thirty-two-bit results. After each arithmetic operation, wrapping selects the signed value with the same low thirty-two bits as the mathematical result. Stored values range from negative 2,147,483,648 through positive 2,147,483,647. A type derivation does not prove that an intermediate mathematical result stays inside that interval. Wrapping defines what happens when it does not, instead of treating that event as a typing failure.
The wrapping preset uses 999 * 999 * 999 * 999 because each literal meets the editor's separate bound. Left association first gives 998,001. Multiplying that by 999 gives 997,002,999, which still fits the signed range. The next product is 996,005,996,001. Reducing it modulo 4,294,967,296 leaves 3,868,550,625. That unsigned remainder exceeds the largest signed value, so subtracting 4,294,967,296 gives negative 426,416,671. The expression remains well typed. Its negative result follows from the arithmetic contract.
Four legal literals produce a wrapped result
Operation
Mathematical integer
Stored signed int32
999 × 999
998,001
998,001
998,001 × 999
997,002,999
997,002,999
997,002,999 × 999
996,005,996,001
−426,416,671
Final product modulo 2³²
3,868,550,625
Subtract 4,294,967,296
Exact integer values, not timings. The final unsigned remainder is above 2³¹ − 1, so its signed representation is negative.
Notice the two independent limits in this example. The lexer accepts the numeric literal 999 but reports a limit error for the literal 1000. Arithmetic may nevertheless produce 1000, for example by adding 999 and one. Literal size protects the teaching interface; it is not the range of the int type. Conversely, a long multiplication made entirely of legal literals can exceed the mathematical signed range. Separating source bounds from value semantics prevents the mistaken conclusion that small input spellings guarantee small computed results.
Other integer contracts would change the same calculation. An unbounded-integer language could retain the complete mathematical product. A checked fixed-width operation could report overflow rather than wrap. Some languages permit optimizer reasoning under conditions that exclude particular overflow cases. You must identify the actual contract before comparing implementations or transformations. SmallExpr's wrapping rule is explicit and applies after each operation, including unary negation. It is not permission to import the behavior of the JavaScript host's ordinary multiplication or another language's signed integer operations.
Try 999 + 1 in the type view, then the wrapping preset. Both receive type int, but one produces a small positive value while the other produces the negative result derived above. Next enter 1000 by itself. The failure is now an input limit, before the checker can establish an expression type. Finally enter true + 1. This fails the arithmetic type requirement rather than a range requirement. These comparisons isolate spelling bounds, operand classification, and execution semantics instead of treating every rejected or surprising result as one kind of error.
Separate spelling limits, types, and arithmetic
Source
First relevant rule
Outcome
999 + 1
Legal literals; integer addition
int, value 1000
1000
Source literal bound 0–999
Limit error
true + 1
No boolean arithmetic coercion
Typing error
999 * 999 * 999 * 999
Wrap every integer operation
int, value −426,416,671
The editor literal bound does not restrict all computed values to 0–999. Overflow is defined arithmetic here, not a typing failure.
A transformation must preserve the selected arithmetic contract as well as the type. Folding a constant multiplication may remove runtime instructions, but its replacement literal must denote the wrapped result, not the unbounded product. Internal compiler literals can represent results beyond the editor's source-literal bound because they were computed rather than typed as source tokens. The current folder uses the same arithmetic operations as execution. Agreement is useful implementation evidence, while the independent modular calculation supplies a separate expected result. A smaller instruction count alone proves neither semantic correctness nor faster execution.
Do not turn a guarantee into a universal safety claim
A sound type system aims to ensure a stated property under a stated semantics, often that well-typed programs avoid specified stuck states. That does not imply termination, correct business logic, absence of all exceptions, or safe interaction with every foreign function. The guarantee must name its domain.
Our arithmetic is defined to wrap at 32 bits rather than trap on overflow. Typing an expression as int does not mean its mathematical result fits an unbounded integer. Many real languages make different choices about overflow, nullability, memory safety, and unsafe operations. Optimization must honor those choices.
State the property that a type rule proves
A soundness claim connects static acceptance to a property of execution under stated assumptions. For this arithmetic language, a useful property is that accepted arithmetic nodes do not receive boolean operands when evaluated under an environment with the checked binding types. Begin at a numeric literal, which produces an integer, or an integer binding, which supplies one. If each child of an accepted arithmetic node produces an integer, the specified operation accepts them and returns another integer. Repeating that argument up the finite tree explains the claimed connection.
The environment assumption matters. If a compiler checks x as an integer but execution later substitutes a boolean for x, the original premise has changed. A larger implementation could prevent that mismatch through typed storage, bytecode verification, runtime checks, or another explicit boundary rule. Here the editor supplies the same fixed environment to checking and execution. The model also validates supplied environment integers as signed thirty-two-bit values. These conditions do not establish trust in arbitrary external data.
Match a guarantee to its assumptions
Claim
Required evidence
Not established by int typing
Arithmetic receives integers
Typing derivation; checked binding types retained
Trust in unvalidated external values
This model finishes
Finite tree; terminating primitive operations
Termination of arbitrary recursive programs
Calculation matches the task
Task specification and expression reasoning
Correct grouping or chosen formula
A rewrite is valid
Preserved acceptance and arithmetic semantics
Speed or correctness from fewer instructions
These obligations are distinct. The first is the local operand guarantee; the others need additional arguments.
Termination needs its own reasoning. SmallExpr evaluation follows a finite, bounded syntax tree, and each supported arithmetic operation completes. Those facts explain why its accepted expressions finish in this model. The int type alone does not establish termination in a language containing unrestricted loops or recursion. Integer typing alone would not prove that a division avoids zero. SmallExpr has no division, so there is no such obligation in this checker. State the operations and excluded failure modes before extending the guarantee.
Even within the language, a perfectly typed expression can answer the wrong question. Suppose a task asks for twice x plus y. The expressions x * 2 + y and x * (2 + y) both have type int. With the fixed values, the first returns fifteen and the second returns thirty-six. Type checking cannot choose between them because their operand categories satisfy identical requirements. Parsing establishes their different structure, and the task specification determines which structure is intended. A correctness argument needs that specification in addition to a typing derivation.
An optimizer must also preserve rejection when its input language requires checking before execution. Consider flag * 0. Replacing the entire tree with zero before checking would conceal an invalid boolean multiplication. The current build checks first and folds numeric literal subtrees afterward, so this source remains invalid. This ordering is an implementation decision that preserves the language's acceptance rules. It does not mean all compilers must use physically separate passes. A combined implementation could enforce the same obligation if it retained enough evidence to reject the original invalid operation.
Both roots have type int, but grouping changes the value
Schematic syntax trees. The fixed environment gives x = 4 and y = 7. Both type-check; the task specification must decide which formula is intended.
For a final guided comparison, predict the outcomes of flag, -flag, x * 2 + y, and x * (2 + y) before entering them. The first is a valid boolean expression; the second fails unary arithmetic typing. The final pair both compile as integers but return different values. Explain each outcome using its own evidence: a binding type, an operator requirement, a grouping decision, or a numerical calculation. This separates static proof from dynamic execution and from task correctness, which is the distinction needed when reading stronger type-system guarantees later.
Exercises
Check without evaluating
Given x: int and flag: bool, can you type-check x * (flag + 1) without knowing the numeric value of x?
Hint
The nested addition already imposes an incompatible requirement.
Worked answer
Node
Requirement
Finding
flag + 1
int and int
bool conflicts
x * inner result
int and int
Inner expression is invalid
A type conflict can be established before any value calculation.
Yes. The inner + requires two integers but receives flag: bool. The expression fails typing regardless of x’s numeric value. Running the multiplication is neither necessary nor permitted as a substitute for this static rule.
Typed does not mean correct
A well-typed program computes a tax using the wrong percentage. Does this refute the usefulness of type checking?
Hint
Identify the property the type system actually checks.
Worked answer
Property
Established by int arithmetic typing here?
Operands are integers
Yes
Tax rate matches policy
No
Program terminates in a richer language
Not by this rule alone
Different guarantees require different evidence.
No. A type system that checks numeric operands does not also prove that a particular percentage matches policy. More expressive types or proofs can encode some domain requirements, but ordinary int typing alone does not. State the guarantee instead of treating typing as either complete correctness or uselessness.
Sources and further reading
The explanations, examples, and worked answers are complete without these optional links. The sources describe specific implementations and language contracts, not one universal compiler pipeline. SmallExpr and the later pseudocode models are constructed teaching examples. Source notes identify the selected material reviewed; this is not an exhaustive compiler survey, production conformance test, or independent specialist review.
Selected material on static type checking, inference, and erased types. An example of a real language’s choices, not a universal type-system guarantee or the rules of SmallExpr.
Selected material on IR structure, SSA, phi semantics, integer operations, and semantic constraints. A production IR reference, not a specification of SmallExpr or a claim that every compiler uses LLVM.