Questions and answers

What Pagda is, what it promises, and what to do about the errors people hit first.

About Pagda

What is Pagda?

Pagda is a subset of Python with dependent types. A file that imports dependent is translated to Agda and checked by the agda program before it runs. Such a file can use the part of Python the checker understands. The pagda program is also a Python 3 interpreter, written in C, and runs ordinary Python files without checking them.

What is a dependent type?

A type that mentions a value. "A list of ints" is an ordinary type. "A list of exactly n ints" is a dependent type, and so is "a proof that i is less than len(xs)".

Do I need to know Agda?

No, to write programs. You write Python. Type errors come from Agda, and they use Agda's spelling for types, so the table of spellings is worth a look. Writing proofs is easier if you have met a proof assistant before, and Proofs starts from the beginning.

How does the name come about?

Python and Agda.

Is it Python?

Which Python programs does pagda run?

Ordinary files run on Pagda's own interpreter. It handles functions with every kind of parameter, closures, decorators, classes with multiple inheritance, generators, comprehensions, exceptions, with, match, f-strings, and imports of .py files and packages.

Its standard library is small: math, sys, time, random, os (part), json, collections, functools, itertools, dataclasses, typing, heapq, bisect, operator, string, copy, abc.

Missing: bytes, complex numbers, async, metaclasses, and modules such as re, enum, datetime and pathlib.

Is a checked file still a Python file?

Yes. It runs under python3 3.12 or newer with dependent.py beside it and prints the same output. There the types are not checked.

What can a checked file not hold?

Floats, sets, finally and with blocks, file access, assigning to a field of an object, and inheritance between classes. The reference has the full list. Code that needs these goes in an ordinary Python file, or behind a @trusted def.

Can checked and ordinary files work together?

Yes. An ordinary file can import a checked file and call its defs. A checked file reaches ordinary Python through defs marked @trusted, and can import other checked files.

What the check guarantees

What does an accepted file promise?

When a checked file is accepted and run as the main program: every call gets arguments of the annotated types, every match finds a case, every loop and recursion 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.

Where does the promise stop?

• An ordinary Python file can call a checked def with any arguments. Annotations are not checked while the program runs.
• A @trusted def is believed. It promises its result type, the same result for the same arguments, that it leaves its arguments unchanged, and that it does not raise.
• Very deep recursion still stops at Python's limit of 1000 nested calls.
• The promise rests on Pagda's translation giving each construct the same meaning the interpreter does. The tests compare the two on edge values.

Do the types slow the program down?

No. Checking happens before the program starts, and the result is remembered until the file changes. The program that runs is the Python you wrote.

Errors people hit first

"The checker cannot see that a condition this line relies on holds"

The line reads xs[i], divides, pops, or subtracts Nats, and nothing nearby shows it is safe. Put it under a test: if i < len(xs):, if xs:, if b != 0:, if k in d:.

"'xs' may be shared here"

The code changes a list or dict in place, and something else might hold the same object: it is a parameter, or it came from a call, or it was given a second name. Make a copy the function owns: xs = list(xs).

"this value may be None"

A value of type Optional[T] is being used as a T. Test it first: if x is None: .... After the test the name holds a plain value.

"the checker has to see that a while loop ends"

The loop is not one of the two shapes the checker handles by itself. Rewrite it as a for loop if you can. Otherwise end it with decreases(measure, proof); Proofs shows how.

Int !=< Nat, or Nat != Int

An int is being used where a Nat is wanted, or a number written out was taken as a Nat where an int is needed. Annotate the name (x: int = 0), or convert with to_nat(x) or abs(x).

"Agda could not work out a type here"

Usually an empty list or a None with nothing to say what it holds. Add an annotation: out: list[int] = [].

The project

Is Pagda open source?

Yes. The source is at github.com/jackmitchelwidman/pagda, under the MIT licence. Bug reports and questions go in the issues there.

How mature is Pagda?

It is new. There are no numbered releases, and it is built from source. Its test suite runs every example on this site, compares Pagda with python3, and holds a set of programs that must be refused.

How is it built?

Pagda is about 17,000 lines of C. Most of it is the interpreter: a parser, a bytecode compiler, a stack machine, and a garbage collector. The translator to Agda is one C file of about 5,000 lines. The Agda definitions that checked files are translated against are in a single Agda module that ships inside the program.

Which Agda does it need?

Agda 2.8.0. Pagda calls the agda program and uses none of Agda's libraries.