A type describes permitted values and operations. A declaration is not a runtime inspection.
By the end: explain what a type claim means and identify where external data needs checking.
This course assumes familiarity with variables, functions, and conditionals, not type theory or compiler implementation. The core uses authored expression trees and a small pure language. Other labs state their own separate rules; they are not full TypeScript, OCaml, or Rust implementations.
A value is not its representation
The integer 3, the boolean true, and the text "3" are different values in our teaching language. They may have similar printed forms or share a machine representation, but the language permits different operations on them. Our addition accepts two Int operands; it does not convert booleans or strings.
A type classifies values and the operations available on them. Int describes more than one integer. A function type describes an input/output relationship rather than a particular function body. These descriptions can rule out some mistakes without describing every property of a program.
Choose which distinctions a type records
A printed character does not determine which operations a value supports. Consider the integer 3 and the text "3". Printing either might show the same digit, but integer addition needs an integer operand. Text would need an explicitly specified conversion first. A representation is how a value is stored or displayed; a type is part of the language's description of how that value may be used. This distinction explains why copying characters from an input box does not establish that the resulting value supports integer arithmetic.
The small expression language used later has an Int type and a Bool type. Int describes integer values; Bool describes exactly false and true. Addition requires Int on both sides, while a conditional requires Bool as its guard, the expression that decides between branches. The language does not interpret zero as false or true as one. These restrictions are definitions, not discoveries about hardware. Two implementations could store booleans differently and still agree on these typing rules. Conversely, shared storage formats would not justify exchanging the two types.
Identical digits do not establish identical operands
Value
Kind of value
Meets an Int operand requirement?
3
Integer
Yes
"3"
Text
No
true
Boolean
No
The operation requires a typed value, not merely a matching printed character. No implicit conversion supplies the missing premise.
A type deliberately forgets some information. The integers 3 and 4 both have type Int, so the type does not tell you which integer an expression returns. That loss makes one description useful for many expressions. Knowing that both operands are Int lets an addition rule apply without enumerating every possible pair of integers. It does not tell you whether the answer is the number your application intended. A price, a count, and an identifier can all have integer representations while requiring different application rules.
A type constructor builds a larger type from component types. Pair<Int, Bool> describes an ordered pair whose first component is an integer and whose second is a boolean. Ordered means that position matters. Pair<Bool, Int> describes a different arrangement, even though it mentions the same component types. The function constructor instead connects an input type to an output type. Int → Bool describes a function accepting an integer and returning a boolean. Neither constructor says that its two component types must be identical, and neither is an arithmetic operation.
For a finite example, pair two boolean components. Each first component has two choices, and each of those can accompany either of two second components. There are therefore four ordered pairs. A function from Bool to Bool describes a different relationship. If we consider only mathematical functions that give one boolean result for each boolean input, there are four possible input/output assignments too. Equal counts do not make pairs and functions interchangeable. A pair stores two positions; a function supports application to an argument. This counting comparison is a paper example, not an additional control.
Component positions belong to different constructors
These schematic type trees separate component position from constructor meaning. Pair construction stores components; function application consumes an input.
The distinction transfers to everyday design decisions. Suppose an integer represents an age. Int alone does not express a lower bound of zero, an upper bound of 130, or whether the number came from a truthful report. You can impose some of those requirements with a validator, a function that examines a value and either accepts it or reports a failure. Before choosing the validator, state the property you need. An integer check, a range check, and an identity check answer different questions, even when they inspect data about the same person.
Static claims and runtime checks
Static typing reasons from source code and declared assumptions before execution. Dynamic checks inspect values during execution. A language can use both. In TypeScript, a type assertion changes the checker’s view but does not validate a JSON payload or convert a string into a number.
The example below actually parses and validates a small JSON object. It accepts a nonblank name and an integer age from 0 through 130. This range is a schema policy, not a consequence of the ordinary number type. Extra fields are ignored and the accepted result copies only name and age.
Separate syntax acceptance from schema acceptance
JSON is a format for representing values as text. Parsing JSON means recognizing that format and producing the represented value. A schema is a separate collection of requirements for a particular use of the value. The lesson's schema requires an object containing a name and an age. A text that parses successfully may represent a list, a boolean, or an object with the wrong fields. None of these is a syntax error in JSON. They fail the later object or field requirements instead, so parsing cannot replace schema validation.
Follow the paper payload {"name":"Mina","age":"20"}. The quotation marks around 20 make its age a string. Parsing preserves that distinction. The result contains an age field, but an integer test fails because text is not a number. Removing those quotation marks produces the integer 20, which passes the integer requirement and both range bounds. The validator does not perform this edit for you. Refusing automatic conversion keeps the accepted property explicit and avoids guessing what a sender meant by an unexpected representation of the field.
Two valid JSON objects reach different schema results
Stage
String age preset
JSON syntax
Accepted
Object
Accepted
Name
Accepted
Age
String "20" fails integer requirement
Result
No validated object
Stage
Valid fields preset
JSON syntax
Accepted
Object
Accepted
Name
Accepted
Age
Integer 20 is within bounds
Result
Name and age copied
Parsing retains the distinction between a number and digit-containing text. Schema validation then checks the represented value without coercion.
The age checks narrow the accepted possibilities in stages. A required own field must exist on the object itself. Its value must be a number, must be an integer, and must lie between zero and 130 inclusive. Inclusive means that both endpoints are allowed. The value 20.5 passes the number check but fails the integer check. The integer 131 passes both of those checks but fails the upper bound. A string containing digits fails earlier. These examples isolate different obligations rather than treating every rejection as the same kind of bad number.
The name rule combines a representation requirement with a content policy. The value must be text, and its length may not exceed 30 UTF-16 code units, the units used by JavaScript string length. An ordinary Latin letter uses one unit, while many emoji use two. This is not a count of visible symbols. Removing surrounding whitespace for the blankness check must leave something. A string containing only spaces therefore fails even though it is text. The successful result copies the original name; the blankness test does not promise to trim or otherwise normalize it. A name with surrounding spaces can pass without losing them. Testing a property and rewriting a value are distinct operations, and this validator performs only the stated copying.
The order of checks explains which error appears when several properties fail. Invalid JSON prevents the validator from obtaining an object at all. A parsed list fails the object requirement before either field has a usable interpretation. For an object, the implementation checks name before age. An object missing both fields therefore reports a name error first; this is not evidence that its age is valid. The displayed message identifies the first failed obligation reached by this procedure. A later edit can expose another failure that was already present in the original text.
Being numeric is not enough to meet the age policy
Age field
Number?
Integer?
Within 0–130?
Accepted age?
20
Yes
Yes
Yes
Yes
20.5
Yes
No
Yes
No
131
Yes
Yes
No
No
"20"
No
No
No numeric age
No
Missing
No value
No value
No numeric age
No
Each column compares a logical requirement independently, not an execution trace after rejection. Numeric representation, integer status and the age range all matter.
Static assumptions become useful after this boundary has established their premises. A function that adds one to a validated age can rely on receiving an integer in the stated range, provided the caller passes the validated result. Merely annotating an unchecked input with a desired type reverses that reasoning. It supplies an assumption without supplying the evidence needed for the assumption. In this lesson, the local validator produces the evidence through actual field checks. It does not ask the core expression-language inference engine to understand arbitrary JSON or the age policy.
Inspect the rules and their result
Compare a claimed type with an actual validation result
Unchecked assertion
Claim: User
A type assertion alone does not inspect these fields.
Validated result
No validated User result.
Rejected: age must be an integer from 0 through 130.
Presets replace the entire local JSON text; manual edits retain no previous success. Parsing accepts JSON syntax; validation checks only name and age. Extra fields are discarded from the returned object, not approved for use elsewhere. No payload is sent or stored. Maximum input length is 200 characters.
Input
What the check establishes
{"name":"Mina","age":20}
Required fields and age range
{"name":"Mina","age":"20"}
Rejected: string is not an integer
A schema check does not verify the truth of a claimed age.
Trace what each payload change establishes
Start the displayed validator with the String age preset. Compare the two panels without changing the text. The unchecked assertion panel continues to state a claim about User, while the validated panel has no successful result. The age error follows from the string representation, not from the spelling of Mina. Now select Valid fields. The entire payload changes, and the validator returns an object containing name and age. The meaningful contrast is that an actual check changes its conclusion when the evidence changes; the assertion alone does not inspect that evidence.
Use the editable text to replace age 20 with 20.5 while keeping the object and name unchanged. JSON parsing still succeeds, so the failed integer condition explains the rejection. Next try 0, 130, and 131. Zero and 130 meet the inclusive bounds; 131 does not. These edits hold all unrelated conditions constant. They separate a numeric representation question from an application range question. The textbox accepts at most 200 UTF-16 code units, so this exploration concerns short local payloads, not file uploads or a validator for unrestricted document sizes.
Controlled payload edits isolate representation and policy
Local edit or preset
Unchanged evidence
Decisive condition
String age → Valid fields
Object and name
String becomes integer
20 → 20.5
JSON syntax and numeric value kind
Integer check fails
20 → 0
All other fields
Lower endpoint is included
20 → 130
All other fields
Upper endpoint is included
130 → 131
Integer representation
Upper bound fails
Keeping the name fixed makes each age edit a comparison of one changed condition, rather than an unexplained overall rejection.
Select Missing age and compare it with String age. One object lacks a required field; the other has the field with an unacceptable value. Both prevent a validated User result, but they require different repairs. Adding age with the value null would fix presence without fixing the numeric requirement. Adding age with the value zero satisfies both. This distinction matters when diagnosing a boundary failure. A field's presence is evidence only for presence, and a broad statement such as 'the field exists' cannot justify arithmetic on whatever value it contains.
Select Extra role field and inspect the successful object rather than only the accepted status. The input contains role, but the output contains only name and age. This operation is a projection: it constructs a result by selecting specified components from a larger input. The validator does not validate role and then silently approve it. It excludes that component from the returned value. Comparing the input and output field lists reveals a stronger boundary than returning the original object after checking only two of its fields would provide for later consumers.
After a success, edit the age into an invalid value again. The previous successful object must no longer represent the current text, and this interface removes it. Otherwise two incompatible observations could remain visible: an invalid current payload and a successful result produced from an earlier payload. The result belongs to one particular input, not to the textbox indefinitely. Here every edit recomputes validation locally. There is no saved account record or remote update behind the display, so an accepted status records the validator's conclusion about the current text only.
The accepted result selects fields rather than approving every field
Input field
Input value
name
"Mina"
age
20
role
"admin"
Result field
Result value
name
"Mina"
age
20
role
Not copied
The extra role remains input data only. Neither ignoring it nor accepting the other fields authorizes an administrative action.
A useful explanation of a result can now name the exact evidence. For the valid Mina payload, parsing establishes an object representation, the name checks establish nonblank bounded text, and the age checks establish an integer within the permitted interval. Copying establishes which fields enter the result. None of those observations verifies that Mina exists or that the browser user may act for her. The lab provides no account lookup or permission check. This is a worked separation of obligations, not a reason to distrust the checks that genuinely succeeded.
Name the boundary of the guarantee
Successful validation establishes those checked properties at that moment. It does not establish a person’s identity, the truth of their stated age, permission to use their data, or compatibility with a remote service. No data in this lesson leaves the browser.
The rest of the course uses a deliberately small language. Its rules are not JavaScript coercion rules or the entire TypeScript type system. Treat the language definition, checker implementation, and runtime behavior as separate objects that must agree.
Carry only the guarantee supported by the evidence
Imagine a later calculation that estimates age next year. If the validated age is 130, integer addition gives 131. The original object satisfied the schema, and the arithmetic result is still an integer, but 131 is outside the accepted age interval. There is no contradiction. The schema constrained the input field, while addition's type constrains the kind of result. A property is preserved by an operation only if the operation's behavior supports that conclusion. Ordinary integer addition does not promise to preserve an arbitrary upper bound chosen for one application.
The same reasoning applies to names. A successful name uses at most 30 UTF-16 code units, but concatenating two accepted names can produce more than 30. Concatenation means joining text end to end; it is an application example here, not an operation of the core expression engine. If one accepted name has 18 ordinary Latin letters and another has 17, the joined text has 35 code units before adding any separator. The length policy would need checking again if that joined value were submitted as a name. Component validity alone does not imply validity after every transformation.
Integer addition does not preserve the age interval
Validated age
Add one
Integer result?
Result in age interval?
0
0 + 1 = 1
Yes
Yes
20
20 + 1 = 21
Yes
Yes
130
130 + 1 = 131
Yes
No
The arithmetic preserves integer representation in these examples. It does not preserve the independent upper bound imposed by the schema.
A guarantee also belongs to a particular value. The validator returns a new object containing the selected fields instead of handing back the complete parsed object. Extra fields cannot enter that result through the original payload's field list. This observation does not establish an ownership system or prove that arbitrary surrounding code cannot later replace fields. Mutation means changing an existing value's stored contents, and the core expression engine deliberately has no mutation. When reasoning about a larger application that does permit it, identify where a checked property might cease to hold.
Types support composition when each operation receives what its assumptions require. Composition means using one operation's result as another operation's input. After validation, a consumer needing an integer age can use the checked field without reparsing the original text. A consumer needing an authorized account owner cannot make the same inference because the validator never established that requirement. This method works even before learning formal typing notation. Write down what the first operation establishes and compare it with what the next operation assumes. Any unmatched assumption is a separate obligation, not a consequence of shared field names.
Distinguishing implementation layers prevents a second mistake. The JSON validator runs real checks on local text, but the later expression labs infer types from authored expression trees. A tree records an expression's operations and children explicitly. Its printed form resembles source code, yet there is no free-text parser that turns your JSON edits into those expressions. Text fields and the Text label in separate labs do not add strings to the core language. Each lab has its own input and rule set, so successful validation cannot be read as an inferred core-language type signature.
Each consumer needs evidence relevant to its operation
Proposed use
Needed evidence
Provided by this validator?
Read age as an integer
Integer field
Yes, in the returned object
Treat age plus one as an accepted age
Transformed result in range
No, 130 is a counterexample
Use role as a permission
Authorization decision
No, role is not copied or checked
Accept claimed age as fact
Evidence about the person
No factual verification
The boundary establishes representation and field policy. Later operations must supply any stronger premises rather than inheriting unrelated guarantees.
Consider two consumers of the same successful result. One displays the name and calculates age plus one. The other grants access to a private account. The first has representation evidence relevant to its operations, though it still needs its own display and application requirements. The second lacks the permission evidence its action requires. Calling both consumers 'type-safe' would hide this difference. A precise conclusion states which values passed which checks and which operations rely on those facts. That conclusion can support further reasoning without claiming that a type or schema captures the entire purpose of the application.
Exercises
An assertion at a boundary
A program parses JSON and asserts that it is a User with a numeric age. Does the assertion prove that adding 1 to age is integer addition?
Hint
Ask whether any runtime check examined the value.
Worked answer
Operation
Inspects runtime payload?
Type assertion
No
JSON parsing
Checks JSON syntax, not the User schema
Schema validation
Checks its stated field rules
Each boundary operation establishes a different fact.
No. The payload might contain a string or lack age. The assertion does not inspect it. Validate the required fields before exposing a trusted User value, and distinguish a successful shape check from evidence that the data is factually true.
A number still needs a policy
Why does the example reject age 20.5 even though it is a JavaScript number?
Hint
Separate a broad representation type from a narrower domain rule.
Worked answer
Value
Number?
Accepted age?
20
Yes
Yes
20.5
Yes
No
131
Yes
No
"20"
No
No
The lesson’s age policy is explicit, not universal.
The schema requires an integer from 0 through 130. The number representation also includes fractions and other values. A type like number alone does not encode the schema’s integer/range policy. The validator must check that policy explicitly.
Sources and further reading
Selected reference passages support the definitions and algorithms below. The examples, explanations, and implementations are original. Terminology and assumptions are stated within each lesson; source review is not an independent audit of this course. Optional links are not runtime dependencies.
Selected contexts, function application, and typing-rule explanations. The formal chapter defines its own calculus; our additional integers, pairs, and let inference are not automatically covered by its theorems.
Selected structural compatibility and documented soundness trade-offs. Exact compiler behavior depends on flags and language version; our idealized variance lab is not a conformance test.