This will be a relatively short post.
I’ve been watching the OPLSS 2014 lectures given by Ulf Norell on “Programming in Agda”. I really enjoyed his tutorial implementation of the simply typed lambda calculus, both as a demonstration of how to use Agda and as a primer on advanced techniques for achieving type safety guarantees for such an interpreter.
Here’s the link to OPLSS 2014.
Here’s a link to several tweets I made about it.
The Agda code given in the video no longer compiles. After some tinkering, I’ve managed to get it compiling with the latest Agda release. The source is available here for download, and is included below for web browsing. I’ve heavily annotated it to make it easier to understand for readers not familiar with emacs, Agda, or mathematical symbols.
The coolest thing about the context-management technique demonstrated below? It shows just how much can be proven with dependent types. Notice that there’s no need to use Either/Maybe to track semantic errors, because those errors are impossible by construction.
It necessarily means that the introduction rules (“constructors”) for all the terms are very demanding (e.g., when you parse a variable, you’re also forced to update the associated Context), but the end result is an evaluator that can’t go wrong.
Happy reading!
{-
Simply Typed Lambda Calculus in Agda
source:
- OPLSS 2014: Ulf Norell - Programming in Agda: Lecture 1
- https://www.cs.uoregon.edu/research/summerschool/summer14/curriculum.html
The following annotated tutorial assumes emacs>=24.3 and Agda>=2.4.2.3
Modifications from original:
* Tutorial used an older version of Agda that seemed to be less strict
about scoping and fixity declarations
* Made All (⊢ , []) instead of (∷ , [])
* Added infixr 3 _⊢_ for All type
* Avoids collisions with List definitions from Prelude
Keyboard notation: 'C-c C-n; eval env e <enter>' means:
* Hold Ctrl
* Press c
* Press n
* Release Ctrl
* Type 'eval env e'
* Press enter
C-c: Ctrl-c
M-c: Meta-c (meta is usually Alt, could be Esc or ...?)
- Quick test: 'M-x' should show 'M-x' at the bottom of your emacs window
Some useful commands (assuming emacs + agda 2.4.2.3):
* C-c C-l : type check whole buffer, replacing ? w/ goals { }0
* C-c C-c : [at goal] split case analysis on a variable
* C-c C-a : [at goal] try to auto solve a goal
* C-c C-n : evaluate expression typed in; sent to agda REPL
Some useful unicode inputs, thanks to agda2-mode:
* '\in' means: type '\' then 'i' then 'n'
|----------------+----------------+--------------------------------------------------+
| Input Sequence | Unicode Output | Description |
|----------------+----------------+--------------------------------------------------+
| \in | ∈ | Set membership |
| \:: | ∷ | Attach to left of list |
| \' | ′ | Prime, other |
| \-> | → | Function arrow; implication; implies |
| \forall | ∀ | For all... |
| \Gamma | Γ | A common variable to represent contexts |
| \|- | ⊢ | Entails; given thing on left, right must be true |
|----------------+----------------+--------------------------------------------------+
-}
module STLC where
-- import the special OPLSS Agda Prelude
-- download here: https://github.com/UlfNorell/agda-summer-school
-- follow these instructions:
-- - https://github.com/UlfNorell/agda-summer-school#getting-the-libraries
open import Prelude
-- Type C-c C-l now to make sure your environment is ready
-- All good? Nice!
--------------------------------------------------------------------------------
-- Simply Typed Lambda Calculus --
--------------------------------------------------------------------------------
-- The types for our lambda calculus
-- T := nat | bool
data Type : Set where
nat : Type
bool : Type
-- a type synonym
Cxt = List Type
-- Set membership
infix 3 _∈_
data _∈_ {A : Set} (x : A) : List A → Set where
zero : ∀ {xs} → x ∈ x ∷ xs
suc : ∀ {y xs} → x ∈ xs → x ∈ y ∷ xs
-- Lambda calculus terms
-- t := var | lit n | true | false | less | plus | if
-- Uses De Bruijn indexes for var scoping/lookup
data Expr (Γ : Cxt) : Type → Set where
var : ∀ {a} → a ∈ Γ → Expr Γ a
lit : {a : Type} (n : Nat) → Expr Γ nat
true : Expr Γ bool
false : Expr Γ bool
less : (a b : Expr Γ nat) → Expr Γ bool
plus : (a b : Expr Γ nat) → Expr Γ nat
if : {t : Type} (a : Expr Γ bool) (b c : Expr Γ t) → Expr Γ t
-- Mapping from Lambda Calculus types to Agda types
Value : Type → Set
Value nat = Nat
Value bool = Bool
-- Context assertions
infixr 3 _⊢_
data All {A : Set} (P : A → Set) : List A → Set where
[] : All P []
_⊢_ : ∀ {x xs} → P x → All P xs → All P (x ∷ xs)
-- Alternative context assertions
data Any {A : Set} (P : A → Set) : List A → Set where
zero : ∀ {x xs} → P x → Any P (x ∷ xs)
suc : ∀ {x xs} → Any P xs → Any P (x ∷ xs)
-- Alternative context membership
_∈′_ : {A : Set} (x : A) → List A → Set
x ∈′ xs = Any (λ y → x ≡ y) xs
-- making sure an environment is well-typed
lookup∈ : ∀ {A} {P : A → Set} {x xs} → All P xs → x ∈ xs → P x
-- impossible case, but needed to make Agda happy
lookup∈ [] ()
-- actual environment verification
lookup∈ (x ⊢ ps) zero = x
lookup∈ (_ ⊢ ps) (suc i) = lookup∈ ps i
-- Verify a context and convert it to an variable lookup Environment
Env : Cxt → Set
Env Γ = All Value Γ
-- evaluator for SLTC
eval : ∀ {Γ t} → Env Γ → (Expr Γ t) → Value t
eval env (var x) = lookup∈ env x
eval env (lit n) = n
eval env true = true
eval env false = false
eval env (less x y) = eval env x < eval env y
eval env (plus x y) = eval env x + eval env y
eval env (if p x y) = if eval env p then eval env x else eval env y
--------------------------------------------------------------------------------
-- Evaluator Demo --
--------------------------------------------------------------------------------
Γ : Cxt
Γ = nat ∷ bool ∷ []
env : Env Γ
env = 5 ⊢ false ⊢ []
-- to see output, type C-c C-l <enter> C-c C-n <enter> eval env e
-- [load buffer] [eval input]
-- Should see '9' below
e : Expr Γ nat
e = if (var (suc zero)) (var zero) (plus (lit 4) (var zero))