About DepPy
DependentTypedPython (DepPy) is an experimental dependently typed language built on Python syntax.
In DepPy, dependent types can directly reference values. An annotation can describe the exact length of a collection or assert an equality that the function body must prove. DepPy statically verifies declarations within its supported subset without executing the source code.
The deppy package also lets you run the original source code with standard Python. Proof checking is a separate step handled by DepPy's checker. Neither standard Python execution nor conventional Python type checkers verify these proofs.
How Dependent Types Work
A return annotation of Nat specifies that the result is a natural number. A dependent return type can also refer to an input value: if a function receives n: Nat, a return type of Vec[Nat, n] specifies a vector of natural numbers whose length is n. Here, n is a value used in a type, rather than a generic parameter representing another type.
DepPy checks that the function body meets this stronger specification for its supported inputs. It elaborates the source into explicit terms and checks those terms with its kernel. A declared length or equality is therefore an obligation to prove, not a comment attached to the code.
Why Describe Values More Precisely?
Standard annotations like list[int] specify the type of elements a list contains, but not its length. With Vec[Nat, n], the length is part of the type, so the checker catches length mismatches before the program runs.
Types can also express claims about values, such as an equality. The type annotation states the claim, and the function body provides the proof:
from deppy import dependent, Nat, Eq, refl
@dependent
def same(n: Nat) -> Eq[Nat, n, n]:
return refl(n)Here, Eq[Nat, n, n] requires the function to return a proof of n = n, and refl(n) supplies that proof. DepPy checks the function body statically. A Python assert or a test suite checks only the values encountered during execution.
The Curry–Howard Correspondence
The Curry–Howard correspondence connects logic and typed programs: a proposition can be represented by a type, and a proof by a term of that type. In the example above, Eq[Nat, n, n] is the proposition and refl(n) is its proof term. The checked function same constructs that evidence for any n: Nat, rather than demonstrating the equality for only a few tested values.
DepPy checks proof terms with its kernel. A declaration can also depend on an explicit axiom; the Results panel reports such dependencies because an assumed axiom is not a proved statement.
What Does “Check” Examine?
@dependent: Marks pure functions and proofs for static verification. DepPy checks their types, bodies, and supported recursive definitions.@verified: Marks imperative code. DepPy converts contracts and control flow into proof obligations and verifies the resulting proofs.
The Results panel displays verified declarations, remaining goals, and errors. Clicking an error navigates directly to its location in the source code.
Why Are Check and Run Python Separate?
- Check statically verifies supported declarations without executing the source code.
- Run Python executes the original source in a browser-based Python environment and captures its output. It shows runtime behavior but does not verify proofs or contracts.
Current Scope
DepPy supports a subset of Python syntax. The checker rejects unsupported constructs and declarations with proof obligations it cannot verify.
The project does not guarantee equivalent behavior across checked terms, generated code, and direct Python execution. For details on supported features and limitations, consult the Reference, Proof Guide, and Python Execution Guide.