Pyfun

Pyfun is an F#-inspired, functional-first language that compiles to readable Python. It brings algebraic data types, exhaustive matching, currying, inferred effects, and units of measure to the Python ecosystem. Its Rust compiler checks all of them before any Python is emitted, then hands you plain Python with no runtime library attached.

type Shape = Circle float | Rect float float

let area s =
  match s:
    case Circle r: 3.14159 * r * r
    case Rect w h: w * h

let shapes = [Circle 2.0, Rect 3.0 4.0]
shapes |> List.fold (fun acc s -> acc + area s) 0.0 |> print

Delete the Rect case and the compiler refuses to build the program, naming the case you forgot. That check, and everything else Pyfun promises, happens before the Python exists.

This site is the learning home for the language. Pick the track that fits you:

• Learn Pyfun: a short, graded course for people who already know some Python. Each lesson introduces one idea and ends with an exercise you can solve in the browser. The compiler checks your work as you type.
• For educators: a ready-made functional programming module for an existing intro-Python course, with session plans, exercises, and answer keys. Free to adapt under CC BY 4.0.
• Inside the compiler: a guided tour of the Rust compiler, one pipeline stage per chapter. Useful if you want to learn how a language is built, read a real dependency-free Rust codebase, or contribute.

Try it right now

The playground runs the real compiler in your browser as WebAssembly. Write Pyfun on the left, watch the Python it compiles to appear on the right, and press Run to execute it. Nothing to install.

When you want it on your own machine (Python 3.12 or newer):

pip install pyfun-lang
pyfun repl

Jupyter users can get Pyfun as a notebook kernel:

pip install "pyfun-lang[jupyter]"
python -m pyfun_kernel.install

More

• The README has the full pitch, a feature tour, and comparisons with related projects.
• DESIGN.md is the language specification and the source of truth for its semantics.
• The interop cookbook shows Pyfun calling real Python libraries with types at the boundary.

The teaching material on this site is licensed under CC BY 4.0; the compiler and all code samples are Apache 2.0.

Learn Pyfun

This course teaches functional programming through Pyfun, in short lessons written for people who already know some Python. Each lesson introduces one idea, shows it working, and ends with an exercise. You do not need to install anything: every exercise links to the playground, where the real compiler checks your code as you type and a Run button executes it.

How the exercises work

The compiler is the marker. Each exercise gives you starter code that is almost right, plus the output the finished program should print. Three kinds of task repeat through the course:

• Fill the hole. The starter contains ? or ?name where an expression is missing. The compiler tells you the type it expects there, and suggests in-scope values that fit. Replace the hole with something of that type until the program compiles.
• Make it total. The starter forgets a case. The compiler names the exact value it cannot handle. Add the missing case.
• Make it compile. The starter contains one deliberate mistake (a type, effect, or unit error). Read the diagnostic and fix it.

When the program compiles, press Run and compare the output with the expected output shown in the exercise. If they match, you are done. Every exercise also has a collapsible solution, but the diagnostics usually get you there without it.

Running lessons your own way

The playground is enough for the whole course. If you prefer your own machine:

pip install pyfun-lang
pyfun run lesson.pyfun

Or work in a notebook with the Jupyter kernel (pip install "pyfun-lang[jupyter]", then python -m pyfun_kernel.install). Lesson 15 uses files and folders, so it needs the installed compiler; everything else runs anywhere.

The course at a glance

Lessons 1 to 8 cover the core: values, functions, and data types, and the habit the whole course builds toward, which is letting the compiler prove your program handles every case. Lessons 9 to 11 cover the workflow: type-driven development with holes, deliberate mutation, and inferred effects. Lessons 12 to 16 reach outward: calling Python libraries, computation expressions, units of measure, multi-file projects, and a capstone that puts everything together.

After the capstone, a Going further set digs into topics the core path skips: recursion, async, active patterns, building your own computation expression, and the fine print of strings and numbers. Take them in any order once you have finished the core lessons they build on.

1. Values and inference

A Pyfun program is built from values you name with let. In Python you would write name = "Ada". Pyfun uses a keyword, let, and the idea is the same: bind a name to a value. The difference is what happens next. A Pyfun let names a value that does not change, so the program reads as a set of definitions rather than a sequence of updates.

let name = "Ada"
let age = 36
let pi = 3.14
let isAdmin = true

print (f"{name} is {age}")
print (f"pi is about {pi}")
print isAdmin

Running this prints:

Ada is 36
pi is about 3.14
True

You never wrote a type. The compiler infers one for every binding: name is a string, age is an int, pi is a float, and isAdmin is a bool. There are no type annotations on let, and that is a deliberate design choice, not a missing feature. You get the safety of static types without writing them out.

Inference is not guessing. The compiler knows enough about each value to reject code that does not fit. Python allows + to mean both numeric addition and string joining, so a mistake there surfaces only when the line runs. Pyfun keeps the two apart and reports the mismatch before any Python is produced:

error: `+` is numeric and does not concatenate strings — use `String.concat a b`
 --> 1:13
  |
1 | let label = "age: " + 36
  |             ^^^^^^^

The compiler saw that "age: " is a string and that + works on numbers, so it stopped. print and f-strings (f"{x}", the same interpolation Python 3.12 uses) are how you observe a value once it is bound. Because a let binding is immutable, there is no statement that overwrites it in place. That capability exists, and it arrives in lesson 10, but the default is a value that stays put.

Exercise

Two baskets hold fruit. Fill the hole so the program adds them and prints the total. Run pyfun check on the starter: the compiler reports the type the hole expects and lists the names in scope that fit. Lesson 9 covers holes in full. For now, read the note and put the right name where ?count sits.

let apples = 4
let oranges = 3
let fruit = apples + ?count
print (f"total fruit: {fruit}")

Expected output:

total fruit: 7

Open in the playground

let apples = 4
let oranges = 3
let fruit = apples + oranges
print (f"total fruit: {fruit}")

2. Functions, currying, and pipes

A function in Pyfun is a let binding with parameters before the =. In Python you would write def add(a, b): return a + b. Pyfun writes the parameters inline and the body is the expression after =. Calls leave off the parentheses and commas: you write add 1 2, not add(1, 2).

let add a b = a + b

let inc = add 1

let double x = x * 2

let result = 5 |> inc |> double

print (add 2 3)
print (inc 10)
print result

Running this prints:

5
11
12

Two things there are new. First, add 1 is a call with one argument to a two-argument function. Instead of an error, it produces a new function that is waiting for the second argument. That is currying: every function takes its arguments one at a time, so a partial call like add 1 hands you back a function. Here inc adds one to whatever you give it.

Second, 5 |> inc |> double is a pipeline. The pipe |> takes the value on its left and feeds it to the function on its right, so you read it left to right as “start with 5, then inc, then double.” In Python you would nest the calls as double(inc(5)), which reads inside out. The pipe keeps the order of operations the same as the order you read.

None of this adds a runtime layer. A fully applied call compiles straight to a normal Python call, and the pipeline unwinds to plain nesting:

import functools
def add(a, b):
    return a + b
inc = functools.partial(add, 1)
def double(x):
    return x * 2
result = double(inc(5))

Currying shows up only where you actually leave an argument off: inc becomes a functools.partial. Everything else is ordinary Python. When you want to name a pipeline without a starting value, >> composes two functions into one, left to right, so inc >> double is the function that runs inc and then double.

Exercise

Finish the pipeline. The value 3 flows through double, then through one more stage. Run pyfun check and the compiler tells you the hole wants a function from int. Put the stage that makes the result 18.

let double x = x + x
let triple x = x + x + x

let result = 3 |> double |> ?stage
print result

Expected output:

18

Open in the playground

let double x = x + x
let triple x = x + x + x

let result = 3 |> double |> triple
print result

3. The None problem: Option

Python uses None to mean “no value here.” A function that might not find something returns None, and every caller is trusted to remember to check for it. When someone forgets, the program runs until an AttributeError surfaces far from the cause. Pyfun makes the absence part of the type. A value that might be missing has type Option, and there are exactly two shapes it can take: Some x when a value is present, and None when it is not.

Because the possibility of None is in the type, the compiler makes you handle both cases. You take an Option apart with match, which works like Python’s match statement: you list the shapes the value can have and give each one a result.

let describe s =
  match String.toInt s:
    case Some n: f"got the number {n}"
    case None: "not a number"

print (describe "41")
print (describe "hello")

let ns = [10, 20, 30]
let third = Option.withDefault 0 (List.get 2 ns)
let missing = Option.withDefault 0 (List.get 9 ns)
print third
print missing

Running this prints:

got the number 41
not a number
30
0

String.toInt is a total parse. In Python int("hello") raises, so calling code wraps it in try/except. Pyfun’s String.toInt returns Some 41 for "41" and None for "hello", and the match handles each. List.get behaves the same way: instead of an index that might raise IndexError, it returns Some when the position exists and None when it does not. When you only want a fallback and not a full match, Option.withDefault supplies one: Option.withDefault 0 (List.get 9 ns) is 0 because position 9 is past the end.

Exercise

The function below labels a parsed number, but it only handles the Some case. Run pyfun check and the compiler reports what is missing:

error: non-exhaustive match: `None` is not matched
 --> 2:3
  |
2 |   match String.toInt s:
  |   ^^^^^^^^^^^^^^^^^^^^^

Add the None case so the match is total and the program runs.

let label s =
  match String.toInt s:
    case Some n: f"number: {n}"

print (label "7")
print (label "nope")

Expected output:

number: 7
no number

Open in the playground

let label s =
  match String.toInt s:
    case Some n: f"number: {n}"
    case None: "no number"

print (label "7")
print (label "nope")

4. Errors as values: Result

Lesson 3 handled the absence of a value. This lesson handles an operation that can fail with a reason. In Python a failing operation raises an exception, and control jumps to whatever try/except happens to be in scope. Pyfun offers a type that carries the outcome as a value instead. Result has two shapes: Ok v when the operation succeeded and produced v, and Error e when it failed with an error e. Like Option, you take it apart with match, and the compiler makes you handle both shapes.

To turn a Python exception into a Result, you first give the Python function a Pyfun type with extern, then wrap the call in try. An extern declares that a Python callable exists and states its type; lesson 12 covers it in full. The try expression runs the call and catches any exception into an Error.

extern parseInt: string -> int = int

let describe s =
  match try (parseInt s):
    case Ok n: f"parsed {n}"
    case Error e: f"failed with {e.errorKind}: {e.errorMessage}"

print (describe "42")
print (describe "oops")

let safe = Result.withDefault 0 (try (parseInt "100"))
let fallback = Result.withDefault 0 (try (parseInt "bad"))
print safe
print fallback

Running this prints:

parsed 42
failed with ValueError: invalid literal for int() with base 10: 'oops'
100
0

try (parseInt s) has type Result int Exception. When int("42") returns cleanly you get Ok 42; when int("oops") raises, the exception is caught and delivered as Error e. The caught value is a record with two fields you can read: e.errorKind is the Python exception class name, here ValueError, and e.errorMessage is its text. Nothing escapes as a raised exception, so the failure is data you handle in the same expression. When you only want a default on failure, Result.withDefault 0 gives back the Ok value or the fallback, mirroring Option.withDefault from lesson 3.

Exercise

This function tries to read a number and report the result, but it matches on parseInt s directly. That call has type int, not Result, so the match does not fit. Run pyfun check:

error: type mismatch: expected Result 'a 'b, found int
 --> 4:9
  |
4 |   match parseInt s:
  |         ^^^^^^^^^^

Wrap the parse in try so it becomes a Result the match can take apart.

extern parseInt: string -> int = int

let describe s =
  match parseInt s:
    case Ok n: f"ok: {n}"
    case Error e: f"bad: {e.errorKind}"

print (describe "88")
print (describe "bad")

Expected output:

ok: 88
bad: ValueError

Open in the playground

extern parseInt: string -> int = int

let describe s =
  match try (parseInt s):
    case Ok n: f"ok: {n}"
    case Error e: f"bad: {e.errorKind}"

print (describe "88")
print (describe "bad")

5. Your own types: ADTs and exhaustive match

So far you have used types the language gives you, like int and Option. Now you define your own. An algebraic data type lists the shapes a value can take, one per line. In Python you might reach for an Enum, or a set of classes, or just a string like "circle" and hope every reader remembers the spelling. Pyfun writes the choices down as a type, and the compiler holds you to them.

type Shape =
  | Circle float
  | Rect float float

let area s =
  match s:
    case Circle r: 3.14159 * r * r
    case Rect w h: w * h

print (area (Circle 2.0))
print (area (Rect 3.0 4.0))

12.56636
12.0

Circle and Rect are the constructors. Each one is a function: Circle takes a float and returns a Shape, Rect takes two. You build a value by applying a constructor, and you take one apart with match, binding the fields with names of your choosing (r, then w and h).

Python 3.10 and later has match/case, and this lowers to it almost one for one:

def area(s):
    match s:
        case Circle(r):
            return 3.14159 * r * r
        case Rect(w, h):
            return w * h
        case _:
            raise RuntimeError("non-exhaustive match")

What Pyfun adds is the proof, before any Python is written, that the match covers every constructor. Delete the Rect case and the compiler stops you with the exact value you left out, so the trailing case _ guard never fires at runtime. This is what “making illegal states unrepresentable” means in practice: you model the domain so that a wrong value cannot be built, and then the compiler checks that your code answers for each shape that can.

Guards and or-patterns

A case arm can carry a condition. Write if after the pattern and the arm only fires when the guard is true:

let sign n =
  match n:
    case 0: "zero"
    case m if m > 0: "positive"
    case _: "negative"

print (sign 5)
print (sign 0)
print (sign (0 - 4))

positive
zero
negative

This is where exhaustiveness gets careful. A guarded arm might not fire, because the guard could be false, so the compiler does not count it toward covering the type. Drop the case _ and keep only the guarded arm, and the check fails:

let sign n =
  match n:
    case 0: "zero"
    case m if m > 0: "positive"

error: non-exhaustive match: add a wildcard `_` arm
 --> 2:3
  |
2 |   match n:
  |   ^^^^^^^^

The case m if m > 0 covers positive numbers at runtime, but the compiler cannot see that, so it asks for a catch-all to answer for the values a guard might let through.

An or-pattern matches any of several alternatives joined with |, exactly like Python’s case 1 | 2 | 3. Every alternative has to bind the same variables, so here they bind none:

let size n =
  match n:
    case 1 | 2 | 3: "small"
    case _: "big"

print (size 2)
print (size 9)

small
big

Exercise

A traffic light has three states, but action only answers for two. Run pyfun check and read the diagnostic: it names the state you forgot. Add the missing case so the program is total and prints the three lines below.

type Light =
  | Red
  | Amber
  | Green

let action l =
  match l:
    case Red: "stop"
    case Green: "go"

print (action Red)
print (action Amber)
print (action Green)

The checker reports:

error: non-exhaustive match: `Amber` is not matched
 --> 7:3
  |
7 |   match l:
  |   ^^^^^^^^

Expected output:

stop
wait
go

Open in the playground

type Light =
  | Red
  | Amber
  | Green

let action l =
  match l:
    case Red: "stop"
    case Amber: "wait"
    case Green: "go"

print (action Red)
print (action Amber)
print (action Green)

6. Records

An ADT models a choice between shapes. A record models one shape with named fields, the way a Python dataclass or a dictionary with fixed keys does. You declare the field names and their types once, then build values that carry all of them.

type Point = { x: int, y: int }

let here = Point { x = 3, y = 4 }
let moved = { here with x = 10 }

print here.x
print moved.x
print here.x
print here

3
10
3
Point(x=3, y=4)

You construct a record by writing the type’s constructor name, then the fields in braces: Point { x = 3, y = 4 }. The name in front is what tags the value as a Point, which is why the printout reads Point(x=3, y=4). You read a field with a dot, here.x, exactly as in Python.

The line { here with x = 10 } is copy and update. It does not change here. It returns a new record equal to here except for x, which is why the third print here.x still shows 3. The immutability from lesson 1 carries straight over: a record is like a frozen dataclass, so every update hands you a fresh value and the original stays put. The emitted Python makes this literal:

from dataclasses import dataclass
@dataclass(frozen=True)
class Point:
    x: int
    y: int
here = Point(3, 4)
moved = Point(10, here.y)

Records also match. A case may name a subset of the fields, and { x } shorthand binds the field to a variable of the same name:

type Point = { x: int, y: int }

let name p =
  match p:
    case Point { x = 0, y = 0 }: "origin"
    case Point { x, y }: "elsewhere"

print (name (Point { x = 0, y = 0 }))
print (name (Point { x = 3, y = 4 }))

origin
elsewhere

When a field itself holds a record, the update sugar nests: { seg with start.x = 99 } reaches through start and rebuilds the path for you, copying the siblings along the way.

Exercise

The hole marked ? is the new balance for a funded account. Run pyfun check: it reports the type the hole expects. Replace ? with 100 so the program prints the three lines below. Notice that opened.balance still shows 0 afterward, because the update produced a new record.

type Account = { name: string, balance: int }

let opened = Account { name = "Ada", balance = 0 }
let funded = { opened with balance = ? }

print funded.name
print funded.balance
print opened.balance

The checker reports:

note: hole `?` has type `int` — or: List.sum ?, String.len ?, ceil ?, floor ?
 --> 4:38
  |
4 | let funded = { opened with balance = ? }
  |                                      ^
1 unfilled hole

Expected output:

Ada
100
0

Open in the playground

type Account = { name: string, balance: int }

let opened = Account { name = "Ada", balance = 0 }
let funded = { opened with balance = 100 }

print funded.name
print funded.balance
print opened.balance

7. Lists, sets, and maps

A List a is a Python list, written with the same square brackets: [1, 2, 3]. The functions that work over lists live in a List module, so you call them as List.map, List.filter, List.fold. Keeping them behind a module name means a shared word like len can belong to every collection without clashing. Set and Map follow the same pattern and lower to Python’s set and dict.

let ns = [1, 2, 3, 4, 5]

let squares = List.map (fun x -> x * x) ns
let bigs = List.filter (fun x -> x > 2) ns
let total = List.fold (+) 0 ns
let doubled = List.map ((*) 2) ns

let third = Option.withDefault 0 (List.get 2 ns)
let missing = Option.withDefault 0 (List.get 9 ns)

let uniq = Set.ofList [1, 1, 2, 3]
let scores = Map.add "ada" 10 Map.empty

print squares
print bigs
print total
print doubled
print third
print missing
uniq |> Set.len |> print

[1, 4, 9, 16, 25]
[3, 4, 5]
15
[2, 4, 6, 8, 10]
3
0
3

fun x -> x * x is a lambda, the same anonymous function you met in lesson 2 written inline. Where the function is just an operator, an operator section is shorter: (+) is addition as a two argument function, and (*) 2 is multiplication with one argument already supplied, so List.map ((*) 2) ns doubles every element. List.fold walks the list carrying an accumulator, starting from 0 here and adding each element, which is how you reduce a list to a single value.

Totality carries over from lesson 3. In Python, ns[9] on a five element list raises IndexError. Pyfun has no bracket indexing at all. Instead List.get 9 ns returns an Option, None when the index is out of range, and you supply a fallback with Option.withDefault. The lookup cannot crash, because the empty case is a value you have to handle. Map.tryFind works the same way, returning an Option so a missing key is data rather than an exception.

Exercise

This program has two holes. List.fold needs a function to combine the running total with each element, and Option.withDefault needs a fallback for when index 10 is out of range. Run pyfun check to see the type each hole expects, then fill them so the program prints the sum and a safe default.

let ns = [4, 8, 15, 16, 23]

let total = List.fold ? 0 ns
let atTen = Option.withDefault ? (List.get 10 ns)

print total
print atTen

The checker reports:

note: hole `?` has type `int -> int -> int` — try: const, max, min — or: flip ?
 --> 3:23
  |
3 | let total = List.fold ? 0 ns
  |                       ^

note: hole `?` has type `int` — try: total — or: List.sum ?, String.len ?, cbrt ?, ceil ?
 --> 4:32
  |
4 | let atTen = Option.withDefault ? (List.get 10 ns)
  |                                ^
2 unfilled holes

Expected output:

66
0

Open in the playground

let ns = [4, 8, 15, 16, 23]

let total = List.fold (+) 0 ns
let atTen = Option.withDefault 0 (List.get 10 ns)

print total
print atTen

8. Tuples and destructuring

A tuple groups a fixed number of values that can have different types, written (a, b), exactly the Python tuple. A record gives its fields names, while a tuple identifies them by position, which suits a short pairing like a name and a score. Because the parentheses are also grouping, Pyfun reads them by how many elements are inside: () is unit, the empty value from lesson 1, (x) is just x in parentheses, and a real tuple has two or more elements. There is no one element tuple.

You take a tuple apart the same way you take an ADT apart, by matching. A single variable pattern covers a tuple completely, so one case is exhaustive:

let swap p =
  match p:
    case (a, b): (b, a)

let names = ["ada", "alan"]
let scores = [10, 9]

let line pair =
  match pair:
    case (name, score): f"{name}: {score}"

let lines = List.zip names scores |> List.map line

let byName = List.zip names scores |> Map.ofList
let adaScore = Option.withDefault 0 (Map.tryFind "ada" byName)

print (swap (1, 2))
print lines
byName |> Map.toList |> print
print adaScore

(2, 1)
['ada: 10', 'alan: 9']
[('ada', 10), ('alan', 9)]
10

List.zip pairs two lists element by element into a list of tuples, so List.zip names scores is [("ada", 10), ("alan", 9)]. Mapping line over that list destructures each pair in the case and binds name and score, the way Python’s for name, score in pairs unpacks as it goes.

Tuples also bridge lists and maps. Map.ofList builds a Map from a list of pairs, and Map.toList turns a map back into its pairs, so a zip followed by Map.ofList is a compact way to build a lookup table from two parallel lists.

Lists destructure too

The same match works over a List. A list pattern names elements in brackets, just like the literal that builds one: [] is the empty list, [only] matches a list of exactly one, and a *rest star soaks up any number of elements. Python allows one star per pattern, and so does Pyfun, but it can sit anywhere: [x, *rest] is head and tail, [*init, last] is everything but the last, and [first, *mid, last] binds the two ends with the middle collected between them.

let describe xs =
  match xs:
    case []: "empty"
    case [only]: f"just {only}"
    case [first, *mid, last]: f"{first} ... {last}"

print (describe [])
print (describe [7])
print (describe [1, 2, 3, 4])

empty
just 7
1 ... 4

An empty-list arm plus a star arm covers every list, so a match built from [] and one starred pattern is exhaustive with no case _. The [first, *mid, last] arm needs at least two elements, which is why the [] and [only] arms come first to catch the shorter lists.

Exercise

List.zip has paired each name with its score, and the case (name, score) arm has already destructured a pair for you. Fill the hole so each pair becomes a line like ada: 10, then the program joins the lines with a comma. Use the bound name and score in an interpolated string.

let names = ["ada", "alan"]
let scores = [10, 9]

let line pair =
  match pair:
    case (name, score): ?

let lines = List.zip names scores |> List.map line

lines |> String.join ", " |> print

The checker reports:

note: hole `?` has type `'a`
 --> 6:25
  |
6 |     case (name, score): ?
  |                         ^
1 unfilled hole

Expected output:

ada: 10, alan: 9

Open in the playground

let names = ["ada", "alan"]
let scores = [10, 9]

let line pair =
  match pair:
    case (name, score): f"{name}: {score}"

let lines = List.zip names scores |> List.map line

lines |> String.join ", " |> print

9. Typed holes and type-driven development

When you write a program, you rarely know every piece at once. You know the shape of what you want, and some parts are still blank. In Python you might leave a TODO comment or a pass and hope you remember what belonged there. Pyfun gives that blank a name and a type. Write ? or ?name anywhere an expression is missing, and the compiler tells you what belongs there: the type it expects, the in-scope values that fit directly, and the functions whose result would fit if you gave them more holes.

Here is a pipeline with one part left blank. It takes a list of names, transforms each one, and joins the results.

let names = ["ada", "grace", "alan"]

let headline names =
  names
  |> List.map ?upper
  |> String.join ", "

names |> headline |> print

Running pyfun check reports the gap rather than a failure:

note: hole `?upper` has type `'a -> string` — try: String.fromFloat, String.fromInt, String.lower, String.strip, String.upper, id — or: String.concat ?, String.join ?, Format.fixed ?, Format.percent ?
 --> 5:15
  |
5 |   |> List.map ?upper
  |               ^^^^^^^

The hole needs a function producing a string, and String.upper is right there under try:. The or: list names functions that would also fit if you filled their own holes. Replace ?upper with String.upper and the program compiles and prints ADA, GRACE, ALAN.

This is the workflow: sketch the whole pipeline with holes, let the compiler name each gap’s type, and fill inward from the types and the suggested fits. You never have to guess a function’s signature, because the hole reports it for you, and a hole blocks compilation by design, so nothing runs until every blank is filled.

Exercise

Fill both holes. report looks a score up in a map, supplies a fallback when the name is absent, and turns the number into a string. pyfun check reports each hole with a try: value that fits. The first report is:

note: hole `?render` has type `int -> 'a` — try: Format.padLeft, Format.padRight, List.range, Seq.range, String.fromFloat, String.fromInt — or: String.slice ?, Format.currency ?, Format.fixed ?, Format.percent ?

let scores = Map.add "ada" 10 (Map.add "alan" 9 Map.empty)

let report name =
  Map.tryFind name scores
  |> Option.withDefault ?missing
  |> ?render

print (report "ada")
print (report "cy")

Expected output:

10
0

Open in the playground

let scores = Map.add "ada" 10 (Map.add "alan" 9 Map.empty)

let report name =
  Map.tryFind name scores
  |> Option.withDefault 0
  |> String.fromInt

print (report "ada")
print (report "cy")

10. Mutation, on purpose

Everything so far has been immutable. A let binds a name to a value once, and that name never changes. This is the default because it removes a whole class of bugs: nothing can quietly reassign a value out from under you. Reassigning a plain let is a compile error, not a silent overwrite.

Sometimes a local accumulator really is the clearest way to express a calculation. Pyfun lets you ask for one explicitly. Inside an indented block body, let mut declares a mutable binding, and acc <- new reassigns it. The arrow is visible in the source, so mutation is something you opt into and a reader can see, not the default everywhere. The block’s last expression is its value.

let checkout price =
  let mut total = price
  total <- total + 5
  total <- total * 2
  total

print (checkout 10)

This prints 30: the price plus a five unit fee, then doubled. If you had written let total instead of let mut total, the first total <- ... would fail:

error: cannot assign to `acc`: it is immutable (declare it with `let mut`)

The mutation is scoped to the block. Outside checkout, nothing mutable escapes. And the emitted Python is exactly the plain statement sequence you would write by hand:

def checkout(price):
    total = price
    total = total + 5
    total = total * 2
    return total
print(checkout(10))

Pyfun has no for or while, so this is not how you iterate over a collection. For that, reach for List.fold and friends from lesson 7. let mut is for a genuine local accumulator built from a few explicit steps.

Exercise

balance starts from an opening amount and applies three transactions in sequence. The starter forgets to mark the accumulator mutable, so it does not compile. Read the diagnostic and fix the declaration.

let balance start =
  let acc = start
  acc <- acc + 100
  acc <- acc - 30
  acc <- acc + 50
  acc

print (balance 0)

Expected output:

120

Open in the playground

let balance start =
  let mut acc = start
  acc <- acc + 100
  acc <- acc - 30
  acc <- acc + 50
  acc

print (balance 0)

11. Effects, inferred

You already sense the difference between a function that computes and one that talks to the world. price * qty just calculates. print reaches out and shows something. In Python that distinction lives only in your head. Pyfun tracks it for you. It infers which functions perform effects, starting from the ones that obviously do, like print performing an io effect, and it propagates that outward: any function that calls an impure function is itself impure.

You never annotate effects. The inference is silent until you ask the compiler to confirm something is pure. Writing let pure in front of a definition is an assertion the compiler checks. If the body performs an effect, it is a compile error.

let pure total price qty = price * qty

let announce price qty =
  print (f"total: {total price qty}")

announce 12 3

This compiles and prints total: 36. total is pure, and the compiler agrees, because multiplication touches nothing outside itself. announce calls print, so it performs io. Its effect is inferred, not declared, and it needs no annotation. If you tried to mark announce as pure, the compiler would reject it, because purity propagates and a function that prints cannot be pure.

Here is what the check looks like when an assertion is wrong. A let pure whose body prints reports exactly where the effect happens:

error: `greet` is declared `pure` but performs `io`
 --> 2:3
  |
2 |   print name
  |   ^^^^^^^^^^

The fix is not to weaken the assertion but to separate the two jobs. Keep the pure part pure by having it return a value, and perform the effect at the call site, where the io belongs. That separation is the point: your calculating code stays provably free of side effects, and the parts that talk to the world are the parts that say so.

Exercise

greet is declared pure, but it prints inside its body, so it does not compile. Fix it by making greet return the greeting string and moving the print to the call site.

let pure greet name =
  print (f"Hello, {name}")
  name

let greeting = greet "ada"

Expected output:

Hello, ada

Open in the playground

let pure greet name = f"Hello, {name}"

print (greet "ada")

12. Talking to Python: extern

Pyfun compiles to Python, so the whole Python ecosystem is within reach. The way in is extern: you name a real Python callable and give it a Pyfun type. extern name: Type = dotted.target imports the target and lets the rest of your program call it with full type checking. The boundary is effectful by default, because most of the world is, so a plain extern is io. When a call is genuinely deterministic and side-effect free, extern pure asserts that, and then the purity checking from lesson 11 can prove whole pipelines pure across the boundary.

extern pure mean: List float -> float = statistics.mean

let readings = [2.0, 4.0, 9.0]

readings |> mean |> print

This prints 5.0. The emitted Python is the direct call you would expect, with the import added for you:

import statistics
readings = [2.0, 4.0, 9.0]
print(statistics.mean(readings))

The framing worth keeping is boundary versus engine. Pyfun shines at the boundary where the world is untyped and can fail, which is parsing, files, and the network. It adds little wrapped around an engine like numpy, whose speed lives in native code Pyfun cannot touch. Call the boundary safely and stay out of the engine’s way.

The clearest boundary is untrusted JSON. When an extern can raise, try from lesson 4 turns the exception into a Result you must handle. Building on that, the built-in Decode module turns raw JSON straight into your own record type or a structured error, so the rest of your program never sees an untyped shape. Decode.field pulls one field and runs a decoder on it, Decode.string and Decode.int decode strictly, Decode.map2 combines two field decoders into one that builds a record, and Decode.decodeString runs the whole thing over a JSON string to yield Result a Exception.

type Book = { title: string, pages: int }

let bookDecoder =
  Decode.map2 (fun title pages -> Book { title = title, pages = pages })
    (Decode.field "title" Decode.string)
    (Decode.field "pages" Decode.int)

let describe r =
  match r:
    case Ok b: f"{b.title}, {b.pages} pages"
    case Error e: f"failed ({e.errorKind})"

let wellFormed = """{"title": "Dune", "pages": 412}"""
let missingField = """{"title": "Dune"}"""

wellFormed |> Decode.decodeString bookDecoder |> describe |> print
missingField |> Decode.decodeString bookDecoder |> describe |> print

The well-formed object decodes to a typed Book. The object missing pages short-circuits to an Error carrying the Python exception, which match forces you to handle. The output is Dune, 412 pages then failed (KeyError).

Exercise

Complete the decoder by filling both holes with the strict field decoders. pyfun check reports each hole’s type and suggests the fit. The first report is:

note: hole `?titleDec` has type `Decoder string` — try: Decode.string — or: Decode.fail ?, Decode.oneOf ?, Decode.succeed ?, Decode.field ? ?

type Book = { title: string, pages: int }

let bookDecoder =
  Decode.map2 (fun title pages -> Book { title = title, pages = pages })
    (Decode.field "title" ?titleDec)
    (Decode.field "pages" ?pagesDec)

let describe r =
  match r:
    case Ok b: f"{b.title}, {b.pages} pages"
    case Error e: f"failed ({e.errorKind}): {e.errorMessage}"

let wellFormed = """{"title": "Dune", "pages": 412}"""
let missingField = """{"title": "Dune"}"""

wellFormed |> Decode.decodeString bookDecoder |> describe |> print
missingField |> Decode.decodeString bookDecoder |> describe |> print

Expected output:

Dune, 412 pages
failed (KeyError): 'pages'

Open in the playground

type Book = { title: string, pages: int }

let bookDecoder =
  Decode.map2 (fun title pages -> Book { title = title, pages = pages })
    (Decode.field "title" Decode.string)
    (Decode.field "pages" Decode.int)

let describe r =
  match r:
    case Ok b: f"{b.title}, {b.pages} pages"
    case Error e: f"failed ({e.errorKind}): {e.errorMessage}"

let wellFormed = """{"title": "Dune", "pages": 412}"""
let missingField = """{"title": "Dune"}"""

wellFormed |> Decode.decodeString bookDecoder |> describe |> print
missingField |> Decode.decodeString bookDecoder |> describe |> print

13. Computation expressions

Chaining steps that each return a Result gets awkward fast. Every step needs a match, and the success branch of one becomes the place you write the next. In lesson 4 you saw one such check. Two in a row already leans right, like a staircase:

let addStrings a b =
  match Option.toResult "bad a" (String.toInt a):
    case Error e: Error e
    case Ok x:
      match Option.toResult "bad b" (String.toInt b):
        case Error e2: Error e2
        case Ok y: Ok (x + y)

print (addStrings "3" "4")
print (addStrings "3" "oops")

Ok(7)
Error('bad b')

Every Error branch does the same thing: stop and pass the error along. A computation expression writes that repetition once. A result { } block lets you bind the success value of a step with let!, and if any step is an Error the whole block stops there and returns it. The same logic, read top to bottom:

let addStrings a b =
  result {
    let! x = Option.toResult "bad a" (String.toInt a)
    let! y = Option.toResult "bad b" (String.toInt b)
    return x + y
  }

print (addStrings "3" "4")
print (addStrings "3" "oops")

Ok(7)
Error('bad b')

let! unwraps an Ok, return wraps the final value back up, and the short-circuit on the first Error is automatic. This is the same idea as F#’s computation expressions. String.toInt gives back an Option (lesson 3), so Option.toResult bridges it to a Result with a message for the None case before let! binds it.

A second built-in builder is seq { }, which describes a sequence one yield at a time. It stays lazy, and it lowers to a Python generator function, which you may already know from Python’s own yield:

let counts =
  seq {
    yield 1
    yield 2
    yield 3
  }

counts |> Seq.toList |> print

def _pf_fn0():
    yield 1
    yield 2
    yield 3
counts = _pf_fn0()
print(list(counts))

Exercise

Fill the two holes so multiply parses both strings and returns their product as a Result. Each hole has type Result int 'a, so reach for the same Option.toResult ... (String.toInt ...) bridge the worked example used. When both parse you get Ok, and a bad string short-circuits to Error.

let multiply a b =
  result {
    let! x = ?
    let! y = ?
    return x * y
  }

print (multiply "6" "7")
print (multiply "6" "nope")

Expected output:

Ok(42)
Error('not a number')

Open in the playground

let multiply a b =
  result {
    let! x = Option.toResult "not a number" (String.toInt a)
    let! y = Option.toResult "not a number" (String.toInt b)
    return x * y
  }

print (multiply "6" "7")
print (multiply "6" "nope")

14. Units of measure

A plain float cannot tell you whether it holds metres, seconds, or kilograms, and mixing them up is a classic source of real bugs. Pyfun lets you tag a number with a unit and then checks the units the way it checks types. You declare a base unit with measure, and a literal carries that unit when the annotation touches the digits, like 100.0<m>.

measure m
measure s
measure kg

measure N = kg m / s^2                # newton, a derived alias

let distance = 100.0<m>
let elapsed = 10.0<s>
let speed = distance / elapsed        # float<m/s>
let side = sqrt 16.0<m^2>             # float<m>
let force = 6.0<N>                    # a value in newtons

print speed
print side
print force

10.0
4.0
6.0

Arithmetic combines units the way dimensional analysis does. Dividing float<m> by float<s> derives float<m/s>, so speed carries the right unit without you writing it down. sqrt halves the exponents, taking a float<m^2> to a float<m>, which is the length of a square’s side from its area. A measure N = kg m / s^2 names a compound of base units, so 6.0<N> is a newton and the compiler knows it means the same thing as 6.0<kg m / s^2>.

Adding quantities with different units is where the checker steps in. Writing distance + elapsed is rejected before any Python is produced:

error: type mismatch: expected float<m>, found float<s>

The units exist only during type checking. They erase at lowering, so the emitted Python is plain numbers with no unit machinery to slow it down:

import math
distance = 100.0
elapsed = 10.0
speed = distance / elapsed
side = math.sqrt(16.0)

Exercise

The program below wants the runner’s speed, but it adds a distance to a time, which does not type-check. Run pyfun check to see the mismatch, then change the one operator so the units line up and the value becomes a speed in float<m/s>. Speed is distance divided by time.

measure m
measure s

let distance = 240.0<m>
let elapsed = 30.0<s>

# Speed is distance per unit of time. This line does not type-check yet.
let speed = distance + elapsed

print speed

The checker reports:

error: type mismatch: expected float<m>, found float<s>
 --> 8:13
  |
8 | let speed = distance + elapsed
  |             ^^^^^^^^^^^^^^^^^^

Expected output:

8.0

Open in the playground

measure m
measure s

let distance = 240.0<m>
let elapsed = 30.0<s>

# Speed is distance per unit of time.
let speed = distance / elapsed

print speed

15. Modules and projects

As a program grows you want to group related definitions and give them a namespace, the way Python uses modules and packages. Pyfun offers this at two scales. The small one is an in-file module, a named block of let bindings. Inside the block members call each other by their bare names, and from outside you reach them qualified as Module.member.

module Geom =
  let square x = x * x
  let area w h = w * h
  let diagSq w h = square w + square h

print (Geom.area 4 5)
print (Geom.diagSq 3 4)

20
25

diagSq calls square directly because they share the module. From the top level you write Geom.area, which reads like math.sqrt does in Python. This grouping is purely organizational, so an in-file module runs anywhere Pyfun runs, including the playground.

The larger scale is one module per file. A sibling source file becomes a module under its capitalized name, and you bring it into scope with import. The project in examples/modules splits work across geometry.pyfun, store.pyfun, and a main.pyfun that imports both:

import Geometry
import Store

let floor = Geometry.area 4 5
let nine = Geometry.square 3
let widen = Geometry.area 10
let strip = widen 2

let hit = Store.lookup 1 |> Option.withDefault 0
let miss = Store.lookup 9 |> Option.withDefault 0

print floor
print nine
print strip
print hit
print miss

Running the whole project with pyfun run examples/modules/main.pyfun prints:

20
9
20
100
0

import Geometry refers to geometry.pyfun by its capitalized name, and the import graph must be acyclic. A Some built in Store is the same Option type main inspects, because the runtime classes are shared. Compiling with pyfun compile examples/modules/main.pyfun -o out writes a readable Python file tree, one .py per module plus a shared _pyfun_rt.py:

_pyfun_rt.py
geometry.py
main.py
store.py

A cross-module call lowers to plain Python attribute access like geometry.area(4, 5). Multi-file projects need the installed compiler on disk, since the playground runs a single source at a time. For practice there, an in-file module gives you the same qualified-use experience.

Exercise

Here is a flat program with two temperature conversions. Group both functions into an in-file module called Temp, then call them qualified as Temp.cToF and Temp.fToC. The output stays the same.

let cToF c = c * 9 // 5 + 32
let fToC f = (f - 32) * 5 // 9

print (cToF 100)
print (fToC 212)

Expected output:

212
100

Open in the playground

module Temp =
  let cToF c = c * 9 // 5 + 32
  let fToC f = (f - 32) * 5 // 9

print (Temp.cToF 100)
print (Temp.fToC 212)

16. Capstone: a typed pipeline

This last lesson puts the course together in one small program. It takes a JSON string of race results, decodes each into a record you define (lesson 12), handles the failure branch as a value (lessons 4 and 5), folds over the list to combine them (lesson 7), and computes an average speed that the compiler checks dimensionally (lesson 14). The whole thing prints a one-line report with an f-string.

The one join worth watching is where JSON meets units. A decoded number is a plain float with no unit attached, because JSON has no notion of metres or seconds. You attach the unit yourself by multiplying by a unit constant like 1.0<m>, which turns a float into a float<m>. From there the units carry through the arithmetic on their own, so dividing a folded float<m> by a folded float<s> gives the average speed in float<m/s> without any annotation.

The exercise is the program itself. Three holes sit at the interesting joints: the decoder for the distance field, the unit constant that lifts a decoded distance into metres, and the divisor that turns total distance and total time into a speed. Run pyfun check and the compiler tells you the type each hole expects, along with names in scope that fit. Fill all three and the report prints.

measure m
measure s

type Run = { name: string, distance: float, time: float }

let runDecoder =
  Decode.map3 (fun n d t -> Run { name = n, distance = d, time = t })
    (Decode.field "name" Decode.string)
    (Decode.field "distance" ?)
    (Decode.field "time" Decode.float)

let input = """[
  {"name": "ada", "distance": 100.0, "time": 20.0},
  {"name": "bo", "distance": 140.0, "time": 30.0}
]"""

let report =
  match Decode.decodeString (Decode.list runDecoder) input:
    case Ok runs:
      let names = runs |> List.map (fun r -> r.name) |> String.join ", "
      let dist = runs |> List.fold (fun a r -> a + r.distance * ?) 0.0<m>
      let time = runs |> List.fold (fun a r -> a + r.time * 1.0<s>) 0.0<s>
      let avg = dist / ?
      f"{names}: average speed {avg} m/s over {List.len runs} runs"
    case Error e: f"could not read input ({e.errorKind})"

print report

The checker names each expected type:

note: hole `?` has type `Decoder float` — try: Decode.float
note: hole `?` has type `float<m>` — try: a
note: hole `?` has type `float<'a>` — try: dist, time

Expected output:

ada, bo: average speed 4.8 m/s over 2 runs

Open in the playground

measure m
measure s

type Run = { name: string, distance: float, time: float }

let runDecoder =
  Decode.map3 (fun n d t -> Run { name = n, distance = d, time = t })
    (Decode.field "name" Decode.string)
    (Decode.field "distance" Decode.float)
    (Decode.field "time" Decode.float)

let input = """[
  {"name": "ada", "distance": 100.0, "time": 20.0},
  {"name": "bo", "distance": 140.0, "time": 30.0}
]"""

let report =
  match Decode.decodeString (Decode.list runDecoder) input:
    case Ok runs:
      let names = runs |> List.map (fun r -> r.name) |> String.join ", "
      let dist = runs |> List.fold (fun a r -> a + r.distance * 1.0<m>) 0.0<m>
      let time = runs |> List.fold (fun a r -> a + r.time * 1.0<s>) 0.0<s>
      let avg = dist / time
      f"{names}: average speed {avg} m/s over {List.len runs} runs"
    case Error e: f"could not read input ({e.errorKind})"

print report

17. Recursion

Lessons 1 to 16 are the graded course. From here on the lessons go a little deeper into corners of the language you can reach for once the basics are comfortable.

A function can call itself. In Pyfun a name is in scope inside its own body, the same way a Python def can refer to itself, so recursion just works with no rec keyword to turn it on:

let fact n =
  if n == 0 then 1
  else n * fact (n - 1)

print (fact 5)

120

fact refers to fact in its own else branch, and each call shrinks n toward the n == 0 base case that stops the descent. Two functions can lean on each other the same way. Mutual recursion needs no special form either, and the order you write them in does not matter, because both names are in scope across the pair:

let isEven n = if n == 0 then true else isOdd (n - 1)
let isOdd n = if n == 0 then false else isEven (n - 1)

print (isEven 10)
print (isOdd 7)

True
True

A recursive Pyfun function compiles to a plain Python function, so it shares Python’s call stack and its recursion limit. A recursion thousands of levels deep will overflow that stack, the same as it would in hand-written Python. For walking a long list or summing a large collection, reach for List.fold and the other combinators from lesson 7, which loop underneath and stay flat. Recursion earns its keep on tree-shaped data, where the depth follows the structure rather than the size of the input.

An arithmetic expression is a natural tree: a number is a leaf, and an addition or a multiplication holds two smaller expressions. The lesson 5 material models it as an ADT, and eval walks it by recursing into each branch:

type Expr =
  | Num int
  | Add Expr Expr
  | Mul Expr Expr

let eval e =
  match e:
    case Num n: n
    case Add l r: eval l + eval r
    case Mul l r: eval l * eval r

let tree = Add (Num 1) (Mul (Num 2) (Num 3))

print (eval tree)

7

Each case handles one shape, and the Add and Mul arms call eval on their sub-expressions, so the recursion bottoms out at the Num leaves. The depth of the calls matches the depth of the tree, which for a balanced expression stays small even when the tree holds many nodes.

Exercise

Tree holds an int at every leaf and branches in two. total should add up every leaf. The Leaf case is done, but the Branch case is a hole. Run pyfun check to see the type it expects, then combine the totals of the two sub-trees.

type Tree =
  | Leaf int
  | Branch Tree Tree

let total t =
  match t:
    case Leaf n: n
    case Branch l r: ?

let sample = Branch (Leaf 1) (Branch (Leaf 2) (Leaf 3))

print (total sample)

The checker reports:

note: hole `?` has type `int` — or: total ?, List.sum ?, String.len ?, ceil ?
 --> 8:22
  |
8 |     case Branch l r: ?
  |                      ^
1 unfilled hole

Expected output:

6

Open in the playground

type Tree =
  | Leaf int
  | Branch Tree Tree

let total t =
  match t:
    case Leaf n: n
    case Branch l r: total l + total r

let sample = Branch (Leaf 1) (Branch (Leaf 2) (Leaf 3))

print (total sample)

18. Async

Lesson 13 introduced computation expressions with result { } and seq { }. The third built-in builder is async { }, and it maps onto Python’s own async/await the way seq maps onto generators. An async { } block builds an Async a value. Inside it, let! awaits another async step, and return hands back the final value.

extern runAsync: Async a -> a = asyncio.run

let fetchScore =
  async {
    let! x = async { return 20 }
    return x + 1
  }

print (runAsync fetchScore)

21

The key idea carries straight over from Python. An async { } block does not run when you write it. It builds a coroutine, exactly like calling an async def in Python hands you an awaitable rather than a result. Nothing happens until something drives that coroutine. Here let! x = async { return 20 } awaits an inner block and binds 20 to x, then return x + 1 produces the final 21, but only once the coroutine is run.

The emitted Python shows the mapping directly. Each async { } becomes a nested async def, each let! becomes an await, and the whole value is a coroutine object:

import asyncio
async def _pf_fn1():
    async def _pf_fn0():
        return 20
    x = await _pf_fn0()
    return x + 1
fetchScore = _pf_fn1()
print(asyncio.run(fetchScore))

Running one at the top level

A coroutine has to be awaited somewhere, and at the top level there is no enclosing async function to await it in. Python solves this with asyncio.run(main()), and Pyfun makes the same move through extern (lesson 12). The line

extern runAsync: Async a -> a = asyncio.run

names Python’s asyncio.run and gives it the Pyfun type Async a -> a: hand it an Async a and it drives the coroutine to completion and returns the a. So fetchScore |> runAsync turns the Async int into a plain int you can print.

Async is an inferred effect

Lesson 11 showed the compiler inferring effects and checking let pure assertions. async is one of those effect labels. Effects are still inferred everywhere, and an extern arrow may state the async label explicitly with ->{async}, overriding the default io:

extern fetchAsync: string ->{async} string = httpx.get

A caller of fetchAsync then performs async, and that propagates outward. So a let pure body that performs async is a compile error, the same way a let pure that prints is:

extern fetchAsync: string ->{async} string = httpx.get

let pure grab url = fetchAsync url

print (grab "http://example.com")

error: `grab` is declared `pure` but performs `async`
 --> 3:21
  |
3 | let pure grab url = fetchAsync url
  |                     ^^^^^^^^^^^^^^

1 error

The effect is impossible to lie about. If a function awaits real async work, its type says so, and purity cannot be claimed over it.

Where async pays off, and where it does not

Async earns its keep when real I/O overlaps, so waiting on one network request or file read lets another proceed. The examples in this lesson are compute-shaped on purpose, because the browser playground has no network access, and Pyodide runs asyncio.run in its worker, so a self-contained block like fetchScore runs there and prints 21.

For real overlapping I/O, install the compiler with pip install pyfun-lang and read the http_fetch entry in the interop cookbook, which fetches URLs with inferred io and async effects over urllib and httpx. If you know Python’s asyncio, you can reach as far as you like through extern: any async client wraps the same way, and the effect system tracks it for you.

Exercise

Fill the hole so combined awaits two async blocks and returns their sum. The hole has type int (the value the second block returns), so any integer literal works. The runner bridge over asyncio.run is already in place, and runAsync combined drives the coroutine to a value.

extern runAsync: Async a -> a = asyncio.run

let combined =
  async {
    let! a = async { return 10 }
    let! b = async { return ? }
    return a + b
  }

print (runAsync combined)

Expected output:

30

Open in the playground

extern runAsync: Async a -> a = asyncio.run

let combined =
  async {
    let! a = async { return 10 }
    let! b = async { return 20 }
    return a + b
  }

print (runAsync combined)

19. Active patterns

A match (lesson 5) matches on the shape of data: constructors, records, tuples. Sometimes the distinction you care about is not a shape but a test, like whether a number is even or a string is blank. In Python that becomes an if/elif chain, and nothing checks that you covered every case. An active pattern gives those tests names and lets you match on them like constructors, so the exhaustiveness checking from lesson 5 applies to your own recognizers.

Total active patterns

A total active pattern lists a closed set of cases between (| ... |). Its body returns one of those cases for every input, so a match over it needs no catch-all: it is exhaustive by construction.

let (|Even|Odd|) n = if n % 2 == 0 then Even else Odd

let parity n =
  match n:
    case Even: "even"
    case Odd: "odd"

print (parity 4)
print (parity 7)

even
odd

The recognizer (|Even|Odd|) is an ordinary function that returns Even or Odd, and parity matches on the result as if Even and Odd were constructors. The emitted Python makes the mechanism plain: the recognizer becomes a function, and each case becomes an isinstance check against a small tag class.

def _ap_Even_Odd(n):
    if n % 2 == 0:
        return _Even()
    else:
        return _Odd()
def parity(n):
    _pf_t0 = _ap_Even_Odd(n)
    if isinstance(_pf_t0, _Even):
        return "even"
    elif isinstance(_pf_t0, _Odd):
        return "odd"
    else:
        raise RuntimeError("non-exhaustive match")

Partial active patterns

Not every recognizer covers every input. A partial active pattern ends in |_| and either binds a payload or tests a predicate, so its match needs a fallthrough case _.

The payload form returns Some value when it matches and None when it does not. The bound value flows into the case body:

let (|Positive|_|) n = if n > 0 then Some n else None

let clamped n =
  match n:
    case Positive p: p
    case _: 0

print (clamped 9)
print (clamped (0 - 5))

9
0

The predicate form returns a plain bool, so it binds nothing. case Blank matches when the recognizer is true:

let (|Blank|_|) s = String.strip s == ""

let lineKind s =
  match s:
    case Blank: "empty"
    case _: "text"

print (lineKind "   ")
print (lineKind "hi")

empty
text

The framing for Python folks is simple. An active pattern is a name for one branch of an if/elif chain, with the test tucked inside the recognizer. Call sites stay declarative, reading like a match over data, and for a total pattern the compiler still checks that you covered every case.

Exercise

Fill the hole so the partial pattern (|Hot|_|) recognizes a temperature of 25 or more. The hole has type bool (the condition that decides whether the pattern matches), so reach for a comparison on c. When it matches, Hot t binds the temperature; otherwise the case _ arm handles it.

let (|Hot|_|) c = if ? then Some c else None

let describe c =
  match c:
    case Hot t: f"hot at {t}"
    case _: "not hot"

print (describe 30)
print (describe 5)

Expected output:

hot at 30
not hot

Open in the playground

let (|Hot|_|) c = if c >= 25 then Some c else None

let describe c =
  match c:
    case Hot t: f"hot at {t}"
    case _: "not hot"

print (describe 30)
print (describe 5)

20. Build your own computation expression

Lesson 13 used result { } to write a chain of Result steps top to bottom, with the short-circuit on the first Error handled for you. The braces notation is not magic. Underneath, a computation expression is just method calls, and any in-file module (lesson 15) that provides bind and return_ becomes a builder you can use with the same { let! ... return ... } syntax.

Here is a builder for the Option type, so Maybe { } chains steps that might be None and stops at the first one:

module Maybe =
  let bind m f =
    match m:
      case Some x: f x
      case None: None
  let return_ x = Some x

let addOpt a b =
  Maybe {
    let! x = a
    let! y = b
    return x + y
  }

print (addOpt (Some 3) (Some 4))
print (addOpt (Some 3) None)

Some(7)
None_

bind says how to run one step and feed its unwrapped value into the next, and return_ wraps a final value back up. That is all a builder needs. The { let! ... return ... } block desugars to plain calls on the module, and ordinary type inference handles the rest, with no builder-specific rule in the compiler. The emitted Python shows the desugaring exactly:

def Maybe_bind(m, f):
    match m:
        case Some(x):
            return f(x)
        case None_():
            return None_()
        case _:
            raise RuntimeError("non-exhaustive match")
def Maybe_return_(x):
    return Some(x)
def addOpt(a, b):
    return Maybe_bind(a, lambda x: Maybe_bind(b, lambda y: Maybe_return_(x + y)))

Each let! becomes a Maybe_bind call whose continuation is a lambda binding the next name, and the return becomes Maybe_return_. The short-circuit falls out of bind: when a step is None, that branch never calls f, so addOpt (Some 3) None is None without running the +.

Builders can do more than bind and return_. A sequence-style builder adds yield_ for a yield, and combine/delay to glue and defer multiple yields, the same members the built-in seq { } relies on. The three built-in builders, async { }, seq { }, and result { }, keep bespoke lowerings so their output reads as idiomatic Python (async/await, generators, and a Result short-circuit) rather than a chain of method calls. The full desugaring rules live in the internals chapter on desugaring.

Exercise

Complete the Maybe builder by filling both holes, then addThree chains three optional values and returns their sum, stopping at the first None. The first hole (in the Some x arm of bind) has type Option 'a, and the compiler suggests f among the fits, so run the continuation f on the unwrapped x. The second hole is the body of return_, which must wrap its argument back up as an Option.

module Maybe =
  let bind m f =
    match m:
      case Some x: ?
      case None: None
  let return_ x = ?

let addThree a b c =
  Maybe {
    let! x = a
    let! y = b
    let! z = c
    return x + y + z
  }

print (addThree (Some 1) (Some 2) (Some 3))
print (addThree (Some 1) None (Some 3))

Expected output:

Some(6)
None_

Open in the playground

module Maybe =
  let bind m f =
    match m:
      case Some x: f x
      case None: None
  let return_ x = Some x

let addThree a b c =
  Maybe {
    let! x = a
    let! y = b
    let! z = c
    return x + y + z
  }

print (addThree (Some 1) (Some 2) (Some 3))
print (addThree (Some 1) None (Some 3))

21. Strings and numbers, in detail

Earlier lessons used strings and numbers as they came up. This one is a reference tour of what the two built-in types offer, grouped so you can find a feature when you need it.

The String module

There is no char type, so everything is a string, and the operations live in a String module. Concatenation, case, splitting, joining and slicing are all pure, and the parses are total: String.toInt and String.toFloat return an Option, None when the text does not parse, so they can never raise.

let title = String.concat "Hello, " "World"
let loud = String.upper title
let words = String.split ", " title
let csv = String.join "," words
let first5 = String.slice 0 5 title

print title
print loud
print words
print csv
print first5
print (Option.withDefault 0 (String.toInt "41"))
print (Option.withDefault 0 (String.toInt "x"))
print (Option.withDefault 0.0 (String.toFloat "2.5"))

Hello, World
HELLO, WORLD
['Hello', 'World']
Hello,World
Hello
41
0
2.5

String.slice 0 5 is total Python slicing, so an out-of-range bound clamps rather than raising, and String.toInt "x" hands back None, defaulted to 0 here.

String literals

An f-string interpolates any expression in {...}, exactly like Python. A {expr=} hole is self-documenting: it prints the source text and then the value, handy for a quick trace. To put a literal brace in the output, double it as {{ or }}. A raw string r"..." turns off escape processing, so a backslash stays a backslash, which is what you want for a Windows path or a regex. A triple-quoted string spans lines, with newlines and lone quotes kept as content.

let who = "Ada"
let score = 41

let line = f"{who} scored {score} ({String.upper who})"
let debug = f"{score=}"
let braces = f"{{literal braces}} around {score}"
let winPath = r"C:\Users\pyfun\data.csv"
let banner = """== pyfun ==
a "quoted" word"""
let emoji = "hi \u{1F600}"

print line
print debug
print braces
print winPath
print banner
print (String.len "café")
print (String.len emoji)

Ada scored 41 (ADA)
score=41
{literal braces} around 41
C:\Users\pyfun\data.csv
== pyfun ==
a "quoted" word
4
4

Regular strings still process escapes: \n, \t, \", \\, and \u{HEX} for a Unicode code point, so "hi \u{1F600}" ends with an emoji. Length counts characters, not bytes: String.len "café" is 4, because the string is real UTF-8 and é is one character, and the emoji string is 4 as well, the h, the i, the space and the one emoji.

Numbers

Integer and float literals carry the conveniences you would reach for in Python. Underscores group digits, 0x, 0o and 0b give hex, octal and binary, and a float can use scientific notation like 3.0e8. Exponentiation ** is float-only and right-associative, so 2.0 ** 3.0 ** 2.0 reads as 2.0 ** (3.0 ** 2.0). Floor division // and modulo % behave as in Python, and a chained comparison such as 0 <= x < 10 reads as one range test and evaluates x once.

let million = 1_000_000
let mask = 0xFF
let bits = 0b1010
let perm = 0o17
let lightSpeed = 3.0e8
let tower = 2.0 ** 3.0 ** 2.0
let q = 17 // 5
let r = 17 % 5
let inRange = 0 <= 7 < 10

print million
print mask
print bits
print perm
print lightSpeed
print tower
print q
print r
print inRange

1000000
255
10
15
300000000.0
512.0
3
2
True

0xFF is 255, 0b1010 is 10 and 0o17 is 15, all the same kind of integer written in different bases. 2.0 ** 3.0 ** 2.0 is 512 because the right-hand ** binds first, giving 2.0 ** 9.0. And 0 <= 7 < 10 is a single True, the way Python chains the two comparisons into one range check.

Exercise

String.toInt gives back an Option, and this program formats the parse into a sentence. The default supplied to Option.withDefault is a hole. Run pyfun check to confirm its type, then fill it so a string that does not parse falls back to 0.

let label raw =
  let n = Option.withDefault ? (String.toInt raw)
  f"{raw} parses to {n}"

print (label "42")
print (label "oops")

The checker reports:

note: hole `?` has type `int` — or: List.sum ?, String.len ?, ceil ?, floor ?
 --> 2:30
  |
2 |   let n = Option.withDefault ? (String.toInt raw)
  |                              ^
1 unfilled hole

Expected output:

42 parses to 42
oops parses to 0

Open in the playground

let label raw =
  let n = Option.withDefault 0 (String.toInt raw)
  f"{raw} parses to {n}"

print (label "42")
print (label "oops")

Educator pack

This pack turns the core 16 lessons of the Learn Pyfun track into a ready-made functional-programming unit you can slot into an existing Python course. It is organized as five class sessions with demo scripts, exercise assignments, and an instructor answer key. You can lift it wholesale or adapt any part of it.

Who this is for

Instructors of an intro or intermediate Python course who want to add a functional-programming unit without leaving the Python ecosystem. The sessions assume you are comfortable teaching Python and want to introduce ideas like immutability, algebraic data types, exhaustive matching, and effects using a language that compiles to readable Python your students already recognize.

What students need beforehand

Students should already know Python variables, functions, lists, and dictionaries. No functional programming background is assumed. The unit introduces every functional idea from scratch and keeps returning to the Python each construct compiles to, so students always have a familiar anchor.

Time budget

The unit runs as five sessions of about 90 minutes of class time each, plus homework between sessions. Each session doc includes a rough minute budget for the demo, discussion, and in-class exercises.

If your schedule favors shorter sessions, split the unit into six. The natural split point is inside Session 5: run lessons 12 and 13 as one session and lessons 14 through 16 as a sixth, with the capstone (lesson 16) as the finale. That split is noted again in the Session 5 doc.

Beyond the core unit, the course has a Going further set (recursion, async, active patterns, building a computation expression, and string/number details). It works well as stretch material for students who finish early, as self-study after the unit, or as the seed of an extra session if your course has room.

Session docs:

• Session 1: Functional basics in Python’s clothing
• Session 2: Making illegal states unrepresentable
• Session 3: Data modeling
• Session 4: The Pyfun workflow
• Session 5: Reaching the Python ecosystem
• Answer keys

Running the material with zero setup

The whole unit runs in a browser. Every lesson and every demo step links to the playground, where the real compiler checks code as you type and a Run button executes it. Nothing needs to be installed for students to follow along or to do the exercises.

If you have lab machines and want students working locally, two options add a native workflow:

pip install pyfun-lang
pyfun run lesson.pyfun

Or a notebook workflow with the Jupyter kernel:

pip install "pyfun-lang[jupyter]"
python -m pyfun_kernel.install

Only lesson 15 (modules across files) needs the installed compiler, because it uses a folder of source files. Every other lesson runs in the playground as it is.

Licensing

This teaching material is licensed under Creative Commons Attribution 4.0 International (CC BY 4.0). You are free to adapt, remix, and redistribute it, including for classroom and commercial use, as long as you give attribution. Institutions should feel free to lift it wholesale into their own courses.

The Pyfun code samples themselves remain under the Apache 2.0 license that covers the rest of the repository.

Session 1: Functional basics in Python’s clothing

Objectives

By the end of this session, students can:

• Bind values with let and explain why a binding is immutable by default.
• Read the type the compiler infers for a value without writing any annotations.
• Define a function with inline parameters and call it without parentheses or commas.
• Explain currying by showing that a partial call returns another function.
• Read a pipeline a |> f |> g and predict the equivalent nested Python call.

Prerequisites

Python variables and functions. No functional programming background. This is the first session of the unit.

Demo script

The thread for this session is that Pyfun is just Python underneath. Keep the playground’s Python output panel visible the whole time so the class sees the emitted Python change as you type.

1. Open the Session 1 worked example in the playground: functions and currying. Press Run first so the class sees 5, 11, 12. Ask them to predict what each line does.
2. Point at the Python panel. Show that let add a b = a + b became a plain def add(a, b), and that print (add 2 3) became print(add(2, 3)). Make the point that there is no runtime library: the output is ordinary Python.
3. Highlight let inc = add 1. This is the currying moment. Show that it compiled to inc = functools.partial(add, 1). Explain that a call missing an argument hands back a function rather than raising, which is what lets inc exist.
4. Highlight let result = 5 |> inc |> double. Show that it compiled to double(inc(5)). Read the pipe left to right (“start with 5, then inc, then double”) and contrast with the inside-out Python nesting. This is the reading-order payoff of the pipe.
5. Break it live. Change let inc = add 1 to let inc = add 1 2 3. The compiler reports too many arguments. Undo, then change double x = x * 2 to double x = x * "2" and show the type error arriving before any Python is produced. Restore the working program.
6. Switch to the Lesson 1 idea of inference. Open the Lesson 1 exercise. Run check, show that the hole ?count reports the type int and lists names in scope, and fill it with oranges. This previews the hole workflow the class will lean on all unit.
7. To close the “just Python” thread, add a line let label = "age: " + 36 to the Lesson 1 program and show the diagnostic that + is numeric and does not concatenate strings. Contrast with Python, where the same mistake would surface only at runtime.

Assigned exercises

• In class: the Lesson 1 exercise (fill the hole), done together in step 6 above.
• Homework: the Lesson 2 exercise, finishing the pipeline so the result is 18. Students should read the hole’s reported type before filling it.

Common misconceptions

• “let is just assignment, so I can reassign it later.” Correction: a let binds a value once and reassigning it is a compile error. Mutation is a separate, explicit feature that arrives in lesson 10.
• “add 1 is a bug, because add takes two arguments.” Correction: a partial call is intentional. It returns a function waiting for the remaining argument. That is currying.
• “The pipe must add overhead, like a stream or an iterator.” Correction: |> is compile-time sugar. 5 |> inc |> double compiles to double(inc(5)) with no runtime layer.
• “No type annotations means the language is dynamically typed like Python.” Correction: types are inferred and fully checked before any Python is emitted. The absence of annotations is a design choice, not the absence of static typing.
• “Calling add 2 3 without commas looks like a syntax error.” Correction: function application in Pyfun is by juxtaposition, so add 2 3 is the call. Parentheses are only for grouping.

Timing

• 10 min: framing the unit and what Pyfun is (compiles to readable Python).
• 30 min: demo script steps 1 to 5 (functions, currying, pipes, breaking it live).
• 20 min: demo script steps 6 to 7 (inference and the hole workflow).
• 20 min: students start the Lesson 2 exercise in the playground while you circulate.
• 10 min: recap and assign the Lesson 2 exercise as homework.

Answer keys: answer-keys.md

Session 2: Making illegal states unrepresentable

Objectives

By the end of this session, students can:

• Explain why None is a source of runtime bugs in Python and how Option moves that possibility into the type.
• Take an Option or Result apart with match and handle both shapes.
• Turn a Python exception into a Result value with try and read its errorKind and errorMessage.
• Define their own algebraic data type with several constructors.
• Read a non-exhaustive-match diagnostic, name the case it reports, and add it.

Prerequisites

Session 1 (values, functions, inference). Python’s own match/case helps but is not required.

Demo script

The centerpiece is the exhaustiveness error naming the exact case the code forgot. Build up to it with Option and Result, then land it on a hand-written ADT.

1. Open the Lesson 3 exercise. Run check. The compiler reports non-exhaustive match: None is not matched. Ask the class what value is missing before revealing it, then add case None: "no number" and Run.
2. Make the point that in Python int("nope") raises, and a caller has to remember to guard it. Here the None case is not a convention to remember, it is a case the compiler refuses to let you skip.
3. Open the Lesson 4 exercise. It matches on parseInt s directly, so check reports a type mismatch: it found int, not a Result. Wrap the call as try (parseInt s) and Run. Show that the caught ValueError reaches the Error arm as data.
4. Draw the contrast: Option models “a value might be absent,” Result models “an operation might fail with a reason.” Both force the caller to answer for the unhappy path.
5. Now the centerpiece. Open the Lesson 5 exercise. The Light type has three constructors but action answers for two. Run check and let the diagnostic speak: non-exhaustive match: Amber is not matched. The compiler names the exact forgotten state.
6. Add case Amber: "wait" and Run to get the three expected lines. Then delete case Green: instead and show the diagnostic now names Green. The point is that the checker tracks every constructor, not just the first gap.
7. Show the emitted Python for the working Light program. Point out the trailing case _: raise RuntimeError("non-exhaustive match") guard and explain that because the compiler already proved coverage, that guard can never fire. Exhaustiveness is checked before any Python exists.
8. Optional stretch: add a fourth constructor | Flashing to the type without touching action. The same diagnostic reappears naming Flashing, showing that widening a type reopens every match over it.

Assigned exercises

• In class: the Lesson 3 exercise and the Lesson 5 exercise, both driven from the demo.
• Homework: the Lesson 4 exercise (wrap the parse in try). Ask students to read errorKind and errorMessage off the caught value in their answer.

Common misconceptions

• “Option is just None with extra steps.” Correction: the difference is enforcement. With Option, the compiler refuses to compile until the None case is handled, so the forgotten check cannot happen.
• “try here works like Python’s try/except block.” Correction: try e is an expression that produces a Result value. There is no jump to a handler. The failure is data you match on in the same expression.
• “An ADT is basically a Python Enum.” Correction: an Enum lists bare names, but ADT constructors can carry data of different types (Circle float, Rect float float), and matching binds that data.
• “I can add a case _: catch-all to silence the exhaustiveness error.” Correction: that works but throws away the guarantee. When you later add a constructor, a real match reopens with a diagnostic, while a catch-all silently swallows the new case.
• “The exhaustiveness check happens at runtime, like the RuntimeError guard.” Correction: the check runs during type checking, before any Python is emitted. The runtime guard is a backstop that a proven-total match never reaches.

Timing

• 10 min: recap Session 1, then motivate the None problem in Python.
• 20 min: demo steps 1 to 4 (Option and Result).
• 25 min: demo steps 5 to 8 (the exhaustiveness centerpiece on a hand-written ADT).
• 25 min: students work the Lesson 3 and Lesson 5 exercises in the playground.
• 10 min: recap and assign the Lesson 4 exercise as homework.

Answer keys: answer-keys.md

Session 3: Data modeling

Objectives

By the end of this session, students can:

• Declare a record type with named fields and construct a value with the tagged constructor syntax.
• Copy and update a record and explain why the original is left unchanged.
• Match on a record, binding a subset of fields with the { x } shorthand.
• Work over lists with List.map, List.filter, and List.fold, using lambdas and operator sections.
• Group values by position with tuples and destructure them in a match arm.

Prerequisites

Sessions 1 and 2 (immutability, functions, match, ADTs). Python dictionaries and dataclasses give useful points of comparison.

Demo script

The thread is choosing the right shape for data: a record for one thing with named parts, a collection for many things, a tuple for a short positional pairing. Keep the Python panel visible so students see records become frozen dataclasses.

1. Open the Lesson 6 exercise. Run check and read the hole note: the hole has type int. Fill it with 100 and Run. Draw attention to the last line: opened.balance still prints 0.
2. Explain the copy-and-update line { opened with balance = 100 }. It builds a fresh Account and leaves opened alone, which is why the original balance is unchanged. Connect this back to the immutability from Session 1.
3. Show the Python panel: Account compiled to a @dataclass(frozen=True), and the update compiled to a new Account(...) call. The immutability is literal in the output.
4. Break it live: change Account { name = "Ada", balance = 0 } to drop the balance field. The compiler reports the missing field. Restore it. This shows records require all their fields.
5. Move to collections. Open the Lesson 7 exercise. Run check and show the two hole notes. The first hole wants int -> int -> int. Fill it with the operator section (+), fill the second with 0, and Run.
6. Make the totality point: there is no ns[10] bracket indexing in Pyfun. List.get 10 ns returns an Option, and Option.withDefault supplies the fallback, so an out-of-range lookup cannot crash. This is the same lesson from Session 2 applied to collections.
7. Move to tuples. Open the Lesson 8 exercise. Show that List.zip names scores produced a list of pairs and that the single case (name, score) arm destructures each pair. Fill the hole with f"{name}: {score}" and Run.
8. Close by contrasting the three shapes with one line each: a record when parts have names, a list when there are many of the same thing, a tuple for a short fixed pairing like a name and a score.

Assigned exercises

• In class: the Lesson 6 exercise and the Lesson 7 exercise, both driven from the demo.
• Homework: the Lesson 8 exercise (build one line per pair, then join). Ask students to note how the tuple pattern binds both parts at once.

Common misconceptions

• “A record is a dictionary, so I can add keys later.” Correction: a record’s fields are fixed by its type. It compiles to a frozen dataclass, and every field must be present when you build it.
• “{ opened with balance = 100 } mutates opened.” Correction: copy-and-update returns a new record. The original is untouched, which is why opened.balance still reads 0.
• “List.get 10 ns will raise IndexError like Python indexing.” Correction: there is no bracket indexing. List.get returns an Option, so an out-of-range index is None, a value you handle.
• “(+) and (*) 2 are odd syntax I have to memorize.” Correction: an operator in parentheses is just that operator as a function, and supplying one argument ((*) 2) is the same partial application from Session 1.
• “A one-element tuple (x) groups one value into a tuple.” Correction: (x) is just x in parentheses. There is no one-element tuple. A real tuple has two or more elements, and () is unit.

Timing

• 10 min: recap Session 2, then motivate choosing a data shape.
• 20 min: demo steps 1 to 4 (records and copy-and-update).
• 20 min: demo steps 5 to 6 (collections and totality).
• 15 min: demo steps 7 to 8 (tuples and the summary).
• 20 min: students work the Lesson 6 and Lesson 7 exercises in the playground.
• 5 min: recap and assign the Lesson 8 exercise as homework.

Answer keys: answer-keys.md

Session 4: The Pyfun workflow

Objectives

By the end of this session, students can:

• Use a typed hole to sketch a program and let the compiler report the type and fitting names at each gap.
• Fill a pipeline inward from the types the holes report, without guessing function signatures.
• Declare a deliberate local accumulator with let mut and reassign it with <-.
• Explain why immutability is the default and mutation is opt-in and visible.
• Read an inferred effect, assert purity with let pure, and fix a failed purity assertion by moving the effect to the call site.

Prerequisites

Sessions 1 through 3 (values, functions, match, records, collections). Students have already seen holes in passing when the earlier exercises reported a hole type.

Demo script

The thread is the day-to-day loop of writing Pyfun: sketch with holes, let types guide the fill, reach for mutation only when it is genuinely clearest, and let the compiler track effects for you.

1. Open the Lesson 9 exercise. Run check. Two holes report at once. Read the ?render note aloud: it has type int -> 'a and suggests String.fromInt among the fits. This is type-driven development in one screen.
2. Fill ?missing with 0 and ?render with String.fromInt, then Run to get 10 and 0. Make the point that you never looked up a signature: each hole reported exactly what belonged there.
3. Emphasize that a hole blocks compilation by design. Nothing runs until every blank is filled, so a half-written program cannot accidentally execute. Contrast with a Python pass or TODO, which runs and fails later.
4. Move to mutation. Open the Lesson 10 exercise. It reassigns acc with <- but declared it with a plain let. Run check and read the diagnostic: it says acc is immutable and points to let mut. Add mut and Run to get 120.
5. Show the emitted Python: the block became the plain statement sequence you would write by hand, total = ... reassigned in place. The <- arrow is what makes mutation visible in the source, and it is scoped to the block. Note there is no for or while, so let mut is for a genuine accumulator, not for iterating a collection.
6. Move to effects. Open the Lesson 11 exercise. greet is declared pure but prints inside its body. Run check and read the diagnostic: greet is declared pure but performs io, pointing at the print line.
7. Fix it the right way. Make greet return the string (let pure greet name = f"Hello, {name}") and move the print to the call site (print (greet "ada")). Run. Make the point: the fix is to separate the calculating part, which stays provably pure, from the part that talks to the world, which now says so.
8. To reinforce inference, add a second function that calls greet and prints, and show that its io effect is inferred without any annotation, while a let pure on it would be rejected. Effect tracking propagates outward on its own.

Assigned exercises

• In class: the Lesson 9 exercise and the Lesson 10 exercise, both driven from the demo.
• Homework: the Lesson 11 exercise (make greet pure by returning the string and printing at the call site).

Common misconceptions

• “A hole is like pass, so the program still runs with a blank.” Correction: a hole blocks compilation. Nothing executes until every hole is filled, which is what makes it safe to sketch.
• “I have to know a function’s signature before I can use it.” Correction: the hole reports the type it expects and lists in-scope names that fit. You fill inward from what the compiler tells you.
• “let mut means I should reach for it whenever I loop.” Correction: there is no for or while. Iterating a collection is List.fold and friends. let mut is for a local accumulator built from a few explicit steps.
• “acc <- x is the same as acc = x, just different syntax.” Correction: <- reassigns an existing mut binding and is visible on purpose. A plain let cannot be reassigned at all.
• “Marking something pure makes it pure.” Correction: let pure is an assertion the compiler checks. If the body performs an effect, it is a compile error. You cannot declare away an effect.

Timing

• 10 min: recap Session 3, then frame the write-with-holes workflow.
• 20 min: demo steps 1 to 3 (typed holes and type-driven development).
• 20 min: demo steps 4 to 5 (deliberate mutation).
• 20 min: demo steps 6 to 8 (inferred effects and let pure).
• 15 min: students work the Lesson 9 and Lesson 10 exercises in the playground.
• 5 min: recap and assign the Lesson 11 exercise as homework.

Answer keys: answer-keys.md

Session 5: Reaching the Python ecosystem

Objectives

By the end of this session, students can:

• Import a real Python callable with extern and give it a Pyfun type, using extern pure where a call is genuinely side-effect free.
• Decode untrusted JSON into a typed record or a structured error with the Decode module.
• Rewrite a staircase of Result matches as a flat result { } computation expression using let! and return.
• Tag a number with a unit of measure and let the compiler check dimensions, then explain that units erase at lowering.
• Group definitions into a module and qualify calls as Module.member.
• Assemble a small end-to-end pipeline that decodes, folds, and computes a unit-checked result.

Prerequisites

Sessions 1 through 4. The capstone leans on records (Session 3), Result and match (Session 2), and folds (Session 3), so this session is best after the whole unit.

Six-session variant

If you are running the unit as six sessions, split here. Session 5 becomes lessons 12 and 13 (extern and decoding, then computation expressions), and Session 6 becomes lessons 14 through 16 (units, modules, and the capstone), with the capstone as the finale. The demo script below is ordered so the split falls cleanly after step 4.

Demo script

The thread is the boundary versus the engine: Pyfun earns its keep where the outside world is untyped and can fail, and it stays out of the way of fast native code.

1. Open the Lesson 12 exercise. Run check and read the ?titleDec note: it has type Decoder string and suggests Decode.string. Fill both holes (Decode.string, Decode.int) and Run. The well-formed object becomes a typed Book, and the object missing pages becomes failed (KeyError): 'pages'.
2. Make the boundary-versus-engine point: the JSON is the untyped, failable edge, and decoding turns it into a Book or a structured error before the rest of the program sees it. Contrast with wrapping something like numpy, where Pyfun adds little because the speed lives in native code.
3. Open the Lesson 13 exercise. Before filling it, show the staircase form from the top of lesson 13 (two nested Result matches) and point out that every Error branch does the same thing. Then fill the two holes with Option.toResult "not a number" (String.toInt a) and its b twin and Run.
4. Make the point that let! unwraps an Ok, return wraps the final value, and the short-circuit on the first Error is automatic. The result { } block is the staircase written once. (If you are splitting into six sessions, this is the break point.)
5. Open the Lesson 14 exercise. It adds a distance to a time. Run check and read the mismatch: expected float<m>, found float<s>. Change the + to / and Run to get 8.0. Show the Python panel: the units are gone, the output is plain distance / elapsed. Units are checked, then erased.
6. Open the Lesson 15 exercise. Wrap the two functions in module Temp = and qualify the calls as Temp.cToF and Temp.fToC. Run. Note that this in-file module runs in the playground, while one-module-per-file projects need the installed compiler.
7. Finish with the capstone. Open the Lesson 16 exercise. Run check and let the three hole notes name each type: Decoder float, float<m>, float<'a>. Fill them (Decode.float, 1.0<m>, time) and Run to get the one-line report. Point at the join where JSON meets units: a decoded number is a plain float, and multiplying by 1.0<m> lifts it into metres so the fold carries a float<m>.
8. Close the unit by naming what the capstone touched: types, matching, records, collections, decoding, computation expressions, units, and modules. Every piece the language showcases, in one small program that fails safely on bad input.

Assigned exercises

• In class: the Lesson 12 exercise and the Lesson 13 exercise, driven from the demo.
• Homework: the Lesson 14 exercise and the Lesson 15 exercise.
• Capstone: the Lesson 16 exercise, fill all three holes. Suitable as an in-class finale or a take-home assessment. As a stretch, ask students to feed the decoder a malformed JSON string and confirm the Error branch reports rather than crashes.

Common misconceptions

• “extern means the Python call is safe now.” Correction: extern gives the call a type, but the boundary is effectful by default and can still raise. Wrap a call that can fail in try, or decode the data, to turn failure into a value.
• “Decoding JSON is just json.loads.” Correction: json.loads hands back an untyped shape. Decode.decodeString produces your record or a structured error, so the rest of the program never meets an untyped value.
• “result { } is a special block that runs differently at runtime.” Correction: it desugars to the same Result short-circuit you would write by hand with nested matches. let! and return are sugar for bind and wrap.
• “Units of measure add runtime overhead to every number.” Correction: units exist only during type checking and erase at lowering. The emitted Python is plain numbers.
• “A module changes how the code runs or performs.” Correction: an in-file module is purely organizational namespacing. Members call each other by bare name inside, and you qualify them as Module.member from outside.

Timing

• 10 min: recap the unit so far, then frame boundary versus engine.
• 20 min: demo steps 1 to 2 (extern and JSON decoding).
• 15 min: demo steps 3 to 4 (computation expressions).
• 15 min: demo steps 5 to 6 (units and modules).
• 20 min: demo steps 7 to 8 (the capstone) or students start it themselves.
• 10 min: unit wrap-up and pointers to the full course and playground.

Answer keys: answer-keys.md

Answer keys

This page is for instructors. It collects the solution and expected output for every exercise in the unit, one section per session. Each solution is the verified answer from the lesson’s own collapsed solution block, so it compiles and runs as shown. The linked lesson page holds the full explanation of each answer.

Session 1

Lesson 1: Values and inference

Lesson page

let apples = 4
let oranges = 3
let fruit = apples + oranges
print (f"total fruit: {fruit}")

Expected output:

total fruit: 7

Lesson 2: Functions, currying, and pipes

Lesson page

let double x = x + x
let triple x = x + x + x

let result = 3 |> double |> triple
print result

Expected output:

18

Session 2

Lesson 3: The None problem: Option

Lesson page

let label s =
  match String.toInt s:
    case Some n: f"number: {n}"
    case None: "no number"

print (label "7")
print (label "nope")

Expected output:

number: 7
no number

Lesson 4: Errors as values: Result

Lesson page

extern parseInt: string -> int = int

let describe s =
  match try (parseInt s):
    case Ok n: f"ok: {n}"
    case Error e: f"bad: {e.errorKind}"

print (describe "88")
print (describe "bad")

Expected output:

ok: 88
bad: ValueError

Lesson 5: Your own types: ADTs and exhaustive match

Lesson page

type Light =
  | Red
  | Amber
  | Green

let action l =
  match l:
    case Red: "stop"
    case Amber: "wait"
    case Green: "go"

print (action Red)
print (action Amber)
print (action Green)

Expected output:

stop
wait
go

Session 3

Lesson 6: Records

Lesson page

type Account = { name: string, balance: int }

let opened = Account { name = "Ada", balance = 0 }
let funded = { opened with balance = 100 }

print funded.name
print funded.balance
print opened.balance

Expected output:

Ada
100
0

Lesson 7: Lists, sets, and maps

Lesson page

let ns = [4, 8, 15, 16, 23]

let total = List.fold (+) 0 ns
let atTen = Option.withDefault 0 (List.get 10 ns)

print total
print atTen

Expected output:

66
0

Lesson 8: Tuples and destructuring

Lesson page

let names = ["ada", "alan"]
let scores = [10, 9]

let line pair =
  match pair:
    case (name, score): f"{name}: {score}"

let lines = List.zip names scores |> List.map line

lines |> String.join ", " |> print

Expected output:

ada: 10, alan: 9

Session 4

Lesson 9: Typed holes and type-driven development

Lesson page

let scores = Map.add "ada" 10 (Map.add "alan" 9 Map.empty)

let report name =
  Map.tryFind name scores
  |> Option.withDefault 0
  |> String.fromInt

print (report "ada")
print (report "cy")

Expected output:

10
0

Lesson 10: Mutation, on purpose

Lesson page

let balance start =
  let mut acc = start
  acc <- acc + 100
  acc <- acc - 30
  acc <- acc + 50
  acc

print (balance 0)

Expected output:

120

Lesson 11: Effects, inferred

Lesson page

let pure greet name = f"Hello, {name}"

print (greet "ada")

Expected output:

Hello, ada

Session 5

Lesson 12: Talking to Python: extern

Lesson page

type Book = { title: string, pages: int }

let bookDecoder =
  Decode.map2 (fun title pages -> Book { title = title, pages = pages })
    (Decode.field "title" Decode.string)
    (Decode.field "pages" Decode.int)

let describe r =
  match r:
    case Ok b: f"{b.title}, {b.pages} pages"
    case Error e: f"failed ({e.errorKind}): {e.errorMessage}"

let wellFormed = """{"title": "Dune", "pages": 412}"""
let missingField = """{"title": "Dune"}"""

wellFormed |> Decode.decodeString bookDecoder |> describe |> print
missingField |> Decode.decodeString bookDecoder |> describe |> print

Expected output:

Dune, 412 pages
failed (KeyError): 'pages'

Lesson 13: Computation expressions

Lesson page

let multiply a b =
  result {
    let! x = Option.toResult "not a number" (String.toInt a)
    let! y = Option.toResult "not a number" (String.toInt b)
    return x * y
  }

print (multiply "6" "7")
print (multiply "6" "nope")

Expected output:

Ok(42)
Error('not a number')

Lesson 14: Units of measure

Lesson page

measure m
measure s

let distance = 240.0<m>
let elapsed = 30.0<s>

# Speed is distance per unit of time.
let speed = distance / elapsed

print speed

Expected output:

8.0

Lesson 15: Modules and projects

Lesson page

module Temp =
  let cToF c = c * 9 // 5 + 32
  let fToC f = (f - 32) * 5 // 9

print (Temp.cToF 100)
print (Temp.fToC 212)

Expected output:

212
100

Lesson 16: Capstone: a typed pipeline

Lesson page

measure m
measure s

type Run = { name: string, distance: float, time: float }

let runDecoder =
  Decode.map3 (fun n d t -> Run { name = n, distance = d, time = t })
    (Decode.field "name" Decode.string)
    (Decode.field "distance" Decode.float)
    (Decode.field "time" Decode.float)

let input = """[
  {"name": "ada", "distance": 100.0, "time": 20.0},
  {"name": "bo", "distance": 140.0, "time": 30.0}
]"""

let report =
  match Decode.decodeString (Decode.list runDecoder) input:
    case Ok runs:
      let names = runs |> List.map (fun r -> r.name) |> String.join ", "
      let dist = runs |> List.fold (fun a r -> a + r.distance * 1.0<m>) 0.0<m>
      let time = runs |> List.fold (fun a r -> a + r.time * 1.0<s>) 0.0<s>
      let avg = dist / time
      f"{names}: average speed {avg} m/s over {List.len runs} runs"
    case Error e: f"could not read input ({e.errorKind})"

print report

Expected output:

ada, bo: average speed 4.8 m/s over 2 runs

Inside the compiler

A guided tour of the Pyfun compiler, read from the front. Pyfun is an F#-inspired, functional-first language that type-checks a small ML-family surface and emits readable Python, and its compiler is a dependency-free Rust crate. This tour walks the pipeline one stage at a time, from raw source text to the diagnostics and tooling on the other end.

Two audiences, one path

The tour is written for two readers at once.

• People learning how a language is built. Each stage of a real compiler is here in order: a hand-written lexer, a recursive-descent parser, a desugaring pass, Hindley-Milner type inference, exhaustiveness checking, lowering, and code emission. The chapters explain what each stage is responsible for and why the boundaries fall where they do.
• People learning Rust by reading a real codebase. The crate takes no dependencies, so every data structure and algorithm is in the tree and readable end to end. Chapters point at small, real excerpts and call out Rust idioms (enums and exhaustive match, ownership, trait derivation) as they appear in context.

It also doubles as contributor onboarding. Every numbered chapter closes with a short “Where you would add…” note naming the first file and function a contributor touches for a plausible change at that stage, so the tour is also a map from an intended change to the code that implements it.

The tour summarizes and points into two reference documents rather than duplicating them: DESIGN.md is the source of truth for what the language does and why, and INTERNALS.md is the map from a semantic rule to the module that implements it. When you want the full rule, follow the link.

The running example

Every chapter follows the same short program. The second half of the tour uses it too, so you can carry one mental model the whole way through.

type Shape = Circle float | Rect float float

let area s =
  match s:
    case Circle r: 3.14159 * r * r
    case Rect w h: w * h

measure m

let shapes = [Circle 2.0, Rect 3.0 4.0]
let total = shapes |> List.fold (fun acc s -> acc + area s) 0.0
let side = sqrt 16.0<m^2>
print (f"total {total}, side {side}")

It is small, but it exercises a lot of the surface: an algebraic data type, a curried function with an exhaustive match, a unit-of-measure declaration and annotation, a list literal, a pipe into a higher-order stdlib call with a lambda, and an interpolated print. Compiled and run, it produces:

total 24.56636, side 4.0

The pipeline at a glance

Pyfun’s central design commitment is that the compiler is the gatekeeper: every type, effect, exhaustiveness, immutability, and unit check runs before any Python is emitted, so a program that compiles cannot fail those checks at runtime. The stages below run in order, and each one gates the next.

source text
  -> lexing              (01)  tokens + offside layout
  -> parsing             (02)  a span-carrying AST
  -> desugaring          (03)  builders/sections collapse to core forms
  -> type inference      (04)  Hindley-Milner + effects
  -> exhaustiveness      (05)  every ADT variant handled
  -> units of measure    (06)  dimensional analysis, erased at runtime
  -> lowering            (07)  Pyfun AST -> Python-AST IR
  -> emission            (08)  readable Python source
  -> diagnostics         (09)  rustc-style errors throughout
  -> the compiler as a library (10)  the same front end, in the CLI and editor

The chapters:

• 00 - Orientation: the gatekeeper thesis, the dependency-free ethos, the crate layout and build order, and how to build and test.
• 01 - Lexing: tokens, the offside rule, unit annotations, holes.
• 02 - Parsing: recursive descent, precedence climbing, the span-carrying AST, and error recovery.
• 03 - Desugaring: computation-expression builders, operator sections, and composition collapsing to core forms.
• 04 - Type inference: Hindley-Milner with let-generalization, inferred effects, and the check-not-annotate philosophy.
• 05 - Exhaustiveness: Maranget-style usefulness and concrete witnesses.

The second half of the tour continues with units of measure (06), lowering (07), emission (08), diagnostics (09), and the compiler as a library, in the CLI and the editor (10).

00 - Orientation

Before we open the lexer, it helps to know the one idea the whole compiler is arranged around, the constraint the crate holds itself to, and where the pieces live.

The gatekeeper thesis

Python compiles to untyped bytecode: the runtime offers no compile-time guarantees. Pyfun gets F#-level safety the way TypeScript, Elm, and Haskell do, by putting a real compiler in front of the runtime. DESIGN.md §2 states it plainly: the Rust compiler enforces everything before any Python is emitted. A failed check stops compilation and produces a rustc-style diagnostic, and Python never runs.

That single commitment explains the shape of the pipeline. Type inference, effect checking, exhaustiveness, immutability, and unit checking all happen on the Pyfun AST, upstream of lowering. Only once a program has passed every gate does the compiler build a Python-AST IR and emit source. So the emitted Python is not where safety lives; it is the output of a process that already proved the program safe. This is why, in later chapters, you will see the checker carry rich structure (schemes, effect sets, a usefulness matrix) while lowering and emission stay comparatively mechanical. The hard thinking is done before a single line of Python exists.

The dependency-free ethos

The crate takes no third-party dependencies. The lexer and parser are hand-written, the diagnostics renderer is hand-written, and even the language server’s JSON layer is hand-rolled (src/lsp/json.rs) rather than pulling in serde. For a tour aimed partly at Rust learners this is a gift: every algorithm the compiler runs is in this tree, readable start to finish, with nothing hidden behind a crate boundary. It also keeps the shipped binary small and its behavior fully owned. The tradeoff is that Pyfun re-implements a few things a dependency would give for free, and the code is written with that in mind, favoring small single-purpose modules.

Crate layout and build order

INTERNALS.md is the canonical module map; the short version is that each stage of the pipeline is its own directory under src/:

• src/lexer/ tokenizer and token types
• src/parser/ recursive descent, with parser/ast.rs holding the span-carrying AST
• src/ast/ traversal and the canonical pretty-printer
• src/desugar.rs computation-expression desugaring, sections, composition
• src/types/ Hindley-Milner inference, effects, units, exhaustiveness
• src/lowering/ Pyfun AST to Python-AST IR
• src/python_emitter/ the IR to readable Python source
• src/diagnostics/ rustc-style error rendering
• src/main.rs the CLI driver, src/project/ the module graph
• src/lsp/ the language server

The dependency order among them is the pipeline order:

Build order: lexer + parser + ast -> desugar -> types (incl. units) -> lowering + python_emitter -> diagnostics + cli -> lsp.

Reading the modules in that order is reading the compiler from front to back, which is exactly what this tour does.

The three reference documents

Keep three files in view as you read the code. DESIGN.md is the semantic source of truth: what a construct means and why it was designed that way. INTERNALS.md is the implementation map: which module and function carries a given rule. ROADMAP.md holds the backlog and the non-goals. A change to the language touches DESIGN; a change to how the compiler realizes it touches INTERNALS. This tour points into both rather than restating them.

Building and testing

The toolchain is pinned (Rust 1.97.0) for reproducible formatting and lint. The everyday loop is short:

cargo build                                 # build the compiler
cargo test                                  # lexer + roundtrip + typecheck + compile/e2e
cargo run -- check   examples/hello.pyfun   # type-check with rustc-style diagnostics
cargo run -- compile examples/hello.pyfun   # lower to Python on stdout
cargo run -- run     examples/hello.pyfun   # compile then execute via python

The test suite leans on snapshot and golden tests: the parser round-trips source through its canonical pretty-printer, the checker compares diagnostics against expected text, and the end-to-end tests run the emitted Python through a real interpreter (skipping, not failing, when none is on PATH). This style keeps the tests close to observable behavior, which is the same lens the rest of this tour takes. When a chapter shows CLI output, it is the real output of the pyfun binary on the running example from the tour landing.

01 - Lexing

The lexer turns a source string into a flat stream of tokens. In Pyfun it also does one job that a whitespace-insensitive language would skip: it runs an offside rule that turns indentation into explicit block structure. Everything in this chapter lives in src/lexer/, with the token kinds in src/lexer/token.rs.

Tokens

The token set is a single Rust enum, Tok, covering literals, identifiers, the keywords, and the operators and punctuation. Keyword recognition is a lookup, not a special case in the main loop: the lexer reads an identifier, then asks whether that spelling is a keyword.

#![allow(unused)]
fn main() {
// src/lexer/token.rs
pub fn keyword(ident: &str) -> Option<Tok> {
    Some(match ident {
        "let" => Tok::Let,
        "match" => Tok::Match,
        "case" => Tok::Case,
        // ...
        _ => return None,
    })
}
}

If you are new to Rust, this is the language’s central idiom in miniature: an enum of variants plus an exhaustive match. The compiler checks that the match handles every possibility, and the _ => return None arm makes “anything else is an ordinary identifier” explicit.

The offside rule

Pyfun uses indentation for statement sequencing and blocks, and the lexer is where that becomes concrete. Its module documentation states the contract:

#![allow(unused)]
fn main() {
// src/lexer/mod.rs
//! Mostly whitespace-insensitive, with an **offside rule** that turns indentation
//! into block structure (outside any `()`/`{}` brackets, where line breaks are
//! always continuations). A layout stack of block columns drives three synthetic
//! tokens:
//! - [`Tok::Indent`] — a `let … =` whose body begins on a *deeper* line opens a
//!   block (the only block opener; `=` at bracket depth 0 primes it).
//! - [`Tok::Dedent`] — a line dedents below the current block's column, closing it.
//! - [`Tok::Sep`] — a line lands on the current block's column and the next token
//!   can begin a statement, separating two statements.
}

The mechanism is a stack of block columns and a pending_block flag. After an = (or another tail-position opener) at bracket depth 0, the lexer primes pending_block; when the next line is indented past the current column it pushes that column and emits Indent, and when a later line dedents it pops columns and emits Dedent. A line that lands back on the block’s own column, and whose leading token can start a statement, gets a Sep. Lines that lead with a continuation token (an infix operator, |, then/else/with) do not, which is what keeps a multi-line match or if glued into one statement. Inside brackets the whole rule is suspended, because a line break in () or {} is always a continuation.

In the running example, this is what lets the two case arms of area and the two top-level let bindings be laid out on their own lines without any punctuation. The parse chapter consumes these Indent/Dedent/Sep tokens as ordinary grammar.

A unit annotation is not a token

The example writes sqrt 16.0<m^2>. It is tempting to think the lexer recognizes <m^2> as a single unit token, but it does not. The lexer emits ordinary tokens, and a < is always the same token whether it opens a unit or means less-than. The lexer test spells this out:

#![allow(unused)]
fn main() {
// src/lexer/mod.rs (tests)
assert_eq!(
    kinds("5<m>"),
    vec![Tok::Int(5), Tok::Lt, Tok::Ident("m".to_string()), Tok::Gt, Tok::Eof]
);
}

So 5<m> and 5 < m produce the same token kinds. The distinction is drawn later, in the parser, by looking at spans: a < counts as a unit annotation only when it sits immediately after the literal with no intervening whitespace. The parser’s maybe_unit makes the call with self.cur_start() == self.prev_end(), the F# rule that keeps units and comparison apart. Keeping this out of the lexer is deliberate: the lexer stays a context-free tokenizer, and the one place that needs positional context (adjacency) reads it off the spans the lexer already recorded.

Holes are tokens

A typed hole, ? or ?name, is a first-class token, lexed like the f"/r" string prefixes with any name read adjacently:

#![allow(unused)]
fn main() {
// src/lexer/token.rs
/// A typed hole in expression position: `?` (anonymous) or `?name` ...
Hole(Option<String>),
}

Doc comments get the same treatment: a ## line at column zero lexes as Tok::Doc, while an ordinary # line is discarded as trivia. Making both holes and doc comments real tokens means they survive into the AST, so the checker can report a hole’s inferred type (see the inference chapter) and hover can show a declaration’s docs, rather than either being lost as whitespace.

Where you would add a new token

A new keyword is two edits: add the variant to Tok in src/lexer/token.rs and a line to Tok::keyword. A new operator or punctuation adds a variant and a branch in the character-dispatch of lex_one in src/lexer/mod.rs, taking care to lex multi-character operators (like <<) before their single-character prefixes. Nothing about the offside rule needs touching unless the token is itself a new block opener.

02 - Parsing

The parser turns the token stream into an abstract syntax tree. Pyfun’s parser is a hand-written recursive-descent parser with precedence climbing for operators, living in src/parser/mod.rs; the AST it builds is defined in src/parser/ast.rs.

Recursive descent and precedence climbing

Each grammar production is a method. Statements and declarations are parsed by parse_module, and an expression flows down a ladder of methods, one per precedence level, each calling the next tighter level and looping to fold in operators at its own level. The entry point dispatches the prefix-keyword forms, then hands the rest to the operator ladder:

#![allow(unused)]
fn main() {
// src/parser/mod.rs
fn parse_expr_head(&mut self) -> Result<Expr, ParseError> {
    match self.peek() {
        Tok::Fun => self.parse_fun(),
        Tok::If => self.parse_if(),
        Tok::Match => self.parse_match(),
        _ => self.parse_pipe(),
    }
}
}

From parse_pipe the ladder descends through composition, or, and, not, comparison, additive, multiplicative, unary minus, application, and finally atoms: parse_pipe -> parse_compose -> parse_or -> parse_and -> parse_not -> parse_comparison -> parse_additive -> parse_multiplicative -> parse_unary -> parse_application -> parse_atom. The ordering is the precedence table, written as call structure rather than a data table, and associativity falls out of whether a level loops (left-associative) or recurses (right-associative). Two details worth noting as you read: application binds tighter than every operator, so area s in acc + area s groups as acc + (area s), and comparison is chained Python-style, so parse_comparison collects a run of links into one node rather than nesting them left-associatively.

The span-carrying AST

Every node carries a source span so the checker and the editor can point at exact code. But spans would wreck the parser’s roundtrip tests, which compare a parsed tree against an expected tree structurally. The AST solves this with a small, clever type: NodeSpan compares equal to any other NodeSpan.

#![allow(unused)]
fn main() {
// src/parser/ast.rs
impl PartialEq for NodeSpan {
    fn eq(&self, _: &Self) -> bool {
        true
    }
}
}

This is a Rust idiom worth pausing on. Most of the AST derives PartialEq automatically with #[derive(PartialEq)], which compares fields structurally. By hand-writing PartialEq for the one field type that should be ignored, the derived equality on every enclosing node skips spans for free. The tree keeps real source locations for diagnostics, and structural equality still means “same shape.”

The expression AST itself is one enum, ExprKind, with variants for literals, Var, curried App, Fn, If, Match, Try, records, tuples, holes, interpolated strings, and the rest. Application is deliberately single-argument (App { func, arg }): a call like List.fold f z xs is a left-nested spine of App nodes, which is exactly the curried view the type checker and lowerer both want.

Error recovery keeps the editor alive

The compiler uses the strict entry point, which fails on the first parse error, because it must reject any broken program. The editor cannot afford that: one mistyped line should not blank out navigation for the whole file. So the parser has a second, error-recovering entry point:

#![allow(unused)]
fn main() {
// src/parser/mod.rs
pub fn parse_recover(tokens: Vec<Token>) -> (Module, Vec<ParseError>) {
    Parser { tokens, pos: 0 }.parse_module_recover()
}
}

On a failed item it records the error, then synchronize skips forward to the next item boundary, tracking Indent/Dedent so that a statement separator inside a broken block is not mistaken for the top-level boundary:

#![allow(unused)]
fn main() {
// src/parser/mod.rs
fn synchronize(&mut self) {
    let mut depth = 0i32;
    loop {
        match self.peek() {
            Tok::Eof => return,
            Tok::Sep if depth <= 0 => return,
            Tok::Indent => depth += 1,
            Tok::Dedent => depth -= 1,
            _ => {}
}

So one broken let no longer hides the rest of the file; the items that parse still drive hover and go-to-definition. The language server chapter (10) returns to how the front end reuses this.

Parsing the running example

The parser has a canonical pretty-printer (src/ast/), and pyfun parse shows the AST by printing it back. This is the real output for the running example:

type Shape = Circle float | Rect float float
let area s =
    match s:
        case (Circle r): ((3.14159 * r) * r)
        case (Rect w h): (w * h)
measure m
let shapes = [(Circle 2.0), ((Rect 3.0) 4.0)]
let total = (shapes |> ((List.fold (fun acc s -> (acc + (area s)))) 0.0))
let side = (sqrt 16.0<m^2>)
(print f"total {total}, side {side}")

The fully-parenthesized rendering makes the tree’s shape visible. 3.14159 * r * r prints as ((3.14159 * r) * r), showing * is left-associative; the total line shows two things at once: |> parses as an ordinary binary operator node (the lowering chapter is where it vanishes), and its right operand ((List.fold (fun …)) 0.0) is a two-deep App spine, showing curried application; and sqrt 16.0<m^2> keeps the unit annotation attached to the literal, showing the adjacency decision from the lexing chapter has already been made. Because the printer is canonical, feeding this output back to the parser produces the same tree, which is what the roundtrip tests check.

Where you would add a new expression form

A new operator adds a BinOp variant in src/parser/ast.rs and a branch at the right rung of the precedence ladder in src/parser/mod.rs; a new prefix form (a keyword-led expression) adds an ExprKind variant and a case in parse_expr_head or parse_atom. Whatever you add, give its node a span via the parser’s mk helper and teach the pretty-printer in src/ast/ to print it, so the roundtrip test still holds.

03 - Desugaring

Desugaring rewrites a few surface conveniences into the core forms the type checker and lowerer already understand, so those later stages need no special cases for the sugar. In Pyfun the pass lives in src/desugar.rs and covers three things: user-defined computation-expression builders, operator sections, and function composition. The design rule is stated in DESIGN.md §8.1: rewrite to ordinary calls and lambdas, then let normal inference and lowering take over.

Operator sections and composition

The smallest cases are the clearest. An operator wrapped in parentheses, like (+), is a first-class curried function. Rather than teaching the checker and emitter about operator values, op_func rewrites it to the lambda you would have written by hand:

#![allow(unused)]
fn main() {
// src/desugar.rs
pub fn op_func(op: BinOp, span: Span) -> Expr {
    let body = mk(
        ExprKind::Binary { op, lhs: Box::new(var("a", span)), rhs: Box::new(var("b", span)) },
        span,
    );
    mk(ExprKind::Fn { params: vec![/* a, b */], body: Box::new(body) }, span)
}
}

So (+) becomes fun a b -> a + b, and its num constraint, currying, and partial application all fall out of the ordinary rules with no bespoke code. Composition is the same tactic: f >> g desugars to fun x -> g (f x) and f << g to fun x -> f (g x). Composition has one extra care that a section does not, because its body embeds the operands, which may reference outer variables, so compose picks a parameter name (_pf_x, else _pf_x0, …) that is free of both operands’ free variables, ruling out capture. The pretty-printer keeps the faithful (op) / (f >> g) spelling regardless, so the roundtrip tests still see the source form.

The running example uses an explicit lambda in its fold, shapes |> List.fold (fun acc s -> acc + area s) 0.0, so it does not exercise a section. But the point-free cousin List.fold (+) 0.0 would desugar to exactly the lambda the example spells out, which is why both styles type-check and lower identically.

Computation-expression builders

Computation expressions are the F# flagship for monadic sugar, written builder { ... }. Pyfun splits them in two. The three built-ins keep bespoke native lowerings and are not desugared here, because a generic bind/return rewrite cannot produce idiomatic output for them. User-defined builders, on the other hand, are handled entirely by this pass. A builder is an in-file module providing protocol functions, and Builder { ... } desugars to calls on them. The protocol, from the module documentation:

#![allow(unused)]
fn main() {
// src/desugar.rs
//! | item            | desugaring                                           |
//! |-----------------|------------------------------------------------------|
//! | `let! x = e` …  | `B.bind e (fun x -> …)`                              |
//! | `do! e` …       | `B.bind e (fun _ -> …)`   (trailing `do! e` → `e`)   |
//! | `let x = e` …   | `(fun x -> …) e`                                     |
//! | `return e`      | `B.return_ e`        (must be last)                  |
//! | `return! e`     | `B.returnFrom e`     (must be last)                  |
//! | `yield e` …     | `B.combine (B.yield_ e) (B.delay (fun _ -> …))`      |
}

The driver, desugar_ce, is a recursion over the CE items. Each item is rewritten into a call on the builder module, threading the rest of the block through as a continuation lambda:

#![allow(unused)]
fn main() {
// src/desugar.rs
CeItem::LetBang { name, name_span, value } => {
    let cont = require_rest(builder, rest, span, "`let!`", value)?;
    Ok(call2(builder, "bind", value.clone(),
             lam(name.clone(), *name_span, cont, span), span))
}
}

Because the result is ordinary calls, the desugaring is type-directed for free: the builder’s own bind and return_ signatures determine the types through normal inference on the rewritten calls. There are no per-builder type rules and no per-builder codegen. Note too that the let!-bound name keeps its original span on the generated lambda parameter, so hover and rename still work on a name that only exists after desugaring.

The built-in result {}, natively

The three built-ins lower directly rather than through this pass, so it is worth seeing what “native” buys. Here is a small result {} block compiled with pyfun compile:

def safeDiv(a, b):
    def _pf_fn0():
        match Error("div by zero") if b == 0 else Ok(a):
            case Ok(x):
                return Ok(x / b)
            case Error(_pf_t0):
                return Error(_pf_t0)
    return _pf_fn0()

That is railway-oriented short-circuiting written as a real match: on Ok it continues, on Error it returns the error unchanged. A generic bind/return desugaring would produce a chain of closure calls instead, which is why the built-ins keep their own lowering while user builders take the desugaring path. The two mechanisms sit side by side: the same protocol shape, but the built-ins earn idiomatic Python by not being desugared.

Where you would add desugared sugar

A new value-level sugar that can be expressed with existing core forms belongs here. Add a constructor function to src/desugar.rs that builds the equivalent Fn/App/Binary tree (following op_func and compose), call it from the parser where the surface form is recognized, and keep the pretty-printer rendering the surface spelling so the roundtrip holds. If the sugar needs its own lowering to stay idiomatic, as the built-in CEs do, it instead belongs downstream in lowering, not in this pass.

04 - Type inference

This is where the gatekeeper does most of its work. The checker in src/types/ runs Hindley-Milner type inference, and alongside the ordinary types it infers units of measure and effects in the same pass. The module’s own header states the shape:

#![allow(unused)]
fn main() {
// src/types/mod.rs
//! Algorithm W with a substitution map and let-generalization, so top-level
//! bindings are polymorphic. Functions are curried.
}

Inference with let-generalization

Algorithm W walks the AST, inventing fresh type variables for unknowns and unifying them as it learns constraints, accumulating the results in a substitution map. At a let binding it generalizes: any type variable in the inferred type that is not pinned by the surrounding environment is quantified, turning a concrete type into a reusable scheme. That is what makes let id x = x usable at many types, and it is the reason a top-level definition needs no annotation to be polymorphic.

Consider area from the running example. Its body is a match on s with two arms, Circle r and Rect w h. Matching s against the Circle/Rect constructors forces s to have type Shape. Both arms compute with floats (3.14159 * r * r and w * h), so the result unifies to float. Nothing was annotated; the type Shape -> float fell out of the constructor patterns and the arithmetic. We can see the checker’s reasoning by planting a typed hole where area’s argument goes and running pyfun check:

note: hole `?s` has type `Shape` — or: Circle ?, Rect ? ?
 --> 8:18
  |
8 | let probe = area ?s
  |                  ^^

The checker inferred that whatever fills ?s must be a Shape, and it even suggests the two constructors that build one. That is the inferred parameter type of area, surfaced without a single annotation in the program.

Check, do not annotate

The absence of type annotations on let and lambda is a deliberate design choice, not a missing feature. HM inference is complete enough that the compiler never needs them, and annotation-free code is part of the point: DESIGN.md §3 makes optional let x : T annotations an explicit non-goal. The one place types are written on purpose is at the extern boundary, where Pyfun is told the type of a Python function it cannot infer. Everywhere else the compiler infers and the tooling reports: hover, pyfun check, and the REPL’s :type all surface the inferred type, so the type is always available even though it is never in the source.

The type machinery is a little richer than textbook HM because Pyfun’s numbers and units ride the same inference. A single built-in num constraint keeps arithmetic polymorphic over int and float, so let add a b = a + b infers num 'a => 'a -> 'a -> 'a and works at both. Units are an abelian group carried on numeric types and generalized like type variables, so let area w h = w * h infers a unit-polymorphic int<'u> -> int<'v> -> int<'u 'v>. Both are still Algorithm W; they just extend what a variable can be constrained by, and both are solved during the same walk.

Effects, inferred in the same pass

Effects are tracked in the type system rather than bolted on, and they are inferred, never written in ordinary code. Each function arrow carries a latent effect, a set of concrete labels plus effect variables for polymorphism:

#![allow(unused)]
fn main() {
// src/types/mod.rs
pub enum EffLabel {
    /// Observable side effects: printing, `<-` mutation, the (non-`pure`) Python
    /// FFI boundary.
    Io,
    /// Asynchronous execution. Produced ... by an `async {}` CE block ...
    Async,
}
}

The rules are propagation rules. print is 'a ->{io} unit, impurity flows outward (calling an impure function makes the caller impure), and labels from different calls union. A pure function reads exactly as it always did, with a plain ->. The one opt-in is the definition-level assertion let pure f ... = ..., which is a compile error if the binding introduces any concrete label. That assertion is how the effect inference becomes visible on the command line. Wrapping the example’s print in a pure binding is rejected, and the error names the exact label that was inferred:

error: `greet` is declared `pure` but performs `io`
 --> 2:3
  |
2 |   print (f"hello {name}")
  |   ^^^^^^^^^^^^^^^^^^^^^^^

The checker inferred io from the print call and propagated it up to the binding, then checked it against the pure assertion and found the contradiction. Effects are fully erased at lowering, so none of this leaves any residue in the emitted Python. Like units, effect tracking is maximum information at compile time and zero cost at runtime.

Where you would add a builtin’s type

The prelude and the stdlib modules are seeded as type schemes in src/types/mod.rs: the single source of truth for each is a names-and-arities table (PRELUDE, LIST_PRELUDE, and the rest) paired with a seed_* function that builds the scheme. To add a builtin you add its entry and its scheme there, marking the effect on the relevant arrow if it is not pure. Lowering reads the same arity table so partial application still works, which the lowering chapter picks up.

05 - Exhaustiveness

A Pyfun match must handle every case. This is one of the safety guarantees the compiler enforces before any Python exists (see DESIGN.md §3): a match that misses a variant is a compile error, not a runtime surprise. The check lives in src/types/ and runs as part of type checking, because it needs the inferred type of the scrutinee to know what the complete set of cases is.

Usefulness, not case-counting

A naive exhaustiveness check might count constructors, but that breaks down as soon as patterns nest: Some 0 | Some n | None should be exhaustive, and Some (Some x) should not be. Pyfun uses the standard, principled approach, Maranget’s usefulness algorithm. The check_exhaustive method documents the idea:

#![allow(unused)]
fn main() {
// src/types/mod.rs
/// Deep exhaustiveness via Maranget's usefulness algorithm ("Warnings for
/// pattern matching", JFP 2007). A `match` is exhaustive iff a wildcard row is
/// *not* useful against the matrix of arm patterns — i.e. there is no value the
/// wildcard would catch that no arm already does.
}

The reframing is what makes it work. Instead of asking “are all cases covered,” the algorithm asks “is a bare wildcard useful against the existing arms,” meaning: is there some value the wildcard would match that no arm already matches. If the wildcard is useless, every value is already covered and the match is exhaustive. If it is useful, the value it would catch is precisely a case that is missing, and the algorithm hands that value back as a witness.

The arms become a matrix of patterns, one row per unguarded arm (guarded arms may fail at runtime, so they never count toward coverage), and useful recurses column by column. It specializes the matrix against each constructor of the column’s type and recurses into the constructor’s fields, which is what gives deep exhaustiveness: nested patterns are checked all the way down, not just at the top level. A short internal enum, Wit, represents the witness it builds on the way back up, a constructor applied to sub-witnesses or _ for “any value.”

A witness from the running example

Delete the Rect arm from area, leaving only Circle:

let area s =
  match s:
    case Circle r: 3.14159 * r * r

Running pyfun check reports:

error: non-exhaustive match: `Rect _ _` is not matched
 --> 4:3
  |
4 |   match s:
  |   ^^^^^^^^

1 error

That message is the algorithm’s output, rendered. The scrutinee’s type is Shape, whose constructors are Circle and Rect. With only the Circle arm present, a wildcard is still useful, because a Rect value would slip past it, and the witness the algorithm produces is Rect applied to two wildcards. render_witness prints that witness back in Pyfun’s own pattern syntax, so the error does not just say “a case is missing,” it names the exact missing shape, Rect _ _, which is the pattern you would write to fix it. When no constructor is missing but a leaf over an infinite type is (a string or an integer literal match), the witness is _ and the message instead suggests adding a wildcard arm.

Two things are worth noticing about the boundary with the inference chapter. First, exhaustiveness runs inside type checking: check_exhaustive takes the already-inferred scrutinee type, so the two passes are not separable stages but one traversal. Second, the same usefulness machinery drives more than plain ADTs. Tuples recurse into their element columns, records into their fields, and even List sequence patterns are checked by modeling a list as the finite Nil | Cons type inside the algorithm only, with no real ADT and no change to lowering.

Why this earns its place

Exhaustiveness is the check that most directly repays the ML-family surface. Because the compiler proves every variant is handled, the emitted Python can lower a match to a real match/case statement and still add a defensive case _: raise arm that, by construction, is unreachable. The program is total on its ADTs before it ever runs, and adding a variant to a type turns every now-incomplete match into a compile error that points at the exact gap. That is the gatekeeper model working for the programmer rather than against them.

Where you would add a new pattern form

A new kind of pattern touches three places in src/types/mod.rs: binding and typing it (bind_pattern), and teaching the usefulness algorithm how it specializes (the column helpers default_matrix and expand_first_column, plus the witness rendering in render_witness). The List/Nil-Cons modeling and the tuple-column recursion are the two worked examples to follow. A pattern that adds no coverage power, such as an as-pattern, can instead be made transparent by peeling it before these steps, which is how Pyfun handles case p as x.

06 - Units of measure

Units of measure are Pyfun’s clearest demonstration of the gatekeeper model: the compiler does full dimensional analysis, then throws all of it away before emitting Python. The rule is in DESIGN.md §8.2; the code lives alongside HM inference in src/types/mod.rs, in the same file as the type checker rather than a separate sub-module, because unit unification is part of unification itself.

Units as a free abelian group

A unit is a product of base measures and unit variables raised to integer powers, with a dimensionless identity. That is exactly a free abelian group, and the representation follows directly:

#![allow(unused)]
fn main() {
// src/types/mod.rs
pub struct Unit {
    factors: BTreeMap<Atom, i32>,
}
}

Atom is either Base(String) (a declared measure like m) or Var(u32) (a unit variable the checker will solve for). The map never stores a zero exponent, so m^0 is not present and two equal units have identical maps. The group operations are the obvious ones over that map: mul adds exponents key by key, inv negates them, and pow(k) multiplies each by k. If you are new to Rust, note that BTreeMap keeps the factors in a stable sorted order, which is what lets equality and display stay deterministic without any extra sorting step.

Unit unification is not syntactic

Ordinary Hindley-Milner unification matches type constructors structurally. Units cannot work that way: m/s and s^-1 m are the same element, and solving 'u^2 ~ m^2 has to discover 'u = m. So unit equality is solved as a group equation. unify_unit reduces a ~ b to a / b ~ 1 and hands it to solve_unit, which runs Knuth/Kennedy variable elimination:

#![allow(unused)]
fn main() {
// src/types/mod.rs
fn unify_unit(&mut self, a: &Unit, b: &Unit) -> bool {
    let eq = self.apply_unit(a).div(&self.apply_unit(b));
    self.solve_unit(eq)
}
}

solve_unit picks the unit variable with the smallest absolute exponent as the pivot. If that exponent divides every other exponent, the variable is solved outright (v = product of the rest). Otherwise it substitutes a fresh variable to shrink the exponents and recurses. When only base measures remain with non-zero exponents there is no variable to pivot on, and the equation is a genuine dimension mismatch, which is exactly the <m> + <s> case below.

Derived-measure aliases expand to base units

measure N = kg m / s^2 is stored expanded. resolve_unit_against looks each name up in decls.measure_aliases and substitutes its base-unit body, so <N> and <kg m / s^2> become the same Unit value and unify freely. The tradeoff (DESIGN §8.2) is that inferred types display the expanded form, since there is no back-mapping from base units to an alias name.

Unit-aware sqrt halves exponents for free

sqrt has the prelude scheme float<'u^2> -> float<'u>, seeded with Unit::var(...).pow(2). Nothing special-cases roots in the unifier: applying sqrt to float<m^2> asks it to solve 'u^2 ~ m^2, and the elimination step halves the even exponent to give 'u = m. An odd exponent has no integer solution, so sqrt of a non-square unit is rejected with a dimension mismatch. In the running example:

let side = sqrt 16.0<m^2>

infers float<m>, and let norm x = sqrt (x * x) stays unit-polymorphic float<'u> -> float<'u>. cbrt is the identical mechanism with pow(3).

Erasure: a mismatch is caught, a clean program keeps no unit

The mismatch is a real compile error. pyfun check on 3.0<m> + 4.0<s>:

error: type mismatch: expected float<m>, found float<s>
 --> 4:11
  |
4 | let bad = 3.0<m> + 4.0<s>
  |           ^^^^^^^^^^^^^^^

1 error

Once a program checks, units vanish. pyfun compile on the running example lowers the sqrt 16.0<m^2> line to plain arithmetic, with no unit anywhere in the output:

side = math.sqrt(16.0)

The <m^2> annotation, the <m> result type, and every other dimension are gone. Nothing in the emitted module can tell you the program ever had units, which is the whole point: maximum static safety, zero runtime residue.

Where you would add a built-in measure or root

To seed a new prelude unit operation (say a fourth root), you add its scheme in seed_prelude in src/types/mod.rs using Unit::var(PRELUDE_UVAR).pow(n), and its name/arity in types::PRELUDE plus a lowering route in lower_var (src/lowering/mod.rs). The unifier needs no change: exponent division already handles the new power. DESIGN §8.2 explains why the built-in root family deliberately stops at sqrt and cbrt.

07 - Lowering

Once a program has passed type, effect, exhaustiveness, and unit checking, lowering turns the Pyfun AST into a Python-AST IR. The strategy is in DESIGN.md §5; the code is src/lowering/mod.rs. The firm rule is that lowering never splices strings. It builds structured PyStmt/PyExpr nodes, and a separate emitter (covered in emission) renders them. Two things make this more than a one-to-one copy, and both show up in the running example.

Expression language to statement language

Pyfun is expression-oriented; Python is statement-oriented. Function bodies lower in return position (lower_return), so an if or a match becomes a clean Python statement rather than a nested ternary. Sub-expressions lower in value position (lower_value), hoisting any statements they need before the value. The area function shows the return-position path: its match becomes a Python match statement whose arms return directly.

Curried in types, n-ary in output

Functions curry by default, but emitting add(1)(2) everywhere would be slow and unreadable. Because arities are known statically, build_call collapses a fully-applied call to a direct n-ary Python call and only synthesizes a closure for a genuine partial application:

#![allow(unused)]
fn main() {
// src/lowering/mod.rs
fn build_call(&mut self, head: PyExpr, arity: Option<usize>, args: Vec<PyExpr>) -> PyExpr {
    let n = args.len();
    match arity {
        Some(k) if n < k => {
            // Partial application.
            self.needs_functools = true;
            // ... functools.partial(head, args...)
        }
        Some(k) if n > k => { /* full call, then apply the remainder one at a time */ }
        // Exact arity, or unknown arity (treated as n-ary).
        _ => PyExpr::Call { func: Box::new(head), args },
    }
}
}

In the running example, area s inside the fold is a full application, so it collapses to the direct call area(s), and the fold’s folder is a two-argument lambda applied fully. Arities come from a syntactic table of top-level functions, constructors, and prelude members, built in the lowerer’s constructor. A genuine partial application (add 1) instead sets needs_functools and emits functools.partial(add, 1). This mirrors what F# does at the IL level: closures only where partial application is real.

The pipe is lowering-time sugar

x |> f has no runtime cost. flatten_app treats a pipe exactly like an application spine when it flattens the head and arguments:

#![allow(unused)]
fn main() {
// src/lowering/mod.rs
// `x |> f` is treated as `f x`, so pipes flatten alongside ordinary calls.
}

So x |> f |> g lowers to g(f(x)) with no intermediate helper, and a piped call reuses the same currying collapse as a written-out call. The running example proves it: let total = shapes |> List.fold (fun acc s -> acc + area s) 0.0 and the prefix spelling List.fold (fun …) 0.0 shapes produce byte-identical Python, the total = _pf_fold(...) line below. The pipe exists for the reader of the source, not for the interpreter.

Scope, name binding, and captured muts

Python makes an assigned name local to its function unless declared otherwise. A closure that reassigns a mut captured from an enclosing scope would therefore miscompile into a fresh local. lower_fn_body scans each body for names it reassigns but does not itself bind, then classifies each: a name found in an enclosing function frame (fn_local_stack) becomes nonlocal, and a module-level name becomes global.

#![allow(unused)]
fn main() {
// src/lowering/mod.rs
for name in &assigned {
    if bound.contains(name) { continue; }
    if self.fn_local_stack.iter().any(|f| f.contains(name)) {
        nonlocals.push(name.clone());
    } else {
        globals.push(name.clone());
    }
}
}

This is the same idea as F# 4.0 auto-boxing a captured mutable into a reference cell; Python’s nonlocal/global mechanism does the job directly.

Unit erasure happens here

Units are checked in types/ and then dropped. By the time lowering runs, a numeric value is just a number: there are no Unit nodes in the Python IR to carry, so sqrt 16.0<m^2> lowers with the annotation already gone (see units).

The running example, lowered

pyfun compile shows both transformations at once:

def area(s):
    match s:
        case Circle(r):
            return 3.14159 * r * r
        case Rect(w, h):
            return w * h
        case _:
            raise RuntimeError("non-exhaustive match")
shapes = [Circle(2.0), Rect(3.0, 4.0)]
total = _pf_fold(lambda acc, s: acc + area(s), 0.0, shapes)
side = math.sqrt(16.0)

The lambda’s area s collapsed to area(s), List.fold routed to the emitted _pf_fold helper (functools.reduce) with its three arguments direct and n-ary, and the unit is gone.

Where you would add a stdlib function’s lowering

A new collection or string helper is routed in lower_var (for its emitted _pf_* helper) or, for a pure one-liner that should inline when fully applied, in try_inline_stdlib inside lower_application, both in src/lowering/mod.rs. Register the member’s arity in the lowerer’s arity table so partial application still lowers to functools.partial, and add any new IR shape to the Python emitter first.

08 - Emission

Lowering produces a Python-AST IR; emission turns it into text. The IR and the emitter both live in src/python_emitter/mod.rs, and the design goal (per DESIGN.md §5) is blunt: the output is the interface. Pyfun compiles to Python you are meant to read, keep in your repo, and hand to Python tooling, so the emitted source has to look like something a person would write.

A small Python IR

PyModule is a flat list of PyStmt, and the statement enum covers only what lowering produces: Import, Assign, Return, Expr, FuncDef, If, Match, Try, ClassDef, and a handful more. If you are new to Rust, this is a textbook use of an enum: each statement shape is one variant carrying exactly its own fields, and the emitter is one match over them. The IR grows only when the language does, so there is no dead abstraction to wade through.

#![allow(unused)]
fn main() {
// src/python_emitter/mod.rs
pub enum PyStmt {
    Import(String),
    Assign { target: String, value: PyExpr },
    Return(PyExpr),
    Match { subject: PyExpr, cases: Vec<PyCase> },
    // ...
}
}

The emitter is line-based and deterministic

emit walks the module, emits the imports that dataclasses need once at the top, then recurses through emit_block/emit_stmt with a depth counter. Indentation is four spaces per level via a single line helper. There is no formatter pass and no randomness: the same IR always produces byte-identical text. That determinism is load-bearing beyond tidiness. The REPL and Jupyter kernel (see tooling) split the emitted program into top-level chunks and send only the chunks the worker has not run yet, which is only sound because re-emitting an unchanged definition yields the exact same bytes.

Match lowers one-for-one

A Pyfun match becomes a Python match, arm for arm. emit_stmt renders the subject, then each case with its optional guard:

#![allow(unused)]
fn main() {
// src/python_emitter/mod.rs
PyStmt::Match { subject, cases } => {
    line(out, depth, &format!("match {}:", expr(subject)));
    for case in cases {
        let guard = match &case.guard {
            Some(g) => format!(" if {}", expr(g)),
            None => String::new(),
        };
        line(out, depth + 1, &format!("case {}{guard}:", pattern(&case.pattern)));
        emit_block(&case.body, depth + 2, out);
    }
}
}

Constructor patterns emit as Python class patterns (case Circle(r):), which is why Pyfun’s ADTs lower to @dataclass classes with generated __match_args__: it lets the emitted match read like idiomatic structural Python. The checker has already proven the match exhaustive, so the trailing case _: raise RuntimeError(...) is a belt-and-braces guard, not something the program should ever hit.

The running example, in full

Here is the complete emitted Python for the running example, straight from pyfun compile:

from dataclasses import dataclass
import functools
import math
def _pf_fold(f, acc, xs):
    return functools.reduce(f, xs, acc)
@dataclass(frozen=True, repr=False)
class Circle:
    _0: float
    def __repr__(self):
        return f"Circle({self._0!r})"
@dataclass(frozen=True, repr=False)
class Rect:
    _0: float
    _1: float
    def __repr__(self):
        return f"Rect({self._0!r}, {self._1!r})"
def area(s):
    match s:
        case Circle(r):
            return 3.14159 * r * r
        case Rect(w, h):
            return w * h
        case _:
            raise RuntimeError("non-exhaustive match")
shapes = [Circle(2.0), Rect(3.0, 4.0)]
total = _pf_fold(lambda acc, s: acc + area(s), 0.0, shapes)
side = math.sqrt(16.0)
print(f"total {total}, side {side}")

Walking through it: the header imports are emitted once because a class is present and helpers are needed. _pf_fold is the emitted-on-demand List.fold helper, a thin wrapper over functools.reduce so the curried Pyfun function is a single callable. Circle and Rect are frozen dataclasses: frozen=True matches Pyfun’s immutability, and the hand-written positional __repr__ (with repr=False suppressing the generated one) makes a value print the way it was constructed, Circle(2.0) rather than Circle(_0=2.0). area is the return-position match. The three top-level lets become plain assignments, the fold folder is an inline lambda, sqrt erased its unit down to math.sqrt(16.0), and the final print uses a real Python f-string. Running it prints total 24.56636, side 4.0. Nothing about this file signals that it came from a compiler.

Where you would add a new emitted construct

A new Python shape (say a while loop for a future optimization) starts as a variant on PyStmt or PyExpr in src/python_emitter/mod.rs, with its rendering arm in emit_stmt/emit_expr, and only then does lowering get to produce it. Adding the IR node first keeps the “no string splicing” contract intact and gives you one place to get indentation and precedence right.

09 - Diagnostics

Pyfun’s pitch is that the compiler is the gatekeeper, so the compiler’s voice matters. DESIGN.md §3 puts it plainly: syntax is cheap, error quality is not. A language that rejects a program owes the reader a clear reason, a precise location, and where possible a way forward. That is why diagnostics get their own attention even though the rendering code is small.

The renderer is deliberately small

src/diagnostics/mod.rs is under a hundred lines. It renders one diagnostic in a rustc-like style: a level, a message, and a single underlined span.

#![allow(unused)]
fn main() {
// src/diagnostics/mod.rs
pub fn render(source: &str, level: Level, message: &str, span: Span) -> String {
    let (line_no, col_no, line_start) = locate(source, span.start);
    // ... builds the gutter, the source line, and a `^^^` underline
}
}

Level is Error, Warning, or Note. locate maps a byte offset to a one-based line and column, and the underline length is clamped to the rest of the line. That is the whole rendering surface. The intelligence lives upstream: the type checker (src/types/mod.rs) composes the message string, including the “did you mean” member hints and the typed-hole reports, and hands render a level, that message, and a span. Keeping presentation this thin means every diagnostic across the compiler shares one format for free.

Three real diagnostics

A type mismatch. HM inference reports the expected and found types at the offending call:

error: type mismatch: expected int<'a>, found string
 --> 2:13
  |
2 | let wrong = add "hello" 5
  |             ^^^^^^^^^^^

A non-exhaustive match. The Maranget usefulness check produces a concrete witness for the case the program forgot, so the message names it rather than saying only “not exhaustive”:

error: non-exhaustive match: `Rect _ _` is not matched
 --> 4:3
  |
4 |   match s:
  |   ^^^^^^^^

A typed hole report. This one is a note, not an error in the ordinary sense: it tells you the type the blank must have and offers ways to fill it.

note: hole `?body` has type `float` — try: h, w — or: area ?, cbrt ?, sqrt ?, abs ?
 --> 6:24
  |
6 |     case Rect w h: w * ?body
  |                        ^^^^^
1 unfilled hole

Typed holes and hole fits

A ? or ?name is a typed blank. It infers as a fresh type variable that unifies freely, so it never causes a spurious error and takes whatever type the context demands; here the context of w * ?body forces float. The report is assembled by Hole::message:

#![allow(unused)]
fn main() {
// src/types/mod.rs
pub fn message(&self) -> String {
    let mut parts = vec![/* hole `?name` has type `T` */];
    if !self.fits.is_empty() { parts.push(format!("try: {}", self.fits.join(", "))); }
    if !self.refinements.is_empty() { parts.push(format!("or: {}", self.refinements.join(", "))); }
    parts.join(" — ")
}
}

The try: list is the valid hole fits: every in-scope binding whose type unifies with the hole’s. The test is a real trial unification that snapshots the substitution maps, instantiates each candidate scheme, unifies it against the resolved hole type, and rolls back (Infer::hole_fits, described in INTERNALS.md’s typed-holes section). Fits are ranked most-specific first and capped. The or: list is refinement fits: a function whose result, after applying one or two further holes, unifies with the target, so area ? and sqrt ? appear because each returns a float. A hole blocks compile and run and makes check exit non-zero, so it is informative during development without ever slipping into emitted Python.

Why this framing

The mismatch names both types, the non-exhaustive report hands you the exact missing shape, and the hole tells you what would type-check right there. Each one answers the reader’s next question instead of leaving them to guess. That is the concrete meaning of “error quality is not cheap”: the checker does extra work (witnesses, trial unification) specifically so the message can be specific.

Where you would add a new diagnostic note

A new hint or note is composed where the checker detects the condition, in src/types/mod.rs (the closest_member “did you mean” path is a good model), and passed through render with the right Level. If a diagnostic needs a shape the renderer cannot express yet, such as a second span or a diagnostic code, that extension goes into src/diagnostics/mod.rs; the module’s own header flags multi-span notes and codes as the natural next step.

10 - The compiler as a library

Everything the earlier chapters described, lexing through emission, is exposed as a plain Rust library with a few pure entry points: pyfun::analyze (resilient diagnostics and inferred types) and pyfun::compile (source to readable Python). The CLI is one caller. The language server, the REPL, the Jupyter kernel, and the browser playground are the others, and they all reuse the same front end rather than reimplementing any of it. This chapter is the tour of those callers.

The language server

src/lsp/mod.rs is a dependency-free LSP server over stdio. To keep the core crate free of serde and lsp-types, the JSON value type, parser, and serializer are hand-rolled in src/lsp/json.rs, the same choice made for the lexer and parser. The message-handling core, Server::handle, is pure (JSON in, JSON out), so it is unit-tested without spawning a process.

Every feature is a view over one analyze result. Diagnostics are the same type, effect, unit, and exhaustiveness errors from earlier chapters, streamed as publishDiagnostics. Hover shows an inferred type, which is the only way to see one since Pyfun never writes them; it comes from a (span, type) table the checker fills in its collecting pass. Go-to-definition, find-references, and rename run over a dependency-free name resolver (src/lsp/resolve.rs) that walks the parsed AST, so navigation works on any program that parses even if it does not yet type-check. That resilience is deliberate: the parser has an error-recovering entry point, so a half-typed file still yields hover and navigation for the parts that parse. Details of the caches and cross-file navigation are in INTERNALS.md.

The module graph

Multi-file projects are resolved by src/project/mod.rs. From an entry file it follows import edges, builds a dependency graph, rejects cycles and missing files, and returns the modules in topological order. The graph logic is decoupled from the filesystem: build takes a loader closure mapping a module name to its source, so it is unit-testable with an in-memory map, and build_from_path is the thin wrapper that resolves names to .pyfun files. Cross-module checking and the parallel .py emit build on that ordered Project.

The REPL

src/repl.rs pairs the Rust checker with one long-lived Python worker process holding a single namespace for the session. Each entry is type-checked against the accumulated definition source, and what reaches Python is a diff: because emission is deterministic (see emission), the program is split into top-level chunks and only chunks the worker has not run yet are sent, length-framed over the worker’s stdin/stdout. The worker itself is a tiny driver that execs each blob in a persistent dict and returns captured output:

# src/repl.rs (the DRIVER fed to python -c)
ns = {}
# ... read a length-framed blob, then:
    exec(code, ns)

So a definition’s effects run once at entry, an expression runs once per entry, and state including top-level let mut persists. A dead worker is respawned and the namespace rebuilt.

The Jupyter kernel

src/kernel.rs (pyfun kernel-engine) is the REPL turned inside out. It does the same accumulate, analyze, compile, chunk-diff bookkeeping, but instead of driving a worker it returns the new-chunk blob for the caller (the pyfun_kernel Python package inside Jupyter) to exec in its own namespace. The kernel process is itself Python, so there is no separate worker and Jupyter’s own stdout capture routes cell output. It reuses the REPL’s chunking helpers directly (blob_of_new, chunk_python), which is why the two stay in step.

The playground

playground/src/lib.rs is a WebAssembly shim. It is a separate crate so the core stays dependency-free (only this binding pulls in wasm-bindgen), and it calls the very same pyfun::analyze and pyfun::compile:

#![allow(unused)]
fn main() {
// playground/src/lib.rs
let analysis = pyfun::analyze(source);
// ... then, when clean:
match pyfun::compile(source) { Ok(py) => Some(py), Err(e) => /* one more diagnostic */ }
}

Neither path touches the filesystem or spawns a process, which is exactly what makes them safe in WebAssembly. The result is that the browser shows byte-for-byte what the CLI emits. To close the loop: the playground on this very site is that shim, running the real compiler in your browser.

Where you would add a new LSP capability

A new editor feature is a new request handler in Server::handle in src/lsp/mod.rs, reading the same Analysis bundle the other features use and, if it needs to walk names, extending src/lsp/resolve.rs. Because handle is pure, you test it with JSON in and JSON out before ever touching stdio, and the thin VS Code client needs no change.