Types
Epsil does not have its own type system: it uses the Compute Engine type language, 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:
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:
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:
function roll(n: integer) random -> integer { Random(n) }
Effect labels are part of the function type. See Effect specifiers for declaration syntax and the function type guide 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:
xs: list<integer>
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<integer>, set<string>), 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<T>(…) 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<never>, 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<finite_integer>
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:
Nothingmeans “no value here” and is removed from function arguments and collection literals.Missingis a position-preserving missing value. Its type ismissing.NaNis the numeric form of an absent or undefined result. Numeric operations and missing numeric fields generally normalize absence toNaN.
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.
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.
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.
Reach for type alias to shorten a type you write often
(type alias grid = list<list<number>>), 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:
(And type alias = tuple<number, number>, 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:
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:
An alias constructor is a checked cast instead of a tag: it validates the arguments against the definition and hands back the plain value.
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 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:
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:
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:
type point = tuple<x: number, y: number>
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, not as a parse error.
To read the parts back, match on the
constructor — a constructor pattern is an ordinary operator pattern, and
binds one variable per field:
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:
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:
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:
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:
Re-running a type statement for a name that an earlier type statement
declared replaces the earlier definition, constructor included —
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<integer> means exactly
tuple<integer, integer>, and that expansion is what type displays and
error messages show:
type alias Pair<T> = tuple<T, T>
let p: Pair<integer> = (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:
type alias Keyed<T: number> = tuple<string, T>
type alias Table<T: integer> = list<Keyed<T>>
let rows: Table<integer> = [("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 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<integer> is never expanded, which is
what lets its body be recursive.
The constructor is quantified — tree: forall T. (T, list<tree<T>>) -> tree<T> — 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:
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:
Variance. A parameter may carry an in/out/inout marker saying how
two applications relate: out (covariant) makes a tree<integer> usable
where a tree<number> 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.
type tree<out T> = tuple<value: T, children: list<tree<T>>>
type sink<in T> = tuple<accept: (T) -> 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:
type events<T> = tuple<log: list<T>, 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<inout T> = … accepts the definition, at the
cost of events<integer> no longer being usable as an events<number>.
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<number> = tree(1, []) works only because the tree<finite_integer> it
builds is a tree<number> 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:
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:
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> = 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<T: number> = …) 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):
function swap<T, U>(x: T, y: U) -> tuple<U, T> { (y, x) }
swap(1, "a")
A type parameter may carry a ground bound (function g<T: number>(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.
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):
x: notatype
produces a type-annotation-error diagnostic pointing at notatype.