# Types Epsil does not have its own type system: it uses the [Compute Engine type language](https://mathlive.io/compute-engine/guides/types/), which covers unions, intersections, tuples, records, function signatures, and generic collection types. See that guide for the type language itself. This page covers where a type annotation is written in Epsil source, what it means, and how a program declares type names of its own. ## Annotation positions A type annotation follows a `:` after a declaration target: ```epsil x: real x: real = 5 ``` Type-syntax tokens — `<`, `>`, `->`, `|`, `&` — are only meaningful **inside** a type annotation. They are never part of the general expression grammar: once the parser sees a leading `symbol :`, it hands the rest of the type expression to the type subparser and resumes parsing Epsil source exactly where the type subparser stopped. An unrelated `:` that doesn't follow a declaration target at the start of a statement is not treated as an annotation at all. Function parameters and return values can also be annotated: ```epsil f(x: real, n: integer) -> real = x^n function g(x: integer) -> integer { x + 1 } (x: integer) |-> x + 1 ``` Parameter annotations are enforced when a function is called. A return-type annotation is recorded in the function's signature, but the current runtime does not reject a returned value merely because its inferred type differs from the annotation. Named functions can also declare their effects between the parameter list and the return type: ```epsil function roll(n: integer) random -> integer { Random(n) } ``` Effect labels are part of the function type. See [Effect specifiers](/control-flow/#effect-specifiers) for declaration syntax and the [function type guide](https://mathlive.io/compute-engine/guides/types/#function-types) for subtyping rules. The whole of a type annotation is read by a dedicated type subparser, so `<`, `>`, `|`, `&`, and `->` inside it are consumed there and never reinterpreted by the surrounding expression grammar. In `u: integer | boolean`, the `|` is part of the type, not a logical operator: ```epsil xs: list f: (real) -> real ``` ## Semantics Type checking is not a separate Epsil-side pass — it happens as the program is prepared and evaluated, the same way it does for any other declared symbol. Epsil does not add a second type checker on top of the runtime's. ## Inference A symbol with no annotation gets its type inferred by the engine from how it is used — the same inference the engine already performs for any undeclared symbol. This includes the engine's existing convention that evaluating a bare symbol as a boolean operand (`And`/`Or`/`Xor`/`Not`) infers that symbol `boolean` for the lifetime of the engine; a later numeric use of the same symbol in the same scope will then error. This is engine behavior, not something specific to Epsil. ## How the type system works None of this section is needed to use Epsil — it is background for readers curious about what kind of type system this is and why it behaves the way it does. ### Types form a lattice The foundation of the system is **subtyping**: types are arranged in a hierarchy, and most questions the engine asks are of the form "is this type a subtype of that one?". The numeric types form a tower — `integer ⊂ rational ⊂ real ⊂ complex ⊂ number` — so an `integer` is accepted anywhere a `real` is expected, with no conversion involved. Around that tower the type language adds unions (`integer | boolean`), range refinements (`integer<0..10>`), collections with element types (`list`, `set`), tuples and records, and function signatures with effect labels. Any two types have a **join** (the narrowest type that covers both — the join of `integer` and `real` is `real`) and a **meet** (the widest type inside both). Joins and meets are the workhorses of the whole system: the type of a mixed list is the join of its element types, and inference (below) is built out of these two moves. ### It is not Hindley–Milner Languages in the ML family (OCaml, Haskell, Elm) use a different foundation, called Hindley–Milner: types are compared for *equality* and solved by unification, which buys two famous guarantees. Every expression has a **principal type** — a single most general type that every other valid type is a specialization of — and inference is **whole-program**: the compiler sees the finished program at once, and a use of a function far from its definition can determine the definition's type, with no annotations anywhere. This system deliberately trades those guarantees away, for two reasons. First, subtyping and principal types pull against each other. In Hindley–Milner, `integer` and `real` simply fail to unify; here, a function declared `forall T. (T, T) -> T` called with an `integer` and a `real` succeeds, solving `T` to their join (a `real`). That is the behavior mathematics wants — but once many types are valid for an expression, "the single most general one" stops being the useful answer, and the engine makes pragmatic choices instead. Second, there is no "whole program" to infer over. A session is open-ended: definitions arrive one statement (or one cell) at a time, may refer to names defined later, and may be redefined. The engine therefore types what it has seen so far and refines as more arrives, rather than solving a closed program once. In character the system is closer to TypeScript or Go than to ML: subtyping at the base, generics that are explicitly declared rather than silently inferred, and types solved locally rather than globally. ### Generics are explicit and solved per call A function is generic only when it is *declared* generic — with a `function f(…)` clause or a `forall` annotation. Nothing is silently generalized: `x |-> x` is a function on some inferred type, not an implicit "for all T". At each call of a generic function, the engine collects what the arguments say about each type variable and solves the variables on the spot, by joining that evidence; the call's result type comes from substituting the solution into the signature. Subtyping also quietly absorbs a classic use of polymorphism: the empty list needs no "for all" type — it is simply `list`, and since `never` is the bottom of the lattice (joining it with anything gives the other type back), `Join([], [1, 2])` comes out as `list` with no quantifier anywhere. ### Inference gathers evidence, and can change its mind When a symbol has no annotation, the engine does not solve equations to find its type — it accumulates **evidence** from how the symbol is used, moving through the lattice as evidence arrives. Using a symbol as an argument *narrows* its type toward the parameter's; assigning it a value *widens* its type to cover the value. A symbol first seen in `x + 1` is provisionally taken to be a `number` — a guess, not a theorem. Because they are evidence, inferred types are **revisable** in ways a Hindley–Milner type never is. A guess that turns out incompatible with a later assignment is discarded in favor of the value's own type, and a function that referred to a name defined only later is re-derived once the definition appears, so declaration order does not change what a program means. Only *inferred* types move: a type you annotate is a commitment, never silently revised — which is the practical takeaway. Annotations are never required, but where the inferred guess isn't what you meant, an annotation pins it. ## Absence values Epsil distinguishes three related kinds of absence: - `Nothing` means “no value here” and is removed from function arguments and collection literals. - `Missing` is a position-preserving missing value. Its type is `missing`. - `NaN` is the numeric form of an absent or undefined result. Numeric operations and missing numeric fields generally normalize absence to `NaN`. `IsMissing(x)` recognizes both `Missing` and `NaN`, regardless of how the value arose. `Coalesce(a, b, ...)` evaluates from left to right and returns the first value that is not missing; if every argument is missing, it returns the last one unchanged. ```epsil-live (Length([1, Missing, 3]), IsMissing(Missing), IsMissing(NaN), Coalesce(Missing, 0), Missing + 1) // ➔ (3, True, True, 0, NaN) ``` A missing dictionary field follows the expected value domain: a numeric field produces `NaN`, while a string or other nonnumeric field produces `Missing`. Use `IsMissing` when the distinction between those representations is not important, and `Coalesce` to supply a fallback. ## Declaring a type A `type` statement gives a name to a type. The name is usable by every annotation later in the program — and by later cells sharing the same engine. There are two forms, and they mean different things. **`type` declares a new, distinct type.** Nothing that merely *looks* like the definition belongs to it: the definition describes how the type is built, not which values are already members of it. ```epsil-live type point = tuple let p = point(1, 2) p // ➔ point(1, 2) ``` **`type alias` declares another name for an existing type.** Any value of that shape is a value of the alias — it is an abbreviation, not a new type. ```epsil-live type alias pair = tuple let a: pair = (1, 2) a // ➔ (1, 2) ``` Reach for `type alias` to shorten a type you write often (`type alias grid = list>`), and for `type` when the new type is meant to be its own thing — a `meters` that a bare number cannot be mistaken for. Neither `type` nor `alias` is a reserved word. Only the statement-position shapes `type name =`, `type name<`, `type alias name =` and `type alias name<` are read as a type declaration, so `type` remains an ordinary identifier everywhere else — `type: integer = 4` still declares a variable named `type`: ```epsil-live let type = 5 type + 1 // ➔ 6 ``` (And `type alias = tuple`, with nothing between `alias` and `=`, declares a type *named* `alias` — legal, but not a spelling to reach for.) ### Constructors A type declaration also declares a **constructor**: a function of the same name that builds values of the type. A `tuple` definition gives a constructor with one argument per field; any other definition gives a one-argument constructor: ```epsil-live type point = tuple type meters = number (point(1, 2), meters(5)) // ➔ (point(1, 2), meters(5)) ``` The arguments are checked against the definition, so `point(1)` and `point("a", 2)` produce an error value rather than a malformed point. A value built this way carries its type with it, wherever it goes: ```epsil-live type point = tuple let ps = [point(1, 2), point(3, 4)] Type(ps) // ➔ "list" ``` An **alias** constructor is a checked cast instead of a tag: it validates the arguments against the definition and hands back the plain value. ```epsil-live type alias pair = tuple pair(1, 2) // ➔ (1, 2) ``` A `record` definition auto-declares **no** constructor: a record's fields are named, so building one from positional arguments would silently depend on the order the fields happen to be written in. Write one instead — see [constructor functions](#constructor-functions) below. Until one is declared, calling the name reports a `type-not-callable` warning. ### Constructor functions A `function` with a declared type's name — in the same scope, after the `type` statement — is that type's **constructor function**. The body computes the *payload*: a value that must satisfy the type's definition (for a record, exactly the definition's keys, each field matching its type). The engine checks the payload and tags it; the result is a value of the type. This is how a `record`-bodied type gets its constructor: ```epsil-live type circle = record function circle(x, y, r) { {x -> x, y -> y, r -> r} } Type(circle(1, 2, 3)) // ➔ "circle" ``` Constructor functions are not record-specific: one may be written for any definition, replacing the automatic constructor — the *smart constructor* idiom of validating or normalizing on the way in: ```epsil-live type frac = record function frac(n: integer, d: integer) { {n -> n / GCD(n, d), d -> d / GCD(n, d)} } frac(2, 4) == frac(1, 2) // ➔ True ``` A value that already satisfies the definition can be handed to the constructor directly — one argument, checked and tagged, body skipped. That raw spelling is also how a constructed value prints and reads back (`circle(1, 2, 3)` prints as `circle({x -> 1, y -> 2, r -> 3})`), so a round trip injects the payload unchanged and a normalizing constructor's values stay equal after it. Because the payload spelling must construct unchanged, a constructor's parameters have to be *distinguishable* from the payload itself: a `function` whose parameters could also be a valid payload — same number of arguments, types the definition overlaps — is rejected when it is declared. Use a different number of arguments, or annotate the parameters with types the definition body cannot mistake. A constructor function may call itself, and returning its own constructed value passes it through unchanged. A `function` with a type's name declared *before* the type is an ordinary function — the later `type` statement then reports the usual conflict. And for an **alias**, a same-name function is just an ordinary function: there is no tag to apply. ### Values of a new type are opaque A `point` is not the tuple it is defined from — that is what makes it a new type. So a plain tuple is not accepted where a `point` is expected, and the operations that take a tuple apart do not reach inside one: ```epsil type point = tuple let q: point = (1, 2) // error: a tuple is not a point let p = point(1, 2) First(p) // error let (a, b) = p // error ``` Each of those lines parses: the rejection happens when the program runs, as an [error value](/evaluation/#errors-are-values), not as a parse error. To read the parts back, [`match`](/control-flow/#match) on the constructor — a constructor pattern is an ordinary operator pattern, and binds one variable per field: ```epsil-live type point = tuple let p = point(3, 4) match p { point(x, y) => x + y } // ➔ 7 ``` To read a single **named field**, use the `.` accessor. It works on values of a declared type whose definition has named fields — a record body or a named-tuple body — and on records and dictionaries generally: ```epsil-live type point = tuple let p = point(3, 4) p.x + p.y // ➔ 7 ``` On a dictionary, `d.x` is exactly `d["x"]`, absent-key behavior included. The accessor reads one named field through the type's definition; it does not make the value a collection — `First(p)`, `p["x"]` and destructuring keep rejecting, and `match` remains the way to take the whole value apart at once. (The dot must touch the value it reads: `p.x` is a field access, `p .x` is not; and a number never takes a field — `2.x` is a multiplication.) An **alias** has none of this reserve — it *is* its definition, so an alias-typed value works anywhere the underlying shape works: ```epsil-live type alias meters = number function height(m: meters) { m + 1 } height(2) // ➔ 3 ``` ### Equality Two values built by the same constructor are equal when their arguments are. Values built by different constructors are never equal, and neither is a constructed value and a plain one of the same shape: ```epsil-live type point = tuple type polar = tuple (point(1, 2) == point(1, 2), point(1, 2) == (1, 2), polar(1, 2) == point(1, 2)) // ➔ (True, False, False) ``` ### Scope, and re-running a cell A type declaration — both the type name and its constructor — lives in the current scope, like a `let`. One inside a block or a loop body stays there: ```epsil-live let origin = 0 do { type inner = tuple inner(3, 4) } // ➔ inner(3, 4) ``` Re-running a `type` statement for a name that an earlier `type` statement declared **replaces** the earlier definition, constructor included — [constructor functions](#constructor-functions) too, since an edited definition may invalidate the old body; re-running the whole cell restores both. Re-running a `function` statement that declares a constructor replaces the constructor. A name declared some other way — a `function` of that name *predating* the type, or a type declared by the host application — is not replaced: the statement reports an error value and declares nothing. ### Type variables A generic **type alias** takes a type-parameter clause between its name and the `=`. The applied spelling is usable anywhere a type is written, and expands **transparently** — `Pair` means exactly `tuple`, and that expansion is what type displays and error messages show: ```epsil type alias Pair = tuple let p: Pair = (1, 2) ``` A parameter may carry a ground bound, enforced wherever the alias is applied — including application to another clause's type variable, which is admitted when the variable's own bound satisfies the parameter's. One alias may therefore be built out of another: ```epsil type alias Keyed = tuple type alias Table = list> let rows: Table = [("a", 1), ("b", 2)] ``` A generic alias may not refer to itself, every parameter must be used in the body, and applying one without its arguments (a bare `Pair`) is an error. Unlike a plain alias, a generic one declares **no** [constructor](#constructor-functions) and claims nothing in the value namespace: a `function` of the same name is an ordinary function, declared before or after. A dependent alias **snapshots** the definitions it was built from: re-running the `type` statement for `Keyed` leaves `Table` as it was until `Table`'s own statement is re-run too — which re-running the cell does. A parameterized **nominal** type — the bare form — takes a clause too, and takes it the same way. The difference is what an application means: a nominal type is **opaque**, so `tree` is never expanded, which is what lets its body be recursive. ```epsil-live type tree = tuple>> let t = tree(1, [tree(2, [])]) Type(t) // ➔ "tree" ``` The constructor is **quantified** — `tree: forall T. (T, list>) -> tree` — so `T` is solved at each construction, from the arguments. Applying the type at the wrong arity — including a bare `tree` — is the same error as for an alias, and a parameter bound is enforced the same way. Reading a **field** reads the definition **instantiated at the application's arguments**, so it comes back at the type the application supplied, not at `T`: ```epsil-live type tree = tuple>> let t: tree = tree(1, []) Type(t.value) // ➔ "number" ``` `match` is not a projection of the annotation — it binds **values**, so each capture comes back at the matched value's *own* type, usually narrower than the annotation's: ```epsil-live type tree = tuple>> let t: tree = tree(1, []) match t { tree(v, cs) => Type(v) } // ➔ "integer" ``` **Variance.** A parameter may carry an `in`/`out`/`inout` marker saying how two applications relate: `out` (covariant) makes a `tree` usable where a `tree` is expected, `in` (contravariant) reverses that, and `inout` (invariant) relates only identical arguments. The words are contextual, claimed only inside a clause. An alias takes no marker — it expands rather than relates. ```epsil type tree = tuple>> type sink = tuple nothing> ``` **A parameter with no marker means `out`** — declared, not inferred, and verified against the body like any written marker. Values are immutable, so covariance is sound, and it is what the common case (a payload container) wants; only the minority that consumes its parameter needs to say so. Because the default is *declared*, a body that uses its parameter in an input position does not quietly change the type's subtyping contract — it is a `variance-violation` naming the offending occurrence and the markers that would verify: ```epsil type events = tuple, notify: (T) -> nothing> ``` This statement parses, but declares nothing: it evaluates to an error value carrying a `variance-violation`. `T` appears in both an output position (`log`) and an input one (`notify.(arg 1)`), so `events` can only be `inout` — writing `type events = …` accepts the definition, at the cost of `events` no longer being usable as an `events`. `inout` verifies against any body: invariance promises nothing, so it is always sound, just less permissive. One limitation follows from that. A construction solves its parameters from its arguments alone, and an annotation does not widen them: `let t: tree = tree(1, [])` works only because the `tree` it builds *is* a `tree` under `out`. For an explicitly `inout` or `in` parameter that step is not available, so such a type can only be constructed at exactly its argument type. **Unions.** A type variable may stand in one arm of a union, which is what makes an optional payload expressible: ```epsil-live type opt = T | missing let a = opt(1) Type(a) // ➔ "opt" ``` Each construction takes exactly one arm. Taking the **ground** arm says nothing about `T`, so `T` is solved to `never` — the narrowest member of the family, and (under `out`) a subtype of every other: ```epsil-live type opt = T | missing let b = opt(Missing) Type(b) // ➔ "opt" ``` Only **one** arm may mention a variable: with two open arms nothing at the construction site says which arm a value took, so neither variable could be solved. `type both = T | U` therefore declares nothing — it evaluates to an error value carrying an `unsupported-variable-position`. A variable may not stand in an intersection or a negation at all; an intersection is usually a constraint written in the wrong place, and the error says so — write a bound (`type box = …`) instead of `T & number`. Generic **functions** are supported: a `function` definition takes a type-parameter clause between its name and its parameter list, and the quantified names scope over the definition's head (its parameters, effect specifier, and return type): ```epsil function swap(x: T, y: U) -> tuple { (y, x) } swap(1, "a") ``` A type parameter may carry a ground bound (`function g(x: T) -> T`), which is enforced at every call. The equivalent full-type spelling is a `forall` annotation — `let f: forall T. (T) -> T = x |-> x`. ### When a type takes effect A `type` statement registers its name as the program is prepared, which is why the statements *after* it — in the same program or in a later cell — can annotate with it. A type the host declares on its own is visible to a program the same way, constructor and all. For the underlying representation, see [Type declarations](/implementation/#type-declarations). ## Diagnostics An invalid type inside an annotation position surfaces as a `type-annotation-error` diagnostic, offset-corrected to point at the offending token within the type text (not at the `:` or the declaration target): ```epsil x: notatype ``` produces a `type-annotation-error` diagnostic pointing at `notatype`.