A subset of Python with dependent types

Python that is checked before it runs.

A Pagda file is a Python file. It is type-checked by Agda before it runs, and its types can state facts about values: this list has ten items, this index is inside the list, this divisor is never zero. The price is a smaller language: no objects that change, no inheritance, no floats.

Get started Take the tour

hero.pychecked

def mean(xs: list[int]) -> int:
    if xs:                            # the test is the proof
        return sum(xs) // len(xs)     # so this cannot divide by zero
    return 0


class Vec[A, n: Nat](Data): ...       # a list whose length is in its type


@constructor
def Nil[A]() -> Vec[A, 0]: ...


@constructor
def Cons[A, n: Nat](head: A, tail: Vec[A, n]) -> Vec[A, n + 1]: ...


# n + 1 is never 0, so this takes only a non-empty Vec
def first[A, n: Nat](xs: Vec[A, n + 1]) -> A:
    match xs:
        case Cons(x, _):
            return x


assert mean([3, 4, 8]) == 5           # checked before the program runs
print(mean([3, 4, 8]), first(Cons("a", Nil())))

$ pagda hero.py

5 a

What the checker catches

Each program on the right was run through pagda to build this page. The panel under the code is what it printed.

An index past the end

xs[i] needs a reason that i is inside the list. A test in the code is a reason. Without one, the file is refused and nothing runs.

f_index.pychecked

def get(xs: list[int], i: Nat) -> int:
    if i < len(xs):
        return xs[i]
    return 0


print(get([4, 8, 15], 1), get([4, 8, 15], 7))

$ pagda f_index.py

8 0

f_index_bad.pyrefused

def get(xs: list[int], i: Nat) -> int:
    return xs[i]

$ pagda f_index_bad.py

  File "f_index_bad.py", line 6
    return xs[i]
TypeCheckError: (i < len xs) != true of type Bool
when checking that the expression refl has type (i < len xs) ≡ true
The checker cannot see that a condition this line relies on holds. xs[i] needs i < len(xs), d[k] needs k in d, // and % need a divisor that is not 0, a - b on Nats needs b <= a, and an assert inside a function needs its condition. known(c) gives the proof inside 'if c:' or 'while c:', with c written the same way. Put the code under an 'if' that tests it.

A None used as a value

A function that may return None says so in its type. The caller has to test for it, and after the test the name holds a plain value.

f_none.pychecked

def find(names: list[str], prefix: str) -> Optional[str]:
    for name in names:
        if name.startswith(prefix):
            return name
    return None


def shout(names: list[str], prefix: str) -> str:
    hit = find(names, prefix)
    if hit is None:
        return "nobody"
    return hit + "!"


print(shout(["ada", "bob"], "b"), shout(["ada"], "z"))

$ pagda f_none.py

bob! nobody

f_none_bad.pyrefused

def find(names: list[str], prefix: str) -> Optional[str]:
    for name in names:
        if name.startswith(prefix):
            return name
    return None


def shout(names: list[str], prefix: str) -> str:
    return find(names, prefix) + "!"

$ pagda f_none_bad.py

  File "f_none_bad.py", line 13
    return find(names, prefix) + "!"
TypeCheckError: this value may be None, and a value that is never None is needed here. Test it first with 'if ... is None:' or 'if ... is not None:'.

A value of the wrong shape

A type can mention a value. Vec[A, n + 1] is a list that has at least one item, so first cannot be called on an empty one.

hero_refused.pyrefused

class Vec[A, n: Nat](Data): ...


@constructor
def Nil[A]() -> Vec[A, 0]: ...


@constructor
def Cons[A, n: Nat](head: A, tail: Vec[A, n]) -> Vec[A, n + 1]: ...


def first[A, n: Nat](xs: Vec[A, n + 1]) -> A:
    match xs:
        case Cons(x, _):
            return x


print(first(Nil()))

$ pagda hero_refused.py

  File "hero_refused.py", line 22
    print(first(Nil()))
TypeCheckError: zero != (suc _n_15) of type Nat
when checking that the expression Nil has type
Vec _A_14 (suc _n_15)

A claim that is false

A return type can be a statement, and the function body is its proof. This one says that n + 0 equals n for every n.

f_proof.pychecked

def plus_zero(n: Nat) -> n + 0 == n:
    if n == 0:
        return refl()
    return cong(suc, plus_zero(n - 1))


print(plus_zero(5))

$ pagda f_proof.py

Refl()

How it works

A file opts in by importing dependent. Every other file runs as ordinary Python.

You write PythonClasses, loops, lists, dicts, f-strings, with type annotations on every def.
Pagda translates itThe file becomes an Agda program that means the same thing.
Agda checks itAn error is reported against the Python line it came from.
The Python runsThe types have done their work, so they cost nothing while the program runs.

What an accepted file promises

Every call gets arguments of the annotated types.
No index, key, pop or division fails.
No None is used as a value.
Every match finds a case.
Every loop and recursion ends.
Every assert holds.
The only exceptions are the ones the file raises.

Where the promise stops

An ordinary Python file can call a checked file with anything.
A def marked @trusted is believed without being read.
Checked files are a subset of Python. Changing an object's fields, inheritance, floats, sets and file access are left out.
Pagda is new. There are no numbered releases yet. The source is open, under the MIT licence.

Read the limits in full

Try it

Pagda is built from source with a C compiler and make. Checking needs Agda 2.8.0.

git clone https://github.com/jackmitchelwidman/pagda
cd pagda
make                      # builds ./pagda
./pagda hello.py          # check, then run
./pagda --check hello.py  # check only

Get started