CSCI 1730 · Fall 2026
Code
The descriptions below are not substitutes for the lecture/book, nor are they meant to make sense in their absence.
Interpreters
A key detail: The tests in these files are deliberately sparse. That is an expository choice, not something you should emulate! Your homeworks are required to have extensive testing. They’re just left out here to reduce clutter (and to avoid doing your homework for you!).
File |
| What it adds |
| The smallest possible language: numbers, +, and *. No parser yet. Write abstract syntax trees by hand! | |
| A parse function that turns text of type Syntax into the corresponding syntax tree, so you can write much more convenient programs. Observe that single-quotes create values of type Syntax, which is what parse consumes. | |
| Booleans and if. The result of evaluation now needs its own datatype. | |
| Variables and let. Evaluation now needs an environment. | |
| Functions (lam) and application. A function value records only its parameter and body, and is applied in the environment of the call. This is dynamic scope; the tests at the end show the resulting behavior, which is not what we want. | |
| Fixes the above: a function value is now a closure that also records the environment where the lam was evaluated, and the body is evaluated in that environment. The argument, however, must still be evaluated in the caller’s environment; the last test checks this. | |
| Syntactic sugar: subtraction, unary negation, and, and cond. Now features a new datatype to represent surface terms. The key is a desugar function that turns surface programs into core ones. A critical detail is that the interpreter is imported: there is no definition in this file. This shows that we could grow the language without modifying the interpreter at all. |
Type Checkers
Each language comes in three files:
the type checker: the core language’s abstract syntax and type_of, with tests written directly as syntax trees;
the front end: the surface syntax, a parser, and a desugarer (the checker only ever sees the desugared, core program);
the interpreter, which runs a program only if it type-checks, and also shows what happens when programs are run without checking them.
The tests are where the interesting examples are, including programs the checker rejects that would have run fine, and programs it accepts that still go wrong.
Language |
| Features |
| Files |
tc-ops |
| Numbers with +, *, and /; strings with ++ (concatenation); and s[i], the one-character string at position i of s: the one operation that takes both a string and a number. Subtraction and negation are sugar. There are two types, Num and Str. Division by zero and out-of-range indexing type-check, and fail only when run. |
|
Tags and Types
A tiny language of numbers and strings, with + on numbers and concatenation on strings. The point is what happens when a program uses a string where a number is expected (or vice versa). This simulates a (overly simplified) memory representation so we can directly see the effect of type-safety.
File |
| What it shows |
| Values are an ordinary datatype (vNum, vStr), so a mismatch is caught by match: a dynamic error. | |
| Values live in a simulated memory with no tags. Mismatched programs are not caught: they silently misread memory and return nonsense. | |
| Every stored value is preceded by a tag word that is checked on every read, so the mismatches are caught again, as dynamic errors. | |
| Back to untagged memory, with no run-time checks at all, but now a type checker runs first. It rejects the bad programs before they run (static errors), so the checks of the previous file are unnecessary: the unsafe operations are now safe. |
Types for Non-Zero Numbers
Can a type say that the second argument to div is not zero? We represent integers with a datatype that separates zero from everything else, and try to give div a type that excludes zero. Each step comes in Shplait and in Java. The Java files need Java 21 or later, and run directly from source: java alg-dt-rep-0.java.
Files |
| What it shows |
| The datatype Int0, with variants for zero and non-zero, and add. Adding two non-zero numbers always produces the non-zero variant, so 5 + -5 gives a non-zero zero. The test that would catch this is commented out. | |
| A function i that picks the right variant for a number; add now uses it, and the test passes. | |
| Adds div. In Shplait, the non-zero variant is not a type, so div must accept any Int0 and check for zero when it runs. In Java, NZ is a type, so div can demand it. But add and i can only promise an Int0, so their results cannot be passed to div, even when they are not zero; and the ways around this (a cast, a check in NZ’s constructor) are themselves run-time checks. The commented-out tests show each case. |
The Same Ideas in Lean
Lean has dependent types: a type can mention a value, and a value can carry a proof about another value. These files revisit the examples above in Lean 4, using only the core language (no libraries). Each runs with lean file.lean, or in VS Code with the Lean extension. Expected results are in a comment above each line; uncomment a commented-out line to see its error.
File |
| What it shows |
| Int0 as in Shplait: nz accepts any integer, div checks for z when it runs, and nz is a constructor, not a type. | |
| nz now requires a proof that its integer is not zero, with a default that tries to find the proof itself. nz 0 is rejected, and so is nz (a + b) in add, which must use i. div is still partial. | |
| The same, but with no default: every nz is given its proof explicitly. | |
| A non-zero integer as a type: an integer paired with a proof. The divisor 1 + 1 is accepted and 1 + -1 rejected. Proofs can use facts about variables. A value known only at run time still needs a test, but the test produces the proof. | |
| Indexing into an array of characters with any index; an index out of range is caught when the program runs. | |
| An index whose type names the array it belongs to, with a proof that it is in range. Shows proofs about constants, about variables, about a concatenation, and in a loop. |