Language reference

Everything a checked file can hold. This page is built from the project's README, so the two always agree.

The first lines

from __future__ import annotations, then from dependent import .... After that a checked file may import names from other checked files: from shapes import Point, width. It has no other imports.

A program

def main() -> None:
    stock = [Item("pen", 3, 10), Item("ink", 12, 2)]
    for item in stock:
        print(f"{item.name}: {item.price}")

if __name__ == "__main__":
    main()

A def can return None, call other defs for what they do, and print. What print writes is not part of what the checker reasons about. Its arguments are checked like any other expression.

Numbers, strings and booleans

• Nat is 0, 1, 2 and so on. It has + * // % ** and the comparisons. if n == 0: splits into the zero case and the other case, and in the other case n - 1 is allowed. Elsewhere a - b needs the checker to see that b is not larger than a (see Operations that can fail). monus(a, b) is subtraction that stops at 0.
• int is any whole number. It has + - * // % **, unary minus, abs, min, max and the comparisons. // and % round the way Python does.
• A literal like 3 is a Nat unless the place it stands in needs an int. A Nat used where an int is wanted is converted. Going the other way is written to_nat(x), which gives 0 for a negative x, or abs(x).
• Locals follow their use. A local that is given an int anywhere in a function is an int from its first assignment, so s = 0 followed by s += x works for an int x. xs = [1, 2] is a list of ints when xs is later passed where a list[int] is wanted. best = None followed by best = x makes best an Optional.
• str has +, * by a number, ==, <, in, len, s[i], slices, looping over the characters, str(n), f-strings, and the methods startswith, endswith, join, split(sep), replace(old, new), strip, lstrip and rstrip. split and replace take the text to look for written out, and not empty.
• f-strings hold str, Nat, int and bool values. Inside print(...) they can hold anything, and can use format specs.
• bool has and, or, not. In a condition, a list, dict or string counts as true when it is not empty, and a number when it is not 0.
• There are no floats, so / is refused.

None and Optional

Optional[T] (or T | None) is a value that is a T or None. A plain value is accepted where an Optional is wanted. Going the other way needs a test:

def price_of(items: list[Item], name: str) -> int:
    item = find(items, name)          # Optional[Item]
    if item is None:
        return -1
    return item.price                 # here item is an Item

d.get(k) gives an Optional. T has to be a type the checker knows, and not a name in square brackets: Python cannot tell "None" from "a None inside", so an Optional of an Optional would not mean the same in both languages.

Lists, tuples and dicts

• list[A]: [1, 2], xs + ys, len(xs), x in xs, xs[i], xs[-1], xs[a:b] (ends may be negative), comprehensions, sum, any, all, sorted (of Nat or int), list(...), and match xs: with case []: and case [first, *rest]:.
• tuple[A, B]: (a, b), a, b = t, a, b = b, a, t[0], and case (a, b):. Two or more parts.
• dict[K, V]: {k: v}, d[k], k in d, d.get(k), d.get(k, default), len(d), and looping over d, d.items(), d.keys() or d.values(). Keys keep the order they were first added. A key is a Nat, int, bool, str, or a tuple of those: the kinds Python can use as keys. d.get(k) needs values that are never None, since it answers None for a missing key.
• range, enumerate, zip, reversed and the dict views can stand after in of a loop or a comprehension, and inside list(...). On their own they are not lists, and Python would not call them equal to one, so they are refused as plain values. For the same reason two dicts cannot be compared with ==.

Operations that can fail

xs[i] fails when i is past the end, xs[-1] and xs.pop() when the list is empty, d[k] when the key is missing, // and % when the divisor is 0, and a - b on Nats has no answer when b is larger. Agda has no failing, so each of these needs a reason it is fine. The checker finds the reason by itself when:

• the code is under a test of the condition: if i < len(xs):, if xs:, if k in d:, if b != 0:, if b <= a:. The test can be an if, a while, or the test of x if c else y;
• an earlier part of the same and tests it, as in while i < len(xs) and xs[i] != t:, or an earlier part of an or rules the bad case out, as in not xs or xs[0] < 10;
• the loop is for i in range(len(xs)): and the body reads or writes xs[i];
• a parameter states it: def at(xs: list[int], i: Nat, ok: (i < len(xs)) == True) -> int:. The caller passes known(i < len(xs)) from inside its own test;
• an assert states it, where Agda can work the assert out;
• Agda can work the condition out, as in [1, 2, 3][1] or n // 2.

An int used as an index needs both ends: if 0 <= i < len(xs):. Otherwise the line is refused with a message that lists what such lines need.

Changing a list or dict

xs.append(x), xs.extend(ys), xs.insert(i, x), x = xs.pop(), xs += ys, xs[i] = v, xs[i], xs[j] = xs[j], xs[i], xs.sort(), xs.reverse(), xs.clear() and d[k] = v are allowed on a local name. In the Agda text the name simply gets a new value.

The Python still runs as Python, where these change the object itself, and every other holder of that object sees the change. Agda's version and Python's agree only when there is no other holder. So the checker allows a change only on a list or dict that the function made itself (a literal, a comprehension, list(xs), xs.copy(), a slice, a + b, sorted(...)) and has not since given another name, passed to a function, put inside another value, or used in a lambda or inner def. A parameter, or the result of a call, has to be copied first: xs = list(xs). A loop cannot change the list it is running over.

Loops

• for runs over a list, a dict, a string, range(...) and the like. break, continue and return work inside it. The names the body assigns must have been assigned before the loop, and each keeps one type through the loop.
• The loop variable is gone after the loop. To keep its last value, give it to another name inside the loop.
• while needs a reason to end. The checker sees it by itself for the two commonest shapes, also when the test has more parts joined by and:

i = 0
while i < len(xs):        # a Nat counted up to a limit the loop does not change
    ...
    i += 1                # the last statement

while k > 0:              # an int counted down to 0
    ...
    k -= 1

• Any other while ends with decreases(measure, proof). The measure is a Nat worked out from the loop's variables. The proof shows (measure at the end of a pass < measure at the start) == True. lemmas has two ready ones, monus_step and down_step.
• A for loop at the top level may hold print statements and further for loops.
• In the Agda text a loop is one expression that folds the body over the items. So if inside a loop does not change what the types know (see Conditions), and case _: return unreachable() is not available there. A property of a loop's result is proved by writing the loop as a recursive function instead.

Exceptions

class ParseError(Exception): ...

def parse(text: str) -> int:
    if not text:
        raise ParseError("nothing to parse")
    ...

def parse_or(text: str, default: int) -> int:
    try:
        n = parse(text)
    except ParseError as e:
        print("bad input:", e)
        return default
    except Exception:
        return default
    return n

• raise takes an exception class and at most a message: raise ValueError("bad"). The built-in classes are Exception, ValueError, TypeError, RuntimeError, IndexError, ZeroDivisionError, ArithmeticError, LookupError and NotImplementedError. A file adds its own with class MyError(Exception): ..., and one of those can be the base of another.
• try / except / else work as in Python: the first clause that names the exception's class, or a class it is built on, handles it. except Exception: and a bare except: catch everything. A bare raise in an except block raises the same exception again.
• In an except block, str(e) and f"{e}" give the message, and print(e) prints it. The name is gone after the block, as in Python.
• A call to a def that can raise stands on its own: as a statement, as the whole right side of an assignment, or as the whole value of a return. return parse(a) + 1 is refused; write n = parse(a) and then return n + 1.
• A def that calls one that can raise can itself raise, unless the call is inside a try whose clauses include one that catches everything. The checker cannot see that a list of named classes covers all that a called def raises.
• An exception that nothing catches ends the program, as in Python. That is allowed for a call that stands alone at the top level, such as main().
• Only raise raises. xs[i], d[k], // and the rest still need a reason they cannot fail, and never raise in a checked file.
• Not available yet: finally, raise ... from ..., an exception with more than one argument, raise inside a def that is inside a function, and a loop inside a try whose body can raise (move the loop into its own def).
• In the Agda text a def that can raise gives back either its value or the exception. From a try on, the rest of the def is one expression, so an if after it does not change what the types know.

Classes

• A class with fields is written with @dataclass. Fields are name: type lines, and a field's type can mention the fields before it, so a field can hold a proof about another field. It can have methods, whose first parameter is self. Point(1, 2), Point(x=1, y=2), p.x, p.norm(), case Point(a, b): and (when every field can be compared) == all work. Fields cannot be assigned to: replace(p, x=3) gives a new value with that field changed.
• A family of types is class Name[params](Data): .... Each constructor is a def marked @constructor with ... as its body. Its parameters are the fields, and its return annotation says which member of the family it builds.
• Names in square brackets (def f[A, n: Nat], class Box[A]) exist only for the checker. They can appear in annotations and nowhere else, because they are gone when the program runs. A name without a : bound is a type.

Functions

• Every parameter and the result must be annotated. Every path must return, unless the def returns None.
• Default values are numbers, strings, True, False or None, written out. Arguments can be passed by name.
• A def inside a function can use the names around it. It cannot call itself, and it cannot change a list or dict of the outer function in place.
• A lambda or inner def made inside a loop cannot use a name that the loop sets. In Python such a function sees the name's value at the time it is called, which is usually the last one. Pass the value in as an argument.
• Function types: Fn[A, B, C] means the same as Callable[[A, B], C]: the last item is the result. An argument can be given a name, and the types after it can then use it. Fn[k: Nat, Vec[A, k]] takes a number k and gives a Vec of that length. The named form is for annotations only.
• Inside a lambda whose argument types the checker cannot see, numbers are taken to be Nat. Use a def for a function on ints that is passed to a generic function.

Conditions and proofs

• In an annotation, a == b is the type of proofs that a equals b. refl() proves a thing equals itself. sym, trans, cong and subst combine proofs, and match p: case Refl(): uses one.
• Inside if c: (outside a loop) the checker has replaced c by True in the types it still has to check, and by False in the else part. So a proof about a function that tests a < b can test a < b itself and finish each branch separately. if a and b: and if a < b < c: count as several tests, one inside the other.
• known(c) inside if c: or while c: is the proof that c is true. In the else part, known(not c) is the proof for the other way. match decide(c): with case Yes(p): and case No(p): does the same job and names the proof.
• assert c inside a function has to be a condition the checker can see holds. After it, the rest of the function may rely on it.
• Impossible cases: case _: return unreachable() is accepted only when Agda can see that no value reaches it.
• lemmas is a built-in checked file of ready-made proofs: plus_zero, plus_suc, plus_comm, plus_assoc, times_zero, times_one, lt_suc, lt_irrefl, lt_asym, lt_trans, monus_step, down_step, append_nil, append_assoc, len_append, false_is_not_true, true_is_not_false. Import the ones needed by name.

Holes

hole() stands for a part that is not written yet. The checker checks the rest of the file, then lists each hole with the type it needs and the names in scope there. A file with a hole does not run.

TypeCheckError: this file has 1 hole, so it was not run.
line 8: hole() needs a value of type
  n₁ + 0 ≡ n₁
with these names to build it from:
  n₁ : Nat

Calling unchecked Python

A checked file cannot import an ordinary Python file. It can hold a def marked @trusted. The checker reads its annotations and nothing else, so the body can be any Python, including imports, loops over anything, and exceptions.

@trusted
def file_size(path: str) -> Nat:
    import os
    return os.path.getsize(path)

Four things are taken on trust: that the def returns a value of the type it says, that the same arguments always give the same result, that it does not change the lists and dicts it is given, and that it does not raise. Agda treats it as a function, so assert f(x) == f(x) passes the check whatever f does.

The top level

name: T = value, calls, print(...), assert, classes, defs, and for loops that print. An assert is checked by Agda before the program runs. A final if __name__ == "__main__": block may hold the same statements. from dependent import * brings in every name of the module, including Fn, Dec, Yes, No, decide, known, hole, dataclass, replace, trusted and Optional. A file that defines its own Yes has to import the names it uses one by one.

What the check covers, and what it does not

• Covered: if a checked file is accepted and run as the main program, every call inside it gets arguments of the annotated types, every match finds a case, every recursion and loop ends, no index, key, pop, division or subtraction fails, no None is used as a value, every assert holds, and the only exceptions are the ones the file raises with raise.
• @trusted defs: the guarantee holds only as far as each one keeps its four promises.
• Callers outside: an ordinary Python file can import a checked file and call it with anything. Annotations are not checked while the program runs. An outside caller can also keep a list it passed in and change it later.
• Deep recursion: Agda proves that a recursion ends. The interpreter still stops at 1000 nested calls with RecursionError. A checked file cannot import sys, so raise the limit from an ordinary file that imports the checked one.
• Large numbers in asserts: Agda works an assert out itself, and it counts Nat values one step at a time in proofs. An assert over large numbers can be slow.
• The translation: the guarantee rests on src/agda.c giving each construct the same meaning the interpreter does, and on lib/dependent.py matching lib/PagdaPrelude.agda. The tests compare the two on edge values through assert, which Agda and Python each work out. pagda always loads its built-in dependent, so a dependent.py in the script's folder is ignored.

Missing from checked files

• Floats, bytes, sets, and string methods beyond the ones listed (no upper, lower, format, int("12")).
• finally, with blocks, and anything that touches the outside world except print. Use a @trusted def.
• Assigning to a field, inheritance between @dataclass classes, field defaults, and methods named __x__ (Python calls those by itself).
• Changing a list that sits inside another list (grid[i][j] = v), and changing a list or dict that might be shared.
• list.remove, dict.pop, del, slices with a step, tuples of one part, range with a step.
• Loop state whose type changes from pass to pass, and else on a loop.
• A def inside a function that calls itself, or has more than 4 parameters.
• Explicit type arguments at a call, as in ident[Nat](3). The checker always works them out.
• A constructor field that holds a type. Agda reports that Set₁ does not fit into Set.
• Function types with more than 4 arguments.
• case ... if, mapping patterns, and keyword patterns.
• Two checked files that import each other.

Each of these is refused with a message that names the Python line.

Reading the error messages

Type errors come from Agda, with positions mapped back to Python lines. Agda writes some things differently: