Get started

Build the pagda program, run a file, then check one.

What you need

A C compiler and make. gcc or clang. This is all that is needed to build Pagda and run ordinary Python files.
Agda 2.8.0. Needed to check files. The Agda documentation explains how to install it. Pagda uses none of Agda's libraries.
Python 3.12 or newer. Only for running Pagda's own tests, which compare its output with python3.

Build

The source is on GitHub.

git clone https://github.com/jackmitchelwidman/pagda
cd pagda
make          # builds ./pagda
make test     # runs every test

The result is one program, pagda, with its standard library inside it. Copy it anywhere on your PATH.

Run a Python file

pagda script.py        # run a file
pagda -c 'print(1)'    # run a string
pagda                  # interactive prompt

A file that does not import dependent runs as ordinary Python 3. Pagda's interpreter covers the core of the language and a small standard library. The FAQ lists what is in and what is out.

Your first checked file

A checked file starts with two lines. The first makes Python leave annotations alone. The second asks for checking.

from __future__ import annotations
from dependent import *

Save this as t01_hello.py. The Copy button gives the whole file, with those two lines.

t01_hello.pychecked

@dataclass
class Item:
    name: str
    price: int
    count: Nat


def total(items: list[Item]) -> int:
    t = 0
    for item in items:
        t += item.price * item.count
    return t


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


if __name__ == "__main__":
    main()

$ pagda t01_hello.py

pen: 3 x 10
ink: 12 x 2
total 54

Now break it. Call a def with the wrong kind of value:

t02_types_bad.pyrefused

def double(n: int) -> int:
    return n * 2


print(double("7"))

$ pagda t02_types_bad.py

  File "t02_types_bad.py", line 9
    print(double("7"))
TypeCheckError: String != Int
when checking that the expression "7" has type Int

The error comes from Agda and names the Python line. The table in the reference shows how to read Agda's spelling of types.

Commands

Command	What it does
`pagda file.py`	Checks the file if it is a checked file, then runs it.
`pagda --check file.py`	Checks the file and does not run it.
`pagda --agda file.py`	Prints the Agda text the file is translated to.

Settings

Name	Meaning
`PAGDA_AGDA`	The path of the `agda` program, when it is not on your `PATH`.
`XDG_CACHE_HOME`	Where checked results are kept. The default is `~/.cache/pagda`.

A file that passed is remembered, so Agda runs again only when the file changes. If agda cannot be started, a checked file is refused and does not run.

The same file under python3

A checked file is a Python file. It runs under python3 3.12 or newer with lib/dependent.py beside it (and lib/lemmas.py, if it uses the ready-made proofs), and prints the same output. There the types are not checked.

The tour walks through the language one idea at a time.
Proofs explains types that state facts.
The reference lists everything a checked file can hold.