Types

slate is dynamically typed with a gradual checker: nothing has to be annotated, and what is annotated is checked twice — once by a pass before the program runs, and once by the machine when the value actually arrives.

The rule the checker obeys

The pass may only report what the machine would also refuse. A program that runs is never refused before it runs. Everything below follows from that one constraint: where the pass cannot be certain, it says nothing rather than guessing, and the machine still checks.

What that costs against TypeScript is worth saying plainly: TS catches a mistake on a path you never ran, and this only fires where the pass can prove the value is wrong or where that path executes.

Three deliberate exceptions, each an annotation the machine cannot check for you. An annotated var is held to its declared type at every assignment; every argument must fit the type a type parameter was solved to; and an object literal written where a shape is expected may carry only the fields that shape names. Each is a promise the program made in writing, and being held to it is what writing one is for.

type

A type is a shape with a name:

type Point = { x: number, y: number }
type Circle = { centre: Point, radius: number }

describe(v) = v match
    Circle -> s"a circle of radius ${v.radius}"
    Point  -> s"the point ${v.x}, ${v.y}"
    _      -> "no idea"

print({ x: 3, y: 4 } is Point)
print(describe({ centre: { x: 0, y: 0 }, radius: 2 }))
print(describe({ x: 3, y: 4 }))
print(describe("nothing"))

true
a circle of radius 2
the point 3, 4
no idea

It is TypeScript’s type — the same declaration, the same structural reading, asking for at least those fields. What differs is that slate’s is not erased: one declaration serves both the pattern and the check at a boundary, where a TypeScript app that reads an API response writes the shape twice, once as a type and once as a schema for the run.

Nothing of a type’s structure exists at run time. A name in pattern position is replaced by the pattern the type declared, while the program is compiled, so p is Point costs no instruction.

A type may not bind a name. type Tagged = { x: n } is refused: a name written inside a type would be introduced wherever the type is used. It is the rule an alternative of a | already followed.

export type is how an interface leaves the file it was written in, and both halves cross — the shape the compiler resolves and the value the name binds.

The type expressions

[T, U]

The brackets say how many. [string, integer] is an array of exactly two elements, so a third is as much a misfit as a wrong one — which is what makes type Pair = [string, integer] read the way it looks. A trailing ... is how a shape says and whatever else:

type Pair = [string, integer]
type Tail = [string, ...]

print(["a", 2] is Pair, ["a", 2, 3] is Pair, ["a"] is Pair)
print(["a", 2, 3] is Tail, [] is Tail)

true false false
true false

The count is checked wherever the shape is, so an annotation refuses the longer array where it arrives:

first(p: [string, integer]) = p[0]

print(first(["a", 2, 3]))

was declared [string, integer]

The brackets mean the same thing in every position, an annotation, an is test, a match arm, a for head and a destructuring val all reading the shape one way — which is the single grammar working, patterns and types being read by the same code. So a name a type declared carries the count with it, and mismatch reports the length rather than picking over the elements:

type Pair = [string, integer]

val [a, b] = ["x", 1]

val what = ["x", 1, 2] match
    Pair -> "a pair"
    _    -> "not a pair"

val why = Pair.mismatch(["x", 1, 2])

print(a, b)
print(what)
print(why[0].wanted, why[0].got)

x 1
not a pair
[string, integer] an array of 3

A rest is how an open-ended shape is written, and the elements before it are still checked — so [string, ...] is begins with a string.

array of T

An array of unknown length is not a tuple, and a rest pattern says nothing about the elements past the ones it writes, so a list of unknown length needs this:

type Tags   = array of string
type Counts = object of integer
type Grid   = array of array of integer

print(["a", "b"] is Tags, [1] is Tags, [] is Tags)
print({ a: 1 } is Counts, { a: "x" } is Counts)
print([[1, 2], [3]] is Grid)

true false true
true false
true

An empty container fits, every element of nothing fitting anything. A floor is said with an intersection: [any, ...] & array of string. The element pattern may not bind, running once per element.

A for over one types its variable, so for u in users where users: array of User makes u a User.

A range

A port is not an integer and a percentage is not a number, and the difference is where the value stops being one. 1..65535 says so, and reads the way the range you would write in a for head does:

type Port    = 1..65535
type Percent = 0..100

listenOn(p: Port) = "port " + string(p)

print(listenOn(8080))
print(50 is Percent, 101 is Percent)

port 8080
true false

Both ends are included, and ..< leaves the top one out — the same pair of spellings a range expression uses. Either end may be left off, which is what “no floor” and “no ceiling” are said with:

print(9 is 0..<10, 10 is 0..<10, 10 is 0..10)
print(-4 is ..0, 4 is 3.., 2 is 3..)

true false true
true true false

Whole ends mean whole numbers. 0..100 is written by somebody describing a percentage, so 2.5 is not one of them; a bound written with a point widens the whole range to any number:

type Percent  = 0..100
type Fraction = 0.0..1.0

print(50 is Percent, 2.5 is Percent)
print(0.25 is Fraction, 1 is Fraction)

true false
true true

The ends are the machine’s and the checker says only that a range is a number. A value it can see is a string is refused where it is written; a value it can only see is an integer is left to the check that runs where the value arrives.

pct(x: 0..100) = x

print(pct("half"))

`pct` takes integer here, and this is string

A range is a pattern like the rest of this table, so the same spelling is an arm of a match and the right-hand side of is.

? and |

A field the value need not have is marked ?. Present it must fit; absent the shape still holds — which a nullable union cannot say, tag: string | null still requiring the key to be there.

type Note = { title: string, pinned?: boolean }

print({ title: "a" } is Note)               // absent, and the shape still holds
print({ title: "a", pinned: true } is Note)
print({ title: "a", pinned: 1 } is Note)    // present, and does not fit

true
true
false

= is for a pattern that binds and ? is for one that tests, and each is refused where the other belongs.

The mark is the shape’s and not the declaration’s, so it reads the same written straight into an annotation — at a parameter, at a binding, or anywhere else a type goes:

greet(person: { name: string, age?: integer }) =
    if has(person, "age") then s"${person.name} (${person.age})" else person.name

print(greet({ name: "ada" }), greet({ name: "grace", age: 36 }))

ada grace (36)

A field the value need not have is still a field the shape knows, which is what makes a misspelling of one catchable: an object literal written at the spot may carry only the fields the shape names, and an optional one it never had is exactly the case that would otherwise pass.

greet(person: { name: string, age?: integer }) = person.name

print(greet({ name: "ada", aeg: 36 }))

`aeg` is not a field of { name: string, age?: integer }

A union may have null as an alternative, which is how a parameter says it will take nothing:

type Point = { x: number, y: number }
type MaybePoint = Point | null
type Shape = { side: number } | { radius: number }

print(null is MaybePoint, { x: 1, y: 2 } is MaybePoint, 3 is MaybePoint)
print({ side: 1 } is Shape, { radius: 1 } is Shape, { area: 1 } is Shape)

true true false
true true false

&

& is |‘s dual and binds tighter, matching only where every part does. A value picks up fields on its way down through a stack of functions, and this is how the one at the bottom says what it receives:

type Authed = { user: { id: integer } }
type Bodied = { body: string }

handle(req: Authed & Bodied) = req.user.id

print(handle({ user: { id: 7 }, body: "hi" }))

7

A part may bind, where an alternative may not: every part runs, so { a } & { b } binding both is sound.

A function type

integer -> integer is the type of n -> n + 1, and it is spelled the way the lambda is. One parameter needs no brackets; none or several are a bracketed list:

apply(f: integer -> integer) -> integer = f(1)
twice(f: (integer, integer) -> integer) = f(2, 3)
later(f: () -> string) = f()

print(apply(n -> n + 1), twice((a, b) -> a * b), later(() -> "hi"))

2 6 hi

The arrow is the loosest thing in a type and groups to the right. string | null -> integer is a function taking either — which is what a parameter usually means — and a union holding a function says so with brackets:

type Handler = string | null -> integer
type MaybeFn = (integer -> integer) | null

run(f: MaybeFn) = if f is null then 0 else f(2)

print(run(null), run(n -> n * 10))

0 20

Writing one down is what types the lambda handed to it, which is where most of what it buys shows up: the parameters flow inwards and what the body does with them is checked.

apply(f: integer -> integer) = f(1)

print(apply(n -> n + "x"))

`+` does not apply to an integer and a string

What is checked is the arity and the parameters, and deliberately not the result. A function’s own -> string is checked against what that function answers and never against what somebody who was handed it expected, so a mismatch there is a complaint no run could make. Where the result matters — f(cb) = cb(1) + 1 — it is read off the annotation and the arithmetic is checked on its own.

At run time a function type asks what it can ask: is this callable, and would it take a call of this size. What a function will do with what it is given is not a question about the value in front of you, which is why the parameters are the checker’s business and the count is both.

A function type may be written over a type parameter like any other type, in a definition’s own head or in a type of its own:

applyTo[T](f: (T) -> T, x: T) -> T = f(x)

type Wrap[T] = (T) -> T

val twice: Wrap[integer] = n -> n * 2

print(applyTo(n -> n + 1, 41), applyTo(s -> upper(s), "hi"), twice(21))

42 HI 42

A callback declaring more parameters than the type says it is handed is refused where it is written, which is the arity half above reading through the substitution:

type Handler[T] = (T, integer) -> null

each(xs: array of string, cb: Handler[string]) = cb(xs[0], 0)

each(["a"], (s, i, extra) -> print(s))

`each` takes (string, integer) -> null here, and this is (any, any, any) -> any

Annotating

Per parameter, and per result:

double(x: number) -> number = x * 2

print(double(21))

42

A result that does not fit what was promised is a fault where the answer was written:

name(p: { id: number }) -> string = p.id

print(name({ id: 7 }))

this answers string, and gave back 7

A parameter’s complaint lands where the value was handed over:

type Point = { x: number, y: number }

d(b: Point) = b.x

print(d({ x: 0 }))

`d` takes { x: number, y: number } here, and this is { x: integer }

A lambda’s parameters may be annotated and its result may not. The arrow already separates the parameters from the body, so there is nowhere for a result to be written; it is read off the body.

val g = (n: integer) -> n + 1

print(g(2))

3

A binding

val x: T = e and var n: T = e, checked where the value arrives and again by the pass that runs before the program does:

val name: string = "ada"
val tags: array of string = ["reading", "writing"]
var count: integer = 0

count += 1

print(name, tags, count)

ada ["reading", "writing"] 1

An annotated var is TypeScript’s let: the declared type is what the name holds for its whole life, so every assignment is checked against it rather than against what happens to be there.

var n: integer = 0

n = "later"

`n` was declared integer, and this is string

An unannotated var is left as it always was — the union of its initialiser and every value ever assigned to it — so a program that deliberately reuses a name for another kind is untouched.

A field

A class’s var and val and a data variant’s field are bindings too, and take every annotation a binding does. The check is made where the object is: the generated constructor tests each annotated field as it would an annotated parameter, and an assignment to one on an object whose class is beyond doubt is held to it as an annotated var‘s is. Classes and data types have the rest.

class Account
    var owner: { name: string }
    var balance: integer = 0
    var audit: (integer) -> boolean = n -> n >= 0

data Entry
    Deposit(amount: integer)
    Note(text: string)

val a = Account({ name: "ada" })

a.balance = 5

print(a.owner.name, a.balance, a.audit(a.balance), Deposit(3).amount)

ada 5 true 3

class Account
    var balance: integer = 0

val a = Account()

a.balance = 2.5

`balance` on `Account` was declared integer, and this is real

An object literal written where a shape is expected

A shape asks for at least its fields — except of a literal written at the spot, which may carry only the fields it names. An object that arrives through a name is one other places hold, so the fields this parameter does not want are somebody else’s business. A literal written here has no other reader, so a field the shape does not name is not a spare: it is a mistake, and the mistake it nearly always is is a misspelling.

type Style = { color: string, weight: integer }

use(s: Style) = s.color

print(use({ colour: "red", weight: 400 }))

`colour` is not a field of { color: string, weight: integer }, and an object literal written here may carry only the fields it names -- did you mean `color`?

It is TypeScript’s excess-property check, drawn in the same place and for the same reason, and it applies to a literal at an annotated parameter — including one typed by a solved type parameter — and to the value of a binding that declared a type.

Only a literal standing at the spot. A value reaching the same parameter through a name is structural as it always was; a literal built by a spread is a merge rather than a literal; and a literal nested inside one is the outer field’s business rather than the annotation’s.

type Spot = { x: number, y: number }

area(p: Spot) = p.x * p.y

val big = { x: 2, y: 3, z: 4 }
val some = { x: 2, z: 9 }

print(area(big), area({ ...some, y: 3 }))

6 6

A rest parameter

...rest: array of T describes the array, because the array is what the name holds: a call gathers what is left over into one, and it is checked once, where the gathering happened.

total(...ns: array of number) = reduce(ns, (a, b) -> a + b, 0)

print(total(1, 2, 3))

6

What the checker knows before the program runs

A call answers in terms of what it was given

filter, sorted, reversed, slice and pop all give back what they were handed, so the element type survives them and a mistake is caught where it is written — in either spelling, a method being checked as the free function it is:

f(xs: array of string) = xs.length

h(ns: array of integer) = f(ns.filter(n -> n > 1))

`f` takes array of string here, and this is array of integer

f(filter(ns, n -> n > 1)) draws the same complaint, a method being checked as the free function it is.

map(ns, n -> string(n)) is an array of string, the lambda’s result being read off its body.

A function’s answer is read off its body

Most functions never say what they answer, and the checker works it out anyway. A definition with no -> type gets the answer its body gives back, and that answer reaches every call to it:

shout(s: string) = s

tally(xs: array of integer) = xs.length

print(shout(tally([1, 2, 3])))

`shout` takes string here, and this is integer

An if or a match used for its value is worth what its branches agree on, so the same thing holds one level down:

tag(s: string) = s

size(n) = if n > 10 then 2 else 1

print(tag(size(20)))

`tag` takes string here, and this is integer

Writing -> type still wins, and the body is checked against it — an annotation is a promise, and this is where it is kept:

name() -> string = 1

print(name())

this was declared to answer string, and answers integer

Where the answer is not certain it is any, which fits everything. Two answer points that disagree give the whole thing up rather than making a union, so a function that gives back a string on one branch and a number on another is said nothing about:

label(n) = if n > 10 then "big" else 1

print(label(20), label(1))

big 1

The same holds for recursion, which is the one place writing the annotation buys something the checker cannot work out on its own: reading a recursive call means reading a result that is not known yet, so an unannotated recursive function answers any and an annotated one answers what it says.

depth(n) = if n <= 0 then 0 else depth(n - 1) + 1

count(xs: array of integer) -> integer = xs.length

print(depth(3), count([1, 2]))

3 2

An async function answers a promise and a generator answers a generator, whatever their bodies give back — what awaiting or stepping produces is not what calling produces. And a function whose body calls something the checker knows nothing about answers any in its turn, which is what keeps this from spreading a guess.

Narrowing

A test tells the checker something, and inside the branch where it held the name has the narrower type. x is string makes x a string there, so a call the wider type would have been refused for is accepted:

shout(s: string) = upper(s) + "!"

say(x: string | number) = if x is string then shout(x) else "#" + string(x)

print(say("hi"), say(3))

HI! #3

The side the test did NOT hold on takes that alternative away. A string | number that is not a string is a number, which is what makes the else branch of a union test worth writing:

double(n: number) = n * 2

widen(x: string | number) = if x is string then x.length else double(x)

print(widen("abcd"), widen(3))

4 6

A FIELD TESTED AGAINST A LITERAL NARROWS THE NAME IT IS READ OFF. Where the alternatives of a union disagree at one field — and the field is written as a literal in each of them — testing that field says which alternative the value is. This is the shape every result in slate has, so it is the narrowing a program meets most often:

type Read = { ok: true, value: string } | { ok: false, error: string }

shout(s: string) = upper(s) + "!"

report(r: Read) = if r.ok then shout(r.value) else "(" + r.error + ")"

print(report({ ok: true, value: "hi" }), report({ ok: false, error: "gone" }))

HI! (gone)

The discriminating field may be a boolean, a string or a whole number, and the test may be ==, !=, a bare read for its truth, or any of those under &&, || and !:

type Answer = { kind: "text", body: string } | { kind: "count", n: integer }

says(a: Answer) = if a.kind == "text" then a.body else string(a.n * 2)

print(says({ kind: "text", body: "hi" }), says({ kind: "count", n: 21 }))

hi 42

It says nothing wherever it cannot be sure, which is the rule every other narrowing follows. A field whose type is the bare word boolean rather than true decides nothing; an alternative that does not name the field at all is kept on both sides, an object pattern matching on the fields it names and ignoring the rest; an optional field is kept for the same reason, the value being free not to have it. And a var is left alone here exactly as it is everywhere else.

A comparison with null narrows the same way, and it is how most of the standard library is guarded — indexOf answers integer | null, so the else branch of the test is where the integer is:

tail(xs: array of integer, mark: integer)
    val at = indexOf(xs, mark)

    if at == null then return xs

    slice(xs, at + 1)

print(tail([1, 2, 3], 1), tail([1, 2, 3], 9))

[2, 3] [1, 2, 3]

A guard that leaves narrows the rest of the block, as the example above does: where the branch always returns, reaching the line below it means the test was false. && narrows its right operand and the branch after it, || narrows the else — reaching it means neither operand held — and ! swaps the two sides, so a test reaches everywhere it decides something:

trimmed(x: string | null) = if x != null && x.length > 0 then trim(x) else ""

named(x: string | null, fallback: string) = if x == null || x.length == 0 then fallback else upper(x)

print(trimmed("  a  "), trimmed(null), named("bo", "?"), named(null, "?"))

a  BO ?

Narrowing may only ever take a complaint away, never add one, which is what decides the three places it says nothing at all:

• A var with no annotation is never narrowed. Its type is already the union of everything ever assigned to it, and the branch that tested it may write to it — so a claim left standing over the assignment would be a stale one, refusing a program that runs.
• A name of type any stays any. There was nothing there to sharpen.
• A union that would empty is left alone. if x is string on an x: string has an else branch nothing reaches, and a complaint about code that never runs is a complaint no run could make.

report(s: string) = s

var m = 1

if m is number
    m = "text"
    print(report(m))

text

An annotated var is FOLLOWED rather than left alone, which is the other half of writing the annotation. var m: string | number carries two types: the one it was declared, which every assignment to it is held to, and the one it holds at the line being read — the initialiser’s type, then whatever the last assignment put there, narrowed by any test the line stands under. So a test narrows it like anything else, and a branch that writes to it says so itself:

report(s: string) = s

var m: string | number = 1

if m is string
    print(report(m))
else
    m = "text"
    print(report(m))

text

A parameter is followed the same way, carrying the same two types — the annotation is what may ever be assigned to it, and a test or an assignment says what it holds at the line being read. So a branch that narrows a parameter and then writes to it is describing the value it wrote, not the one the test proved:

report(s: string) = s

f(x: string | number)
    if x is number
        x = "text"
        return report(x)

    "no"

print(f(1))

text

The assignment is still measured against the annotation, which is what writing one asks for — a value outside it is refused on the line that wrote it:

f(x: string | number)
    if x is number
        x = true

    x

f(1)

`x` was declared string | number, and this is boolean

Below the branches the name holds the union of what each of them left it at, and a branch that always returns leaves nothing behind to join. Where that union cannot be worked out the declared type is what is left: a loop runs an unknown number of times, a try may stop anywhere in its body, and a closure that writes to the name runs at a time the block cannot place at all — so a name assigned inside any of the three reads as what it was declared, and a call wanting the narrower type is refused there. The assignment itself is always measured against the annotation, wherever it is written.

assert(c) narrows the lines below it exactly as an early exit does. It raises whenever c is false, so reaching the next line means c held — which is if !c then throw … written as a call:

double(n: integer) = n * 2

val at = indexOf([5, 6, 7], 7)

assert(at != null)
print(double(at))

4

That is slate’s own assert, a statement on its own line; a function a program writes and calls assert promises nothing, and a condition that says nothing about a name narrows nothing.

A bare value is a test of its truth, and slate’s truthiness is JavaScript’s: false, null, an absence, 0, NaN and "" are false and everything else is true. So the true side of if x takes null away, and the false side takes away whatever is never false — an object, an array, a function, a set, a map — which is what makes if !found then return the guard it reads as:

lookup(name: string) -> object | null = if name == "home" then { path: "/" } else null

describe(name: string)
    val found = lookup(name)

    if !found then return name + ": none"

    name + ": " + string(keys(found))

print(describe("home"), describe("away"))

home: ["path"] away: none

A string or a number tested false may still be one, the empty string and zero being false too, so the false side of a string | null says nothing:

shout(s: string) = upper(s)

quiet(x: string | null) = if x then "" else shout(x)

`shout` takes string here, and this is string | null

A path of fields narrows too — o.m, a.b.c, with no index and no ?. in it — under every test above: a comparison with null, an is, a bare read for its truth, and assert:

lookup(name: string) -> object | null = if name == "home" then { path: "/" } else null

val entry = { name: "home", target: lookup("home") }

if entry.target != null then print(keys(entry.target))

["path"]

Anything that could change the object between the test and the read ends the narrowing, and that is deliberately stricter than TypeScript, which lets a call keep one. A call — a method’s included — may change any object it can reach, and so may an await or a yield, which let other code run. A write to the root name ends the paths under it; a write to a field or through an index ends every path, the object written to being one a path may reach under another name. A function’s body runs whenever it is called and a loop’s next turn runs after its last one, so neither sees a path narrowed outside it. A name declared again is another root.

lookup(name: string) -> object | null = if name == "home" then { path: "/" } else null
note(s: string) = s

val entry = { name: "home", target: lookup("home") }

if entry.target != null
    note("found")
    print(keys(entry.target))

`keys` takes object | array here, and this is object | null

Where it errs, it errs toward accepting: a getter is code that runs at every read and may answer differently the second time, and an operator a class defined and a toString an interpolation asks for run code too — none of the three is counted by the rule above.

And the narrowing is a claim that can still be wrong, which is what says it is being checked at all:

double(n: number) = n * 2

say(x: string | number) = if x is string then double(x) else 0

`double` takes number here, and this is string

A function whose body is one test of its parameters narrows what a call hands it, exactly as the test written inline would — TypeScript’s inferred type predicate. Nothing is declared: the checker reads the body. The test may be a comparison with null, an is, a bare parameter read for its truth, ! of one, or several joined with &&, over parameters with no default and no dots. A call to one narrows in both branches, under !, && and ||, below an early exit, under assert, and for a path of fields handed to it:

isPresent(m: object | null) -> boolean = m != null
isText(v: string | integer) = v is string

count(m: object | null) = if isPresent(m) then keys(m).length else 0
size(v: string | integer) = if isText(v) then v.length else v + 1

print(count({ a: 1 }), count(null), size("abc"), size(4))

1 0 3 5

isPresent(m: object | null) -> boolean = m != null
lookup(name: string) -> object | null = if name == "home" then { path: "/" } else null

val entry = { name: "home", target: lookup("home") }

first(m: object | null)
    assert(isPresent(m))
    keys(m)

print(first(entry.target), if isPresent(entry.target) then keys(entry.target) else [])

["path"] ["path"]

It travels with the function — to another name a val gives it, to a lambda a val is bound to, and to a file that imports it. The narrowing a predicate makes outlives its own call, the body running nothing but the test; a path narrowed before that call is still ended by it, as by any call.

The false side is narrowed too, so a body is a predicate only where its answer being false says as much as the inline test being false would. && being false says nothing, so a body testing two parameters narrows both on the true side only. A truthiness test keeps the rule a bare value has: a string | null turned down may still be the empty string, and the false side says nothing:

filled(s: string | null) = s
shout(s: string) = upper(s)

say(s: string | null) = if filled(s) then "-" else shout(s)

`shout` takes string here, and this is string | null

A body of more than one statement is not a predicate, however simple; nor is one with an ||, a test of a field, or a test of anything but a parameter. A call to it narrows nothing:

isPresent(m: object | null)
    val ok = m != null
    ok

count(m: object | null) = if isPresent(m) then keys(m).length else 0

`keys` takes object | array here, and this is object | null

A function can say what its call proves

Where the body is more than one test, the result annotation says it instead — TypeScript’s explicit type predicate. -> p is T says the function answers a boolean, and that where a call to it answers true the argument given for parameter p is a T. On the false side the argument is not a T, so a union holding T as one of its alternatives loses that alternative there, which is TypeScript’s rule; a union T is not an alternative of loses nothing. The false side is read only where p is undeclared or declared as a union with T among its alternatives, which is where the machine holds a false answer to the claim (below):

type User = { id: integer, name: string }

isUser(v: User | string) -> v is User =
    if !(v is object) then return false
    val id = v.id
    id is integer && id > 0

greet(u: User) = "hello, " + u.name
shout(s: string) = upper(s)

say(v: User | string) = if isUser(v) then greet(v) else shout(v)

print(say({ id: 1, name: "ann" }), say("bob"))

hello, ann BOB

-> asserts p is T says the function answers nothing and that a call which returns at all proves the argument is a T — so the lines below a call written as a statement of its own know it, exactly as the lines below assert do. -> asserts p says the same of p‘s truth. A call to an assertion used as a value — in a condition, or bound to a name — answers nothing and narrows nothing:

type User = { id: integer, name: string }

ensureUser(v: any) -> asserts v is User =
    if !(v is object) || !(v.id is integer) then throw "not a user"

present(m: object | null) -> asserts m =
    if !m then throw "nothing here"

greet(u: User) = "hello, " + u.name

welcome(v: User | string)
    ensureUser(v)
    greet(v)

fields(m: object | null)
    present(m)
    keys(m)

print(welcome({ id: 1, name: "ann" }), fields({ a: 1 }))

hello, ann ["a"]

Either form reaches everywhere an inferred predicate does — a val naming it, an import and a re-export, a path of fields, !, && and ||, an early exit, and assert(isUser(x)) — and a spread, a named argument or a ?. call gets nothing from it. Where both could be read, the annotation wins. The words are not reserved: asserts means this only right after a definition’s -> and before a name.

The definition is held to its own annotation. p has to be one of its parameters, and T has to be something that parameter may hold:

isText(v: string | integer) -> w is string = v is string

`w` is not a parameter of `isText`, so `-> w is string` is about nothing a call hands over -- `isText` takes `v`

isText(v: integer) -> v is string = false

`v` is declared integer, and string is not one, so `v is string` could never be true

A predicate answers a boolean on every way out of it, and an assertion answers no value — it fails by throwing and holds by returning. Each answer that cannot be right is named where it is written:

isSmall(v: integer) -> v is integer =
    if v > 9 then return false
    "yes"

`isSmall` is a type predicate (`-> v is integer`), so every way out of it answers a boolean, and this one answers string

ensureSmall(v: integer) -> asserts v is integer =
    if v > 9 then throw "too big"
    v

`ensureSmall` is an assertion (`-> asserts v is integer`), so it answers nothing, and this answers integer

The machine holds every answer to the claim, where TypeScript trusts it. Each time a predicate or an assertion returns, the argument it was handed is checked against what it answered, on both back ends:

• -> p is T answering true faults where the argument is not a T;
• -> p is T answering false faults where the argument is a T — wherever a caller’s else branch takes T away, which is where p is undeclared or declared as a union with T among its alternatives;
• -> asserts p is T returning faults where the argument is not a T, and -> asserts p where it is falsy.

So a predicate that lies faults in its own body, rather than steering a caller into a branch the run would not take:

isText(v: string | integer) -> v is string = v is integer

print(isText(42))

`isText` answered true, but its claim `v is string` does not hold of what it was given -- a caller's then branch takes true to mean it does, so the predicate's body is what is wrong: `v` was 42

The argument checked is the one the call passed, so a body that reassigns its parameter is still answering about what it was handed. A predicate or an assertion that throws is never checked — the throw is what the caller gets. Where the false side is not held — isWhole(n: number) -> n is integer, whose parameter is no union — a call narrows on its true side only, so the checker and the machine agree about exactly which answers can be wrong.

An inferred predicate is not checked, and needs no check: its body is the test, so its answer is right by construction and it costs nothing. An explicit claim costs one store when the function is entered and one type test when it returns — two for a false answer that is held.

A method can be a predicate too

A method is a function handed the object it was called on as its first parameter, so everything above reaches it: a call checker.isUser(v) narrows v exactly as isUser(checker, v) would, whether the method’s body is one test or its annotation says so, and -> asserts works the same way.

this is T is a claim about the receiver, TypeScript’s spelling — this names whatever the method calls its first parameter, so -> self is T says the same thing. A body that is one test of that parameter is read as one, just as a function’s is, so isCircle(self) = self is Circle needs no annotation:

data Shape
    Circle(r: real)
    Square(side: real)

    isCircle(self) = self is Circle
    isSquare(self) -> this is Square =
        val yes = self is Square
        yes
    ensureCircle(self) -> asserts this is Circle =
        if !(self is Circle) then throw "not a circle"

radius(c: Circle) = c.r
side(q: Square) = q.side

either(s: Circle | Square) = if s.isSquare() then side(s) else radius(s)

round(s: Shape)
    s.ensureCircle()
    radius(s)

print(either(Square(2.5)), either(Circle(1.5)), round(Circle(0.5)))

2.5 1.5 0.5

type User = { id: integer, name: string }

class Checker
    var strict = false

    isUser(self, v: User | string) -> v is User =
        if !(v is object) then return false
        v.id is integer

greet(u: User) = "hello, " + u.name

val check = Checker()

say(v: User | string) = if check.isUser(v) then greet(v) else upper(v)

print(say({ id: 1, name: "ann" }), say("bob"))

hello, ann BOB

Which method a call reaches is worked out where the checker knows the receiver’s class: a val bound to Checker(), or a value whose type is a data type or some of its variants. The class’s own members are looked at first and then the chain its from names, which is where the machine looks. A receiver whose class is not known — one typed any, or reached through anything else — narrows nothing, and neither does a ?. call. A receiver that is a path of fields narrows as a path does, and a call still ends a path narrowed before it.

Where a subclass overrides a method, the class the checker knows decides, which is TypeScript’s rule. A receiver known to be the subclass reads the subclass’s method — its own predicate, or none if it declares none — and one known only as the base reads the base’s, whatever the run dispatches to. That is the same trust the claim itself is given.

The receiver is held to its class. What a data type’s method is called on is one of its variants, and what a class’s method is called on is an object, so a claim that could never be true of it is refused — and so is this on something that is not a method:

data Shape
    Circle(r: real)

    isText(self) -> this is string = false

`this` is the `Shape` the method was called on, and string is not one, so `this is string` could never be true

isText(v) -> this is string = v is string

`this` is the object a method was called on, and `isText` is not a method

A callback knows what it is handed

map, filter, forEach and the rest call their function with one element; sorted calls its comparator with two; reduce calls its function with a running value and an element. The checker says so, so a lambda written at the call gets its parameters typed from the array beside it — and what it does with them is checked:

h(ns: array of integer) = map(ns, n -> n * 2)   // an array of integer, not of any

print(h([1, 2, 3]))

[2, 4, 6]

What the callback does with what it was handed is checked:

g(ss: array of string) = map(ss, s -> s * 2)

`*` does not apply to string and integer

and so is its arity — in one direction. A function may declare FEWER parameters than its caller supplies, every call dropping what it cannot bind; see Functions. Declaring more is refused, there being nothing to fill them with:

q(ns: array of integer) = map(ns, (a, b, c, d) -> a)

`map` takes (integer, integer, array of integer) -> any here, and this is (integer, integer, array of integer, any) -> integer

The relaxation does not stop at a builtin, because the CALL is what makes it sound rather than the caller. A parameter the program annotated reads the same way: apply(f: (integer, integer) -> integer) = f(1, 2) takes n -> n, the call dropping the second argument exactly as map would. Only the floor is a limit, on either side.

None of that is a type variable. A builtin’s signature names an argument by position, and the type at that position is filled in at the call — no binding, no scope, nothing to write anywhere. What a program writes for itself is the next section.

Type parameters

first[T](xs: array of T) -> T is how a function you write says the same thing a builtin says: the answer is whatever the call was given.

first[T](xs: array of T) -> T = xs[0]

print(first(["ada", "grace"]), first([1, 2]))

ada 1

The parameters are solved from the arguments left to right, so a callback written at the call is typed from the arguments before it — and what it does with them is checked:

map2[A, B](xs: array of A, f: A -> B) -> array of B = map(xs, f)

print(map2(["a", "b"], s -> upper(s)))

["A", "B"]

They are declared in one place and nowhere else — [T] after the name of a definition or a type — and there are no bounds, no variance and no defaults. A generic type is used by giving it what it is generic over, and the shape that comes out is the shape both declarations describe:

type Pair[A, B] = { first: A, second: B }

show(p: Pair[string, integer]) = s"${p.first} is ${p.second}"

print(show({ first: "ada", second: 36 }))
print({ first: "ada", second: "x" } is Pair[string, integer])

ada is 36
false

What it is generic over may stand anywhere in the type, not only at a field. The declaration is an ordinary type expression with a name in it, so an array, a union, array of T and a function type are all things a generic type may be — and what comes out is substituted where the type is used, in an annotation, an is test or a match arm alike:

type Pair[T]   = [T, T]
type Result[T] = { ok: true, value: T } | { ok: false, error: string }
type Bag[T]    = array of T

read(r: Result[string]) = r match
    { ok: true, value }  -> value
    { ok: false, error } -> s"!${error}"

print([1, 2] is Pair[integer], ["a", "b"] is Pair[integer])
print([1, 2, 3] is Bag[integer], [1, "a"] is Bag[integer])
print(read({ ok: true, value: "hi" }), read({ ok: false, error: "no" }))

true false
true false
hi !no

A generic type used without its arguments is refused rather than quietly erased, because a check that passes for the wrong reason is worse than no check:

type Pair[A, B] = { first: A, second: B }

show(p: Pair) = p.first

`Pair` is generic over 2 types, so it needs them here

Every argument must fit the type the parameter was solved to

A type parameter is solved from the arguments, and every one of them has to be contained in the answer. The candidates are gathered across the whole call and the one that every other candidate fits is chosen; where there is no such candidate the call is refused, naming the parameter, what it was taken to be, and the argument that disagrees:

pair[T](a: T, b: T) -> array of T = [a, b]

print(pair(1, "x"))

`T` is integer from an argument before this one, and this is string

A union is still an answer where the PROGRAM declared one, because then it is a candidate like any other and the value beside it fits:

pair[T](a: T, b: T) -> array of T = [a, b]

val mixed: integer | string = 1

print(pair(mixed, "x"))

[1, "x"]

fits is the same relation used everywhere else on this page, so an integer does not fit a real. pair(1, 2.5) is refused for that reason, and number is the type that takes both — which is what to annotate with where a call means to mix them:

pair[T](a: T, b: T) -> array of T = [a, b]

print(pair(1, 2.5))

`T` is integer from an argument before this one, and this is real

What a type parameter still does not do

It is erased, so nothing at run time knows it was there. The machine sees values, not the calls that were made — which is exactly why the check above happens while compiling or not at all.

So x is T cannot be asked, and it is refused where it is written rather than answering something. There are no type arguments at a call either — first[string](xs) is an index followed by a call, and no grammar can have both — so they are solved from the arguments or not given.

Inside the definition a T is a value nothing is known about, which is what makes upper(xs[0]) in a generic function perfectly legal: T may be a string, and refusing a program that runs is the one thing the checker may not do.

It reads the rest of the block before it says what a name holds

• A var is the union of its initialiser and every value ever assigned to it, so a counter stays an integer through += 1 and n++ and a wrong call is refused before the program runs. A var the program reassigns to another kind is said nothing about. An ANNOTATED var is what it was declared and every assignment is checked against that, which is the one place the pass refuses something the machine would have run: the annotation is a promise the program made, and being held to it is what writing one is for.
• An array literal says what it was built out of, so map([1, 2], n -> n * 2) types its callback and first([1, 2]) answers an integer. Elements that disagree make a union and one that is not known gives the whole thing up. A NAME does not keep it: an array is mutable and outlives the line that built it, so the element type is dropped where a literal is bound to a name — the rule an object’s shape already follows. An annotation is not dropped, being a promise the machine checks.
• A local object’s fields are known for as long as nothing can have made them stale: its name never mentioned except to read a field off it, so nothing else holds the object and no field of it is ever written. o with { … } is a mention.
• An annotated parameter’s shape is not carried past the call. The object came from somewhere else, the caller may hold another name for it, and the annotation is checked on the way in and says nothing about after.

A function from another file is checked as one written here

A call to an imported function gets the checks a call beside its definition gets: too few or too many arguments, and an argument that does not fit an annotated parameter, are refused before the program runs. The signature is the one the exporting file was checked with — its defaults, its rest parameter and the answer read off its body included — so this holds for a quoted file, a package, and one of slate’s own modules written in slate alike, and for a name a file re-exports.

• Only a function crosses. Any other exported value is any in the importing file (unless its type names an opaque type): the importer holds a snapshot it may change, so a shape read at home could be wrong by the time it is used.
• An unannotated parameter takes anything, there as here.
• A function that throws on every path never answers, imported or not, so a guard ending in a call to one — if n == null then refuse("…") — narrows n below it exactly as a throw would.
• import * as m binds m as any, so m.f(1, 2) is a call through a value and is not checked.

Where it steps aside

• A call that spreads — f(...xs) — is not checked for arity, the count being a run-time fact.
• A receiver whose type is any is never asked what methods it has.
• An object’s field names are the program’s, so an object is never asked whether it has one.
• A method name is refused before it runs where the receiver’s kind is certain — "abc".push(1), date(…).hour() — because that asks the machine’s own question: the dispatch table is one table.

A type is a value under its own name

Which is what makes the declaration the validator — nothing written twice, and no schema library to keep in step with it:

type Note = { title: string, pinned?: boolean }

print(Note.test({ title: "a" }))
print(Note.mismatch({ }))
print(Note.name())

true
[{path: "title", wanted: "string", got: "nothing"}]
Note

mismatch collects every reason rather than stopping at the first, because a person filling in a form wants to be told about all of it at once, and path says where in the value each one is.

Those three are the whole surface: a shape’s fields cannot be read back out, so nothing can grow to depend on the structure of a type. is is deliberately not extended to take one — a bare name in pattern position binds, so v is s would match everything — and shape is a type word, so s is shape asks whether s is one of these.

This covers all three declarations that name a type, so a class name and a data name answer the same three about themselves — the shape being the very pattern is tests, interned where the declaration stands:

class Point
    var x
    var y

data Failure
    NotFound(what)
    Empty

print(Point.name(), Point.test(Point(1, 2)), Point.test({ x: 1, y: 2 }))
print(Failure.test(Empty), Failure.mismatch(3))
print(NotFound.test(NotFound("a")), NotFound.test(Empty))

Point true false
true [{path: "", wanted: "Failure", got: "integer"}]
true false

A class and a variant ask a nominal question — was this value made from that declaration — so test is is and a mismatch against one names the type and stops. There is nothing more useful to say about a value that was made from something else.

A static the class itself declares wins over all three, the shape answering only where the object’s own fields and its whole proto chain have said nothing. So test and name are still words a class may use for its own purposes.

shape as a type word takes all three, so f(s: shape) is how a function says it wants one — and Point is shape is true where Point(1, 2) is shape is not, a value being what the type describes rather than the type.

Interfaces

An interface, in the sense of a set of operations, needs nothing further — functions are values, so type Drawable = { draw: function } is one. A class promises one with is in its header, which is TypeScript’s implements and is checked where the class is written.