Exam: TSPL Exam file
module Exam where
IMPORTANT For ease of marking, when modifying the given code please write
-- begin
-- endbefore and after code you add, to indicate your changes.
Imports
import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; sym; trans; cong; _≢_) open import Data.Empty using (⊥; ⊥-elim) open import Data.Nat using (ℕ; zero; suc; _<_; _≤_; _≤?_; z≤n; s≤s) open import Data.List using (List; []; _∷_; _++_) open import Data.Product using (∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩) open import Data.String using (String; _≟_) open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Nullary.Decidable using (False; toWitnessFalse)
Problem 1
module Problem1 where open import Function using (_∘_)
Remember to indent all code by two spaces.
(a)
(b)
Problem 2
Remember to indent all code by two spaces.
module Problem2 where
Infix declarations
infix 4 _⊢_ infix 4 _∋_ infixl 5 _,_ infixr 7 _⇒_ infix 5 ƛ_ infix 5 μ_ infixl 7 _·_ infix 8 `suc_ infix 9 `_ infix 9 S_
Types and contexts
data Type : Set where _⇒_ : Type → Type → Type `ℕ : Type data Context : Set where ∅ : Context _,_ : Context → Type → Context
Variables and the lookup judgment
data _∋_ : Context → Type → Set where Z : ∀ {Γ A} ---------- → Γ , A ∋ A S_ : ∀ {Γ A B} → Γ ∋ A --------- → Γ , B ∋ A
Terms and the typing judgment
data _⊢_ : Context → Type → Set where `_ : ∀ {Γ} {A} → Γ ∋ A ------ → Γ ⊢ A ƛ_ : ∀ {Γ} {A B} → Γ , A ⊢ B ---------- → Γ ⊢ A ⇒ B _·_ : ∀ {Γ} {A B} → Γ ⊢ A ⇒ B → Γ ⊢ A ---------- → Γ ⊢ B `zero : ∀ {Γ} ---------- → Γ ⊢ `ℕ `suc_ : ∀ {Γ} → Γ ⊢ `ℕ ------- → Γ ⊢ `ℕ case : ∀ {Γ A} → Γ ⊢ `ℕ → Γ ⊢ A → Γ , `ℕ ⊢ A ----------- → Γ ⊢ A μ_ : ∀ {Γ A} → Γ , A ⊢ A ---------- → Γ ⊢ A
Renaming
ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) ----------------------------------- → (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A) ext ρ Z = Z ext ρ (S x) = S (ρ x) rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) ------------------------ → (∀ {A} → Γ ⊢ A → Δ ⊢ A) rename ρ (` x) = ` (ρ x) rename ρ (ƛ N) = ƛ (rename (ext ρ) N) rename ρ (L · M) = (rename ρ L) · (rename ρ M) rename ρ (`zero) = `zero rename ρ (`suc M) = `suc (rename ρ M) rename ρ (case L M N) = case (rename ρ L) (rename ρ M) (rename (ext ρ) N) rename ρ (μ N) = μ (rename (ext ρ) N)
Simultaneous Substitution
exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) ---------------------------------- → (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A) exts σ Z = ` Z exts σ (S x) = rename S_ (σ x) subst : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) ------------------------ → (∀ {A} → Γ ⊢ A → Δ ⊢ A) subst σ (` k) = σ k subst σ (ƛ N) = ƛ (subst (exts σ) N) subst σ (L · M) = (subst σ L) · (subst σ M) subst σ (`zero) = `zero subst σ (`suc M) = `suc (subst σ M) subst σ (case L M N) = case (subst σ L) (subst σ M) (subst (exts σ) N) subst σ (μ N) = μ (subst (exts σ) N)
Single and double substitution
_[_] : ∀ {Γ A B} → Γ , A ⊢ B → Γ ⊢ A --------- → Γ ⊢ B _[_] {Γ} {A} {B} N V = subst {Γ , A} {Γ} σ {B} N where σ : ∀ {B} → Γ , A ∋ B → Γ ⊢ B σ Z = V σ (S x) = ` x _[_][_] : ∀ {Γ A B C} → Γ , A , B ⊢ C → Γ ⊢ A → Γ ⊢ B --------- → Γ ⊢ C _[_][_] {Γ} {A} {B} {C} N V W = subst {Γ , A , B} {Γ} σ {C} N where σ : ∀ {C} → Γ , A , B ∋ C → Γ ⊢ C σ Z = W σ (S Z) = V σ (S (S x)) = ` x
Values
data Value : ∀ {Γ A} → Γ ⊢ A → Set where V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} --------------------------- → Value (ƛ N) V-zero : ∀ {Γ} ----------------- → Value (`zero {Γ}) V-suc : ∀ {Γ} {V : Γ ⊢ `ℕ} → Value V -------------- → Value (`suc V)
Reduction
infix 2 _—→_ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A} → L —→ L′ ----------------- → L · M —→ L′ · M ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A} → Value V → M —→ M′ -------------- → V · M —→ V · M′ β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A} → Value W ------------------- → (ƛ N) · W —→ N [ W ] ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ} → M —→ M′ ---------------- → `suc M —→ `suc M′ ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A} → L —→ L′ -------------------------- → case L M N —→ case L′ M N β-zero : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A} ------------------- → case `zero M N —→ M β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A} → Value V ----------------------------- → case (`suc V) M N —→ N [ V ] β-μ : ∀ {Γ A} {N : Γ , A ⊢ A} --------------- → μ N —→ N [ μ N ]
Reflexive and transitive closure
infix 2 _—↠_ infix 1 begin_ infixr 2 _—→⟨_⟩_ infix 3 _∎ data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where _∎ : (M : Γ ⊢ A) ------ → M —↠ M step—→ : (L : Γ ⊢ A) {M N : Γ ⊢ A} → M —↠ N → L —→ M ------ → L —↠ N pattern _—→⟨_⟩_ L L—→M M—↠N = step—→ L M—↠N L—→M begin_ : ∀ {Γ A} {M N : Γ ⊢ A} → M —↠ N ------ → M —↠ N begin M—↠N = M—↠N
Progress
data Progress {A} (M : ∅ ⊢ A) : Set where step : ∀ {N : ∅ ⊢ A} → M —→ N ------------- → Progress M done : Value M ---------- → Progress M progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M progress (` ()) progress (ƛ N) = done V-ƛ progress (L · M) with progress L ... | step L—→L′ = step (ξ-·₁ L—→L′) ... | done V-ƛ with progress M ... | step M—→M′ = step (ξ-·₂ V-ƛ M—→M′) ... | done VM = step (β-ƛ VM) progress (`zero) = done V-zero progress (`suc M) with progress M ... | step M—→M′ = step (ξ-suc M—→M′) ... | done VM = done (V-suc VM) progress (case L M N) with progress L ... | step L—→L′ = step (ξ-case L—→L′) ... | done V-zero = step (β-zero) ... | done (V-suc VL) = step (β-suc VL) progress (μ N) = step (β-μ)
Evaluation
record Gas : Set where constructor gas field amount : ℕ data Finished {Γ A} (N : Γ ⊢ A) : Set where done : Value N ---------- → Finished N out-of-gas : ---------- Finished N data Steps : ∀ {A} → ∅ ⊢ A → Set where steps : ∀ {A} {L N : ∅ ⊢ A} → L —↠ N → Finished N ---------- → Steps L eval : ∀ {A} → Gas → (L : ∅ ⊢ A) ----------- → Steps L eval (gas zero) L = steps (L ∎) out-of-gas eval (gas (suc m)) L with progress L ... | done VL = steps (L ∎) (done VL) ... | step {M} L—→M with eval (gas m) M ... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin
Example
Here is a term (in extrinsic style) to add two numbers.
plus = μ "plus" ⇒ ƛ "m" ⇒ ƛ n ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ ` "plus" · ` "m" · ` "n" ]Here is a sample reduction demonstrating that two plus two is four.
pattern two = `suc `suc `zero pattern plus = μ ƛ ƛ (case (` S Z) (` Z) (`suc (` S S S Z · ` Z · ` S Z))) 2+2 : ∅ ⊢ `ℕ 2+2 = plus · two · two _ : 2+2 —↠ `suc `suc `suc `suc `zero _ = begin plus · two · two —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩ (ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z))) · two · two —→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩ (ƛ case two (` Z) (`suc (plus · ` Z · ` S Z))) · two —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩ case two two (`suc (plus · ` Z · two)) —→⟨ β-suc (V-suc V-zero) ⟩ `suc (plus · `suc `zero · two) —→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩ `suc ((ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z))) · `suc `zero · two) —→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩ `suc ((ƛ case (`suc `zero) (` Z) (`suc (plus · ` Z · ` S Z))) · two) —→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩ `suc (case (`suc `zero) (two) (`suc (plus · ` Z · two))) —→⟨ ξ-suc (β-suc V-zero) ⟩ `suc (`suc (plus · `zero · two)) —→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩ `suc (`suc ((ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z))) · `zero · two)) —→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩ `suc (`suc ((ƛ case `zero (` Z) (`suc (plus · ` Z · ` S Z))) · two)) —→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩ `suc (`suc (case `zero (two) (`suc (plus · ` Z · two)))) —→⟨ ξ-suc (ξ-suc β-zero) ⟩ `suc (`suc (`suc (`suc `zero))) ∎
Problem 3
Remember to indent all code by two spaces.
module Problem3 where
Syntax
infix 4 _∋_⦂_ infix 4 _⊢_↑_ infix 4 _⊢_↓_ infixl 5 _,_⦂_ infixr 7 _⇒_ infix 5 ƛ_⇒_ infix 5 μ_⇒_ infix 6 _↑ infix 6 _↓_ infixl 7 _·_ infix 8 `suc_ infix 9 `_
Types
data Type : Set where _⇒_ : Type → Type → Type `ℕ : Type
Identifiers
Id : Set Id = String
Contexts
data Context : Set where ∅ : Context _,_⦂_ : Context → Id → Type → Context
Terms
data Term⁺ : Set data Term⁻ : Set data Term⁺ where `_ : Id → Term⁺ _·_ : Term⁺ → Term⁻ → Term⁺ _↓_ : Term⁻ → Type → Term⁺ data Term⁻ where ƛ_⇒_ : Id → Term⁻ → Term⁻ `zero : Term⁻ `suc_ : Term⁻ → Term⁻ `case_[zero⇒_|suc_⇒_] : Term⁺ → Term⁻ → Id → Term⁻ → Term⁻ μ_⇒_ : Id → Term⁻ → Term⁻ _↑ : Term⁺ → Term⁻
Lookup
data _∋_⦂_ : Context → Id → Type → Set where Z : ∀ {Γ x A} -------------------- → Γ , x ⦂ A ∋ x ⦂ A S : ∀ {Γ x y A B} → x ≢ y → Γ ∋ x ⦂ A ----------------- → Γ , y ⦂ B ∋ x ⦂ A
Bidirectional type checking
data _⊢_↑_ : Context → Term⁺ → Type → Set data _⊢_↓_ : Context → Term⁻ → Type → Set data _⊢_↑_ where ⊢` : ∀ {Γ A x} → Γ ∋ x ⦂ A ----------- → Γ ⊢ ` x ↑ A _·_ : ∀ {Γ L M A B} → Γ ⊢ L ↑ A ⇒ B → Γ ⊢ M ↓ A ------------- → Γ ⊢ L · M ↑ B ⊢↓ : ∀ {Γ M A} → Γ ⊢ M ↓ A --------------- → Γ ⊢ (M ↓ A) ↑ A data _⊢_↓_ where ⊢ƛ : ∀ {Γ x N A B} → Γ , x ⦂ A ⊢ N ↓ B ------------------- → Γ ⊢ ƛ x ⇒ N ↓ A ⇒ B ⊢zero : ∀ {Γ} -------------- → Γ ⊢ `zero ↓ `ℕ ⊢suc : ∀ {Γ M} → Γ ⊢ M ↓ `ℕ --------------- → Γ ⊢ `suc M ↓ `ℕ ⊢case : ∀ {Γ L M x N A} → Γ ⊢ L ↑ `ℕ → Γ ⊢ M ↓ A → Γ , x ⦂ `ℕ ⊢ N ↓ A ------------------------------------- → Γ ⊢ `case L [zero⇒ M |suc x ⇒ N ] ↓ A ⊢μ : ∀ {Γ x N A} → Γ , x ⦂ A ⊢ N ↓ A ----------------- → Γ ⊢ μ x ⇒ N ↓ A ⊢↑ : ∀ {Γ M A B} → Γ ⊢ M ↑ A → A ≡ B ------------- → Γ ⊢ (M ↑) ↓ B
Type equality
_≟Tp_ : (A B : Type) → Dec (A ≡ B) `ℕ ≟Tp `ℕ = yes refl `ℕ ≟Tp (A ⇒ B) = no λ() (A ⇒ B) ≟Tp `ℕ = no λ() (A ⇒ B) ≟Tp (A′ ⇒ B′) with A ≟Tp A′ | B ≟Tp B′ ... | no A≢ | _ = no λ{refl → A≢ refl} ... | yes _ | no B≢ = no λ{refl → B≢ refl} ... | yes refl | yes refl = yes refl
Prerequisites
dom≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → A ≡ A′ dom≡ refl = refl rng≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → B ≡ B′ rng≡ refl = refl ℕ≢⇒ : ∀ {A B} → `ℕ ≢ A ⇒ B ℕ≢⇒ ()
Unique lookup
uniq-∋ : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B uniq-∋ Z Z = refl uniq-∋ Z (S x≢y _) = ⊥-elim (x≢y refl) uniq-∋ (S x≢y _) Z = ⊥-elim (x≢y refl) uniq-∋ (S _ ∋x) (S _ ∋x′) = uniq-∋ ∋x ∋x′
Unique synthesis
uniq-↑ : ∀ {Γ M A B} → Γ ⊢ M ↑ A → Γ ⊢ M ↑ B → A ≡ B uniq-↑ (⊢` ∋x) (⊢` ∋x′) = uniq-∋ ∋x ∋x′ uniq-↑ (⊢L · ⊢M) (⊢L′ · ⊢M′) = rng≡ (uniq-↑ ⊢L ⊢L′) uniq-↑ (⊢↓ ⊢M) (⊢↓ ⊢M′) = refl
Lookup type of a variable in the context
ext∋ : ∀ {Γ B x y} → x ≢ y → ¬ (∃[ A ] Γ ∋ x ⦂ A) ---------------------------- → ¬ (∃[ A ] Γ , y ⦂ B ∋ x ⦂ A) ext∋ x≢y _ ⟨ A , Z ⟩ = x≢y refl ext∋ _ ¬∃ ⟨ A , S _ ⊢x ⟩ = ¬∃ ⟨ A , ⊢x ⟩ lookup : ∀ (Γ : Context) (x : Id) ----------------------- → Dec (∃[ A ] Γ ∋ x ⦂ A) lookup ∅ x = no (λ ()) lookup (Γ , y ⦂ B) x with x ≟ y ... | yes refl = yes ⟨ B , Z ⟩ ... | no x≢y with lookup Γ x ... | no ¬∃ = no (ext∋ x≢y ¬∃) ... | yes ⟨ A , ⊢x ⟩ = yes ⟨ A , S x≢y ⊢x ⟩
Promoting negations
¬arg : ∀ {Γ A B L M} → Γ ⊢ L ↑ A ⇒ B → ¬ (Γ ⊢ M ↓ A) -------------------------- → ¬ (∃[ B′ ] Γ ⊢ L · M ↑ B′) ¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′ ¬switch : ∀ {Γ M A B} → Γ ⊢ M ↑ A → A ≢ B --------------- → ¬ Γ ⊢ (M ↑) ↓ B ¬switch ⊢M A≢B (⊢↑ ⊢M′ A′≡B) rewrite uniq-↑ ⊢M ⊢M′ = A≢B A′≡B
Synthesize and inherit types
synthesize : ∀ (Γ : Context) (M : Term⁺) ----------------------- → Dec (∃[ A ] Γ ⊢ M ↑ A ) inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type) --------------- → Dec (Γ ⊢ M ↓ A) synthesize Γ (` x) with lookup Γ x ... | no ¬∃ = no (λ{ ⟨ A , ⊢` ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ }) ... | yes ⟨ A , ∋x ⟩ = yes ⟨ A , ⊢` ∋x ⟩ synthesize Γ (L · M) with synthesize Γ L ... | no ¬∃ = no (λ{ ⟨ _ , ⊢L · _ ⟩ → ¬∃ ⟨ _ , ⊢L ⟩ }) ... | yes ⟨ `ℕ , ⊢L ⟩ = no (λ{ ⟨ _ , ⊢L′ · _ ⟩ → ℕ≢⇒ (uniq-↑ ⊢L ⊢L′) }) ... | yes ⟨ A ⇒ B , ⊢L ⟩ with inherit Γ M A ... | no ¬⊢M = no (¬arg ⊢L ¬⊢M) ... | yes ⊢M = yes ⟨ B , ⊢L · ⊢M ⟩ synthesize Γ (M ↓ A) with inherit Γ M A ... | no ¬⊢M = no (λ{ ⟨ _ , ⊢↓ ⊢M ⟩ → ¬⊢M ⊢M }) ... | yes ⊢M = yes ⟨ A , ⊢↓ ⊢M ⟩ inherit Γ (ƛ x ⇒ N) `ℕ = no (λ()) inherit Γ (ƛ x ⇒ N) (A ⇒ B) with inherit (Γ , x ⦂ A) N B ... | no ¬⊢N = no (λ{ (⊢ƛ ⊢N) → ¬⊢N ⊢N }) ... | yes ⊢N = yes (⊢ƛ ⊢N) inherit Γ `zero `ℕ = yes ⊢zero inherit Γ `zero (A ⇒ B) = no (λ()) inherit Γ (`suc M) `ℕ with inherit Γ M `ℕ ... | no ¬⊢M = no (λ{ (⊢suc ⊢M) → ¬⊢M ⊢M }) ... | yes ⊢M = yes (⊢suc ⊢M) inherit Γ (`suc M) (A ⇒ B) = no (λ()) inherit Γ (`case L [zero⇒ M |suc x ⇒ N ]) A with synthesize Γ L ... | no ¬∃ = no (λ{ (⊢case ⊢L _ _) → ¬∃ ⟨ `ℕ , ⊢L ⟩}) ... | yes ⟨ _ ⇒ _ , ⊢L ⟩ = no (λ{ (⊢case ⊢L′ _ _) → ℕ≢⇒ (uniq-↑ ⊢L′ ⊢L) }) ... | yes ⟨ `ℕ , ⊢L ⟩ with inherit Γ M A ... | no ¬⊢M = no (λ{ (⊢case _ ⊢M _) → ¬⊢M ⊢M }) ... | yes ⊢M with inherit (Γ , x ⦂ `ℕ) N A ... | no ¬⊢N = no (λ{ (⊢case _ _ ⊢N) → ¬⊢N ⊢N }) ... | yes ⊢N = yes (⊢case ⊢L ⊢M ⊢N) inherit Γ (μ x ⇒ N) A with inherit (Γ , x ⦂ A) N A ... | no ¬⊢N = no (λ{ (⊢μ ⊢N) → ¬⊢N ⊢N }) ... | yes ⊢N = yes (⊢μ ⊢N) inherit Γ (M ↑) B with synthesize Γ M ... | no ¬∃ = no (λ{ (⊢↑ ⊢M _) → ¬∃ ⟨ _ , ⊢M ⟩ }) ... | yes ⟨ A , ⊢M ⟩ with A ≟Tp B ... | no A≢B = no (¬switch ⊢M A≢B) ... | yes A≡B = yes (⊢↑ ⊢M A≡B)
Example
two : Term⁻ two = `suc (`suc `zero) plus : Term⁺ plus = (μ "p" ⇒ ƛ "m" ⇒ ƛ "n" ⇒ `case (` "m") [zero⇒ ` "n" ↑ |suc "m" ⇒ `suc (` "p" · (` "m" ↑) · (` "n" ↑) ↑) ]) ↓ (`ℕ ⇒ `ℕ ⇒ `ℕ) 2+2 : Term⁺ 2+2 = plus · two · twoA smart constructor, to make it easier to access a variable.
S′ : ∀ {Γ x y A B} → {x≢y : False (x ≟ y)} → Γ ∋ x ⦂ A ------------------ → Γ , y ⦂ B ∋ x ⦂ A S′ {x≢y = x≢y} x = S (toWitnessFalse x≢y) xHere is the result of typing two plus two on naturals:
⊢2+2 : ∅ ⊢ 2+2 ↑ `ℕ ⊢2+2 = (⊢↓ (⊢μ (⊢ƛ (⊢ƛ (⊢case (⊢` (S′ Z)) (⊢↑ (⊢` Z) refl) (⊢suc (⊢↑ (⊢` (S′ (S′ (S′ Z))) · ⊢↑ (⊢` Z) refl · ⊢↑ (⊢` (S′ Z)) refl) refl)))))) · ⊢suc (⊢suc ⊢zero) · ⊢suc (⊢suc ⊢zero))We confirm that synthesis on the relevant term returns natural as the type and the above derivation:
_ : synthesize ∅ 2+2 ≡ yes ⟨ `ℕ , ⊢2+2 ⟩ _ = refl