Examples
Complete programs. Each was checked and run to build this page. They are also part of Pagda's test suite.
A report from a list of records
Ordinary Python: a class, lists, a dict, f-strings, a value that may be None, and a main. Nothing here is a proof. The checker still guarantees that mean never divides by zero and that hist[g] never misses.
"""A program written the way a Python user would write it: grades and a report."""
from __future__ import annotations
from dependent import *
@dataclass
class Student:
name: str
scores: list[int]
def mean(xs: list[int]) -> int:
if not xs:
return 0
return sum(xs) // len(xs)
def best(xs: list[int]) -> Optional[int]:
result = None
for x in xs:
if result is None or x > result:
result = x
return result
def grade(score: int) -> str:
if score >= 90:
return "A"
elif score >= 80:
return "B"
elif score >= 70:
return "C"
return "F"
def histogram(students: list[Student]) -> dict[str, int]:
counts: dict[str, int] = {}
for s in students:
g = grade(mean(s.scores))
counts[g] = counts.get(g, 0) + 1
return counts
def top_students(students: list[Student], n: int = 2) -> list[str]:
ranked = sorted([mean(s.scores) for s in students])
ranked.reverse()
names = []
for target in ranked[:n]:
for s in students:
if mean(s.scores) == target and s.name not in names:
names.append(s.name)
return names
def report(students: list[Student]) -> None:
for s in students:
b = best(s.scores)
line = f"{s.name}: mean {mean(s.scores)} grade {grade(mean(s.scores))}"
if b is not None:
line += f" best {b}"
print(line)
hist = histogram(students)
for g in ["A", "B", "C", "F"]:
if g in hist:
print(g, "#" * hist[g])
def main() -> None:
students = [
Student("ada", [95, 88, 92]),
Student("bob", [72, 65, 80]),
Student("cy", []),
Student("dee", [85, 91]),
]
report(students)
print(top_students(students))
print(top_students(students, n=1))
if __name__ == "__main__":
main()
$ pagda ex_grades.py
ada: mean 91 grade A best 95 bob: mean 72 grade C best 80 cy: mean 0 grade F dee: mean 88 grade B best 91 A # B # C # F # ['ada', 'dee'] ['ada']
An array of exactly ten items
A class can carry a proof about its own fields. size is a proof that items has ten items, so an Array10 with any other length cannot be built.
@dataclass
class Array10:
items: list[int]
size: len(items) == 10 # a proof: the list has exactly 10 items
def get(self, i: Nat, ok: (i < 10) == True) -> int:
inside: (i < len(self.items)) == True = subst(lambda n: Eq[i < n, True], sym(self.size), ok)
return self.items[i]
def total(self) -> int:
return sum(self.items)
a: Array10 = Array10([1, 2, 3, 4, 5, 6, 7, 8, 9, 10], refl())
print(a.get(0, refl()), a.get(9, refl()), a.total())
$ pagda ex_array10.py
1 10 55
get asks its caller for a proof that the index is below 10. The inside line joins that with the size proof to show the index is inside the list. A list of the wrong length is refused:
@dataclass
class Array10:
items: list[int]
size: len(items) == 10
short: Array10 = Array10([1, 2, 3], refl())
$ pagda ex_array10_bad.py
File "ex_array10_bad.py", line 11
short: Array10 = Array10([1, 2, 3], refl())
TypeCheckError: 3 != 10 of type Nat
when checking that the expression refl has type
len (pos 1 ∷ pos 2 ∷ pos 3 ∷ []) ≡ 10Text, searching and loops
String handling, a dict of counts, a binary search and several while loops. The last def is a proof, imported from lemmas, that joining two lists adds their lengths.
"""Text processing, searching and while loops, with one proved property."""
from __future__ import annotations
from dependent import *
from lemmas import len_append
def tokenize(text: str) -> list[str]:
words = []
current = ""
for ch in text:
if ch == " " or ch == "\n":
if current:
words.append(current)
current = ""
else:
current += ch
if current:
words.append(current)
return words
def word_counts(words: list[str]) -> dict[str, int]:
counts: dict[str, int] = {}
for w in words:
if w in counts:
counts[w] += 1
else:
counts[w] = 1
return counts
def longest(words: list[str]) -> str:
best = ""
for w in words:
if len(w) > len(best):
best = w
return best
def is_sorted(xs: list[int]) -> bool:
i = 1
while i < len(xs):
if i > 0 and xs[i - 1] > xs[i]:
return False
i += 1
return True
def binary_search(xs: list[int], target: int) -> int:
lo = 0
hi = len(xs)
steps = 0
while steps < len(xs) and lo < hi:
mid = (lo + hi) // 2
if mid < len(xs):
if xs[mid] == target:
return mid
if xs[mid] < target:
lo = mid + 1
else:
hi = mid
steps += 1
return -1
def collatz_steps(n: int, limit: int = 1000) -> int:
steps = 0
left = limit
while left > 0:
if n == 1:
break
if n % 2 == 0:
n = n // 2
else:
n = 3 * n + 1
steps += 1
left -= 1
return steps
def fib(n: Nat) -> Nat:
a, b = 0, 1
for _ in range(n):
a, b = b, a + b
return a
def caesar(text: str, table: dict[str, str]) -> str:
out = ""
for ch in text:
out += table.get(ch, ch)
return out
# a property, proved once for every pair of lists
def joined_length(a: list[str], b: list[str]) -> len(a + b) == len(a) + len(b):
return len_append(a, b)
def main() -> None:
text = "the quick brown fox jumps over the lazy dog the end"
words = tokenize(text)
counts = word_counts(words)
print(len(words), longest(words), counts["the"] if "the" in counts else 0)
for w, c in counts.items():
if c > 1:
print(f"{w} appears {c} times")
print(is_sorted([1, 2, 2, 5]), is_sorted([3, 1]), binary_search([1, 3, 5, 7, 9], 7), binary_search([1, 3, 5], 4))
print(collatz_steps(27), fib(10), caesar("abc", {"a": "b", "b": "c"}))
assert tokenize("a b\nc") == ["a", "b", "c"]
assert fib(10) == 55
assert binary_search([1, 3, 5, 7, 9], 7) == 3
assert is_sorted([1, 2, 2, 5]) and not is_sorted([3, 1])
assert collatz_steps(6) == 8
if __name__ == "__main__":
main()
$ pagda ex_words.py
11 quick 3 the appears 3 times True False 3 -1 111 55 bcc
Vectors with their length in the type
A dot product that only accepts two vectors of the same length.
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 dot[n: Nat](a: Vec[int, n], b: Vec[int, n]) -> int:
match a:
case Nil():
return 0
case Cons(x, xs):
match b:
case Cons(y, ys):
return x * y + dot(xs, ys)
v: Vec[int, 2] = Cons(1, Cons(2, Nil()))
w: Vec[int, 2] = Cons(3, Cons(4, Nil()))
print(dot(v, w))
$ pagda t07_vec.py
11
A lookup that cannot go out of range
Fin[n] is a number below n. Indexing a Vec[A, n] with a Fin[n] needs no test and no proof at the call.
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]: ...
class Fin[n: Nat](Data): ... # a number below n
@constructor
def FZ[n: Nat]() -> Fin[n + 1]: ...
@constructor
def FS[n: Nat](before: Fin[n]) -> Fin[n + 1]: ...
def lookup[A, n: Nat](xs: Vec[A, n], i: Fin[n]) -> A:
match xs:
case Cons(x, rest):
match i:
case FZ():
return x
case FS(j):
return lookup(rest, j)
def nothing_below_zero[A](i: Fin[0]) -> A:
match i:
case _:
return unreachable()
v: Vec[str, 3] = Cons("a", Cons("b", Cons("c", Nil())))
print(lookup(v, FZ()), lookup(v, FS(FS(FZ()))))
$ pagda p_unreachable.py
a c