More: Additional constructs of simply-typed lambda calculus

Wen Kokke, Jeremy Siek, Philip Wadler

Prev • Index • Next

module plfa.part2.More where
Shift+Enter to run
Agda
PLFA+

So far, we have focussed on a relatively minimal language, based on Plotkin's PCF, which supports functions, naturals, and fixpoints. In this chapter we extend our calculus to support the following:

  • primitive numbers

  • let bindings

  • products

  • an alternative formulation of products

  • sums

  • unit type

  • an alternative formulation of unit type

  • empty type

  • lists

All of the data types should be familiar from Part I of this textbook. For let and the alternative formulations we show how they translate to other constructs in the calculus. Most of the description will be informal. We show how to formalise the first four constructs and leave the rest as an exercise for the reader.

Our informal descriptions will be in the style of Chapter Lambda, using extrinsically-typed terms, while our formalisation will be in the style of Chapter DeBruijn, using intrinsically-typed terms.

By now, explaining with symbols should be more concise, more precise, and easier to follow than explaining in prose. For each construct, we give syntax, typing, reductions, and an example. We also give translations where relevant; formally establishing the correctness of translations will be the subject of the next chapter.

Primitive numbers

We define a Nat type equivalent to the built-in natural number type with multiplication as a primitive operation on numbers:

Syntax

A, B, C ::= ...                     Types
  Nat                                 primitive natural numbers
L, M, N ::= ...                     Terms
  con c                               constant
  L `* M                              multiplication
V, W ::= ...                        Values
  con c                               constant
Agda

Typing

The hypothesis of the con rule is unusual, in that it refers to a typing judgment of Agda rather than a typing judgment of the defined calculus:

c : ℕ
--------------- con
Γ ⊢ con c : Nat
Γ ⊢ L : Nat
Γ ⊢ M : Nat
---------------- _`*_
Γ ⊢ L `* M : Nat
Agda

Reduction

A rule that defines a primitive directly, such as the last rule below, is called a δ rule. Here the δ rule defines multiplication of primitive numbers in terms of multiplication of naturals as given by the Agda standard prelude:

L —→ L′
----------------- ξ-*₁
L `* M —→ L′ `* M
M —→ M′
----------------- ξ-*₂
V `* M —→ V `* M′
----------------------------- δ-*
con c `* con d —→ con (c * d)
Agda

Example

Here is a function to cube a primitive number:

cube : ∅ ⊢ Nat ⇒ Nat
cube = ƛ x ⇒ x `* x `* x
Agda

Let bindings

Let bindings affect only the syntax of terms; they introduce no new types or values:

Syntax

L, M, N ::= ...                     Terms
  `let x `= M `in N                   let
Agda

Typing

Γ ⊢ M ⦂ A
Γ , x ⦂ A ⊢ N ⦂ B
------------------------- `let
Γ ⊢ `let x `= M `in N ⦂ B
Agda

Reduction

M —→ M′
--------------------------------------- ξ-let
`let x `= M `in N —→ `let x `= M′ `in N
--------------------------------- β-let
`let x `= V `in N —→ N [ x := V ]
Agda

Example

Here is a function to raise a primitive number to the tenth power:

exp10 : ∅ ⊢ Nat ⇒ Nat
exp10 = ƛ x ⇒ `let x2  `= x  `* x  `in
              `let x4  `= x2 `* x2 `in
              `let x5  `= x4 `* x  `in
              x5 `* x5
Agda

Translation

We can translate each let term into an application of an abstraction:

(`let x `= M `in N) †  =  (ƛ x ⇒ (N †)) · (M †)
Agda

Here M † is the translation of term M from a calculus with the construct to a calculus without the construct.

Products {#products}

Syntax

A, B, C ::= ...                     Types
  A `× B                              product type
L, M, N ::= ...                     Terms
  `⟨ M , N ⟩                          pair
  `proj₁ L                            project first component
  `proj₂ L                            project second component
V, W ::= ...                        Values
  `⟨ V , W ⟩                          pair
Agda

Typing

Γ ⊢ M ⦂ A
Γ ⊢ N ⦂ B
----------------------- `⟨_,_⟩ or `×-I
Γ ⊢ `⟨ M , N ⟩ ⦂ A `× B
Γ ⊢ L ⦂ A `× B
---------------- `proj₁ or `×-E₁
Γ ⊢ `proj₁ L ⦂ A
Γ ⊢ L ⦂ A `× B
---------------- `proj₂ or `×-E₂
Γ ⊢ `proj₂ L ⦂ B
Agda

Reduction

M —→ M′
------------------------- ξ-⟨,⟩₁
`⟨ M , N ⟩ —→ `⟨ M′ , N ⟩
N —→ N′
------------------------- ξ-⟨,⟩₂
`⟨ V , N ⟩ —→ `⟨ V , N′ ⟩
L —→ L′
--------------------- ξ-proj₁
`proj₁ L —→ `proj₁ L′
L —→ L′
--------------------- ξ-proj₂
`proj₂ L —→ `proj₂ L′
---------------------- β-proj₁
`proj₁ `⟨ V , W ⟩ —→ V
---------------------- β-proj₂
`proj₂ `⟨ V , W ⟩ —→ W
Agda

Example

Here is a function to swap the components of a pair:

swap× : ∅ ⊢ A `× B ⇒ B `× A
swap× = ƛ z ⇒ `⟨ proj₂ z , proj₁ z ⟩
Agda

Alternative formulation of products

There is an alternative formulation of products, where in place of two ways to eliminate the type we have a case term that binds two variables. We repeat the syntax in full, but only give the new type and reduction rules:

Syntax

A, B, C ::= ...                     Types
  A `× B                              product type
L, M, N ::= ...                     Terms
  `⟨ M , N ⟩                          pair
  case× L [⟨ x , y ⟩⇒ M ]             case
V, W ::=                            Values
  `⟨ V , W ⟩                          pair
Agda

Typing

Γ ⊢ L ⦂ A `× B
Γ , x ⦂ A , y ⦂ B ⊢ N ⦂ C
------------------------------- case× or ×-E
Γ ⊢ case× L [⟨ x , y ⟩⇒ N ] ⦂ C
Agda

Reduction

L —→ L′
--------------------------------------------------- ξ-case×
case× L [⟨ x , y ⟩⇒ N ] —→ case× L′ [⟨ x , y ⟩⇒ N ]
--------------------------------------------------------- β-case×
case× `⟨ V , W ⟩ [⟨ x , y ⟩⇒ N ] —→ N [ x := V ][ y := W ]
Agda

Example

Here is a function to swap the components of a pair rewritten in the new notation:

swap×-case : ∅ ⊢ A `× B ⇒ B `× A
swap×-case = ƛ z ⇒ case× z
                     [⟨ x , y ⟩⇒ `⟨ y , x ⟩ ]
Agda

Translation

We can translate the alternative formulation into the one with projections:

  (case× L [⟨ x , y ⟩⇒ N ]) †
=
  `let z `= (L †) `in
  `let x `= `proj₁ z `in
  `let y `= `proj₂ z `in
  (N †)
Agda

Here z is a variable that does not appear free in N. We refer to such a variable as fresh.

One might think that we could instead use a more compact translation:

-- WRONG
  (case× L [⟨ x , y ⟩⇒ N ]) †
=
  (N †) [ x := proj₁ (L †) ][ y := proj₂ (L †) ]
Agda

But this behaves differently. The first term always reduces L before N, and it computes proj₁ and proj₂ exactly once. The second term does not reduce L to a value before reducing N, and depending on how many times and where x and y appear in N, it may reduce L many times or not at all, and it may compute proj₁ and proj₂ many times or not at all.

We can also translate back the other way:

(`proj₁ L) ‡  =  case× (L ‡) [⟨ x , y ⟩⇒ x ]
(`proj₂ L) ‡  =  case× (L ‡) [⟨ x , y ⟩⇒ y ]
Agda

Sums {#sums}

Syntax

A, B, C ::= ...                     Types
  A `⊎ B                              sum type
L, M, N ::= ...                     Terms
  `inj₁ M                             inject first component
  `inj₂ N                             inject second component
  case⊎ L [inj₁ x ⇒ M |inj₂ y ⇒ N ]    case
V, W ::= ...                        Values
  `inj₁ V                             inject first component
  `inj₂ W                             inject second component
Agda

Typing

Γ ⊢ M ⦂ A
-------------------- `inj₁ or ⊎-I₁
Γ ⊢ `inj₁ M ⦂ A `⊎ B
Γ ⊢ N ⦂ B
-------------------- `inj₂ or ⊎-I₂
Γ ⊢ `inj₂ N ⦂ A `⊎ B
Γ ⊢ L ⦂ A `⊎ B
Γ , x ⦂ A ⊢ M ⦂ C
Γ , y ⦂ B ⊢ N ⦂ C
----------------------------------------- case⊎ or ⊎-E
Γ ⊢ case⊎ L [inj₁ x ⇒ M |inj₂ y ⇒ N ] ⦂ C
Agda

Reduction

M —→ M′
------------------- ξ-inj₁
`inj₁ M —→ `inj₁ M′
N —→ N′
------------------- ξ-inj₂
`inj₂ N —→ `inj₂ N′
L —→ L′
---------------------------------------------------------------------- ξ-case⊎
case⊎ L [inj₁ x ⇒ M |inj₂ y ⇒ N ] —→ case⊎ L′ [inj₁ x ⇒ M |inj₂ y ⇒ N ]
--------------------------------------------------------- β-inj₁
case⊎ (`inj₁ V) [inj₁ x ⇒ M |inj₂ y ⇒ N ] —→ M [ x := V ]
--------------------------------------------------------- β-inj₂
case⊎ (`inj₂ W) [inj₁ x ⇒ M |inj₂ y ⇒ N ] —→ N [ y := W ]
Agda

Example

Here is a function to swap the components of a sum:

swap⊎ : ∅ ⊢ A `⊎ B ⇒ B `⊎ A
swap⊎ = ƛ z ⇒ case⊎ z
                [inj₁ x ⇒ `inj₂ x
                |inj₂ y ⇒ `inj₁ y ]
Agda

Unit type

For the unit type, there is a way to introduce values of the type but no way to eliminate values of the type. There are no reduction rules.

Syntax

A, B, C ::= ...                     Types
  `⊤                                  unit type
L, M, N ::= ...                     Terms
  `tt                                 unit value
V, W ::= ...                        Values
  `tt                                 unit value
Agda

Typing

------------ `tt or ⊤-I
Γ ⊢ `tt ⦂ `⊤
Agda

Reduction

(none)

Example

Here is the isomorphism between A and A `× `⊤:

to×⊤ : ∅ ⊢ A ⇒ A `× `⊤
to×⊤ = ƛ x ⇒ `⟨ x , `tt ⟩
from×⊤ : ∅ ⊢ A `× `⊤ ⇒ A
from×⊤ = ƛ z ⇒ proj₁ z
Agda

Alternative formulation of unit type

There is an alternative formulation of the unit type, where in place of no way to eliminate the type we have a case term that binds zero variables. We repeat the syntax in full, but only give the new type and reduction rules:

Syntax

A, B, C ::= ...                     Types
  `⊤                                  unit type
L, M, N ::= ...                     Terms
  `tt                                 unit value
  `case⊤ L [tt⇒ N ]                   case
V, W ::= ...                        Values
  `tt                                 unit value
Agda

Typing

Γ ⊢ L ⦂ `⊤
Γ ⊢ M ⦂ A
------------------------ case⊤ or ⊤-E
Γ ⊢ case⊤ L [tt⇒ M ] ⦂ A
Agda

Reduction

L —→ L′
------------------------------------- ξ-case⊤
case⊤ L [tt⇒ M ] —→ case⊤ L′ [tt⇒ M ]
----------------------- β-case⊤
case⊤ `tt [tt⇒ M ] —→ M
Agda

Example

Here is half the isomorphism between A and A `× `⊤ rewritten in the new notation:

from×⊤-case : ∅ ⊢ A `× `⊤ ⇒ A
from×⊤-case = ƛ z ⇒ case× z
                      [⟨ x , y ⟩⇒ case⊤ y
                                    [tt⇒ x ] ]
Agda

Translation

We can translate the alternative formulation into one without case:

(case⊤ L [tt⇒ M ]) †  =  `let z `= (L †) `in (M †)
Agda

Here z is a variable that does not appear free in M.

Empty type

For the empty type, there is a way to eliminate values of the type but no way to introduce values of the type. There are no values of the type and no β rule, but there is a ξ rule. The case⊥ construct plays a role similar to ⊥-elim in Agda:

Syntax

A, B, C ::= ...                     Types
  `⊥                                  empty type
L, M, N ::= ...                     Terms
  case⊥ L []                          case
Agda

Typing

Γ ⊢ L ⦂ `⊥
------------------ case⊥ or ⊥-E
Γ ⊢ case⊥ L [] ⦂ A
Agda

Reduction

L —→ L′
------------------------- ξ-case⊥
case⊥ L [] —→ case⊥ L′ []
Agda

Example

Here is the isomorphism between A and A `⊎ `⊥:

to⊎⊥ : ∅ ⊢ A ⇒ A `⊎ `⊥
to⊎⊥ = ƛ x ⇒ `inj₁ x
from⊎⊥ : ∅ ⊢ A `⊎ `⊥ ⇒ A
from⊎⊥ = ƛ z ⇒ case⊎ z
                 [inj₁ x ⇒ x
                 |inj₂ y ⇒ case⊥ y
                             [] ]
Agda

Lists

Syntax

A, B, C ::= ...                     Types
  `List A                             list type
L, M, N ::= ...                     Terms
  `[]                                 nil
  M `∷ N                              cons
  caseL L [[]⇒ M | x ∷ y ⇒ N ]        case
V, W ::= ...                        Values
  `[]                                 nil
  V `∷ W                              cons
Agda

Typing

----------------- `[] or List-I₁
Γ ⊢ `[] ⦂ `List A
Γ ⊢ M ⦂ A
Γ ⊢ N ⦂ `List A
-------------------- _`∷_ or List-I₂
Γ ⊢ M `∷ N ⦂ `List A
Γ ⊢ L ⦂ `List A
Γ ⊢ M ⦂ B
Γ , x ⦂ A , xs ⦂ `List A ⊢ N ⦂ B
-------------------------------------- caseL or List-E
Γ ⊢ caseL L [[]⇒ M | x ∷ xs ⇒ N ] ⦂ B
Agda

Reduction

M —→ M′
----------------- ξ-∷₁
M `∷ N —→ M′ `∷ N
N —→ N′
----------------- ξ-∷₂
V `∷ N —→ V `∷ N′
L —→ L′
--------------------------------------------------------------- ξ-caseL
caseL L [[]⇒ M | x ∷ xs ⇒ N ] —→ caseL L′ [[]⇒ M | x ∷ xs ⇒ N ]
------------------------------------ β-[]
caseL `[] [[]⇒ M | x ∷ xs ⇒ N ] —→ M
--------------------------------------------------------------- β-∷
caseL (V `∷ W) [[]⇒ M | x ∷ xs ⇒ N ] —→ N [ x := V ][ xs := W ]
Agda

Example

Here is the map function for lists:

mapL : ∅ ⊢ (A ⇒ B) ⇒ `List A ⇒ `List B
mapL = μ mL ⇒ ƛ f ⇒ ƛ xs ⇒
         caseL xs
           [[]⇒ `[]
           | x ∷ xs ⇒ f · x `∷ mL · f · xs ]
Agda

Formalisation

We now show how to formalise

  • primitive numbers

  • let bindings

  • products

  • an alternative formulation of products

and leave formalisation of the remaining constructs as an exercise.

Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _*_)
open import Relation.Nullary using (¬_)
Shift+Enter to run
Agda
PLFA+

Syntax

infix  4 _⊢_
infix  4 _∋_
infixl 5 _,_
infixr 7 _⇒_
infixr 9 _`×_
infix  5 ƛ_
infix  5 μ_
infixl 7 _·_
infixl 8 _`*_
infix  8 `suc_
infix  9 `_
infix  9 S_
infix  9 #_
Shift+Enter to run
Agda
PLFA+

Types

data Type : Set where
  `ℕ    : Type
  _⇒_   : Type → Type → Type
  Nat   : Type
  _`×_  : Type → Type → Type
Shift+Enter to run
Agda
PLFA+

Contexts

data Context : Set where
  ∅   : Context
  _,_ : Context → Type → Context
Shift+Enter to run
Agda
PLFA+

Variables and the lookup judgment

data _∋_ : Context → Type → Set where
  Z : ∀ {Γ A}
      ---------
    → Γ , A ∋ A
  S_ : ∀ {Γ A B}
    → Γ ∋ B
      ---------
    → Γ , A ∋ B
Shift+Enter to run
Agda
PLFA+

Terms and the typing judgment

data _⊢_ : Context → Type → Set where
  -- variables
  `_ : ∀ {Γ A}
    → Γ ∋ A
      -----
    → Γ ⊢ A
  -- functions
  ƛ_  :  ∀ {Γ A B}
    → Γ , A ⊢ B
      ---------
    → Γ ⊢ A ⇒ B
  _·_ : ∀ {Γ A B}
    → Γ ⊢ A ⇒ B
    → Γ ⊢ A
      ---------
    → Γ ⊢ B
  -- naturals
  `zero : ∀ {Γ}
      ------
    → Γ ⊢ `ℕ
  `suc_ : ∀ {Γ}
    → Γ ⊢ `ℕ
      ------
    → Γ ⊢ `ℕ
  case : ∀ {Γ A}
    → Γ ⊢ `ℕ
    → Γ ⊢ A
    → Γ , `ℕ ⊢ A
      -----
    → Γ ⊢ A
  -- fixpoint
  μ_ : ∀ {Γ A}
    → Γ , A ⊢ A
      ----------
    → Γ ⊢ A
  -- primitive numbers
  con : ∀ {Γ}
    → ℕ
      -------
    → Γ ⊢ Nat
  _`*_ : ∀ {Γ}
    → Γ ⊢ Nat
    → Γ ⊢ Nat
      -------
    → Γ ⊢ Nat
  -- let
  `let : ∀ {Γ A B}
    → Γ ⊢ A
    → Γ , A ⊢ B
      ----------
    → Γ ⊢ B
  -- products
  `⟨_,_⟩ : ∀ {Γ A B}
    → Γ ⊢ A
    → Γ ⊢ B
      -----------
    → Γ ⊢ A `× B
  `proj₁ : ∀ {Γ A B}
    → Γ ⊢ A `× B
      -----------
    → Γ ⊢ A
  `proj₂ : ∀ {Γ A B}
    → Γ ⊢ A `× B
      -----------
    → Γ ⊢ B
  -- alternative formulation of products
  case× : ∀ {Γ A B C}
    → Γ ⊢ A `× B
    → Γ , A , B ⊢ C
      --------------
    → Γ ⊢ C
Shift+Enter to run
Agda
PLFA+

Abbreviating de Bruijn indices

lookup : Context → ℕ → Type
lookup (Γ , A) zero     =  A
lookup (Γ , _) (suc n)  =  lookup Γ n
lookup ∅       _        =  ⊥-elim impossible
  where postulate impossible : ⊥
count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n
count {Γ , _} zero     =  Z
count {Γ , _} (suc n)  =  S (count n)
count {∅}     _        =  ⊥-elim impossible
  where postulate impossible : ⊥
#_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n
# n  =  ` count n
Shift+Enter to run
Agda
PLFA+

Renaming

ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B)
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)
rename ρ (con n)        =  con n
rename ρ (M `* N)       =  rename ρ M `* rename ρ N
rename ρ (`let M N)     =  `let (rename ρ M) (rename (ext ρ) N)
rename ρ `⟨ M , N ⟩     =  `⟨ rename ρ M , rename ρ N ⟩
rename ρ (`proj₁ L)     =  `proj₁ (rename ρ L)
rename ρ (`proj₂ L)     =  `proj₂ (rename ρ L)
rename ρ (case× L M)    =  case× (rename ρ L) (rename (ext (ext ρ)) M)
Shift+Enter to run
Agda
PLFA+

Simultaneous Substitution

exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ⊢ B)
exts σ Z      =  ` Z
exts σ (S x)  =  rename S_ (σ x)
subst : ∀ {Γ Δ} → (∀ {C} → Γ ∋ C → Δ ⊢ C) → (∀ {C} → Γ ⊢ C → Δ ⊢ C)
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)
subst σ (con n)        =  con n
subst σ (M `* N)       =  subst σ M `* subst σ N
subst σ (`let M N)     =  `let (subst σ M) (subst (exts σ) N)
subst σ `⟨ M , N ⟩     =  `⟨ subst σ M , subst σ N ⟩
subst σ (`proj₁ L)     =  `proj₁ (subst σ L)
subst σ (`proj₂ L)     =  `proj₂ (subst σ L)
subst σ (case× L M)    =  case× (subst σ L) (subst (exts (exts σ)) M)
Shift+Enter to run
Agda
PLFA+

Single and double substitution

_[_] : ∀ {Γ A B}
  → Γ , A ⊢ B
  → Γ ⊢ A
    ---------
  → Γ ⊢ B
_[_] {Γ} {A} N V =  subst {Γ , A} {Γ} σ N
  where
  σ : ∀ {B} → Γ , A ∋ B → Γ ⊢ B
  σ Z      =  V
  σ (S x)  =  ` x
_[_][_] : ∀ {Γ A B C}
  → Γ , A , B ⊢ C
  → Γ ⊢ A
  → Γ ⊢ B
    -------------
  → Γ ⊢ C
_[_][_] {Γ} {A} {B} N V W =  subst {Γ , A , B} {Γ} σ N
  where
  σ : ∀ {C} → Γ , A , B ∋ C → Γ ⊢ C
  σ Z          =  W
  σ (S Z)      =  V
  σ (S (S x))  =  ` x
Shift+Enter to run
Agda
PLFA+

Values

data Value : ∀ {Γ A} → Γ ⊢ A → Set where
  -- functions
  V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
      ---------------------------
    → Value (ƛ N)
  -- naturals
  V-zero : ∀ {Γ}
      -----------------
    → Value (`zero {Γ})
  V-suc_ : ∀ {Γ} {V : Γ ⊢ `ℕ}
    → Value V
      --------------
    → Value (`suc V)
  -- primitives
  V-con : ∀ {Γ n}
      -----------------
    → Value (con {Γ} n)
  -- products
  V-⟨_,_⟩ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
    → Value V
    → Value W
      ----------------
    → Value `⟨ V , W ⟩
Shift+Enter to run
Agda
PLFA+

Implicit arguments need to be supplied when they are not fixed by the given arguments.

Reduction

infix 2 _—→_
data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
  -- functions
  ξ-·₁ : ∀ {Γ 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} {V : Γ ⊢ A}
    → Value V
      --------------------
    → (ƛ N) · V —→ N [ V ]
  -- naturals
  ξ-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 ]
  -- fixpoint
  β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
      ----------------
    → μ N —→ N [ μ N ]
  -- primitive numbers
  ξ-*₁ : ∀ {Γ} {L L′ M : Γ ⊢ Nat}
    → L —→ L′
      -----------------
    → L `* M —→ L′ `* M
  ξ-*₂ : ∀ {Γ} {V M M′ : Γ ⊢ Nat}
    → Value V
    → M —→ M′
      -----------------
    → V `* M —→ V `* M′
  δ-* : ∀ {Γ c d}
      ---------------------------------
    → con {Γ} c `* con d —→ con (c * d)
  -- let
  ξ-let : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ , A ⊢ B}
    → M —→ M′
      ---------------------
    → `let M N —→ `let M′ N
  β-let : ∀ {Γ A B} {V : Γ ⊢ A} {N : Γ , A ⊢ B}
    → Value V
      -------------------
    → `let V N —→ N [ V ]
  -- products
  ξ-⟨,⟩₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ ⊢ B}
    → M —→ M′
      -------------------------
    → `⟨ M , N ⟩ —→ `⟨ M′ , N ⟩
  ξ-⟨,⟩₂ : ∀ {Γ A B} {V : Γ ⊢ A} {N N′ : Γ ⊢ B}
    → Value V
    → N —→ N′
      -------------------------
    → `⟨ V , N ⟩ —→ `⟨ V , N′ ⟩
  ξ-proj₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
    → L —→ L′
      ---------------------
    → `proj₁ L —→ `proj₁ L′
  ξ-proj₂ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
    → L —→ L′
      ---------------------
    → `proj₂ L —→ `proj₂ L′
  β-proj₁ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
    → Value V
    → Value W
      ----------------------
    → `proj₁ `⟨ V , W ⟩ —→ V
  β-proj₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
    → Value V
    → Value W
      ----------------------
    → `proj₂ `⟨ V , W ⟩ —→ W
  -- alternative formulation of products
  ξ-case× : ∀ {Γ A B C} {L L′ : Γ ⊢ A `× B} {M : Γ , A , B ⊢ C}
    → L —→ L′
      -----------------------
    → case× L M —→ case× L′ M
  β-case× : ∀ {Γ A B C} {V : Γ ⊢ A} {W : Γ ⊢ B} {M : Γ , A , B ⊢ C}
    → Value V
    → Value W
      ----------------------------------
    → case× `⟨ V , W ⟩ M —→ M [ V ][ W ]
Shift+Enter to run
Agda
PLFA+

Reflexive and transitive closure

infix  2 _—↠_
infix  1 begin_
infixr 2 _—→⟨_⟩_
infix  3 _∎
data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
  _∎ : ∀ {Γ A} (M : Γ ⊢ A)
      ------
    → M —↠ M
  _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
    → L —→ M
    → M —↠ N
      ------
    → L —↠ N
begin_ : ∀ {Γ A} {M N : Γ ⊢ A}
  → M —↠ N
    ------
  → M —↠ N
begin M—↠N = M—↠N
Shift+Enter to run
Agda
PLFA+

Values do not reduce

V¬—→ : ∀ {Γ A} {M N : Γ ⊢ A}
  → Value M
    ----------
  → ¬ (M —→ N)
V¬—→ V-ƛ          ()
V¬—→ V-zero       ()
V¬—→ (V-suc VM)   (ξ-suc M—→M′)     =  V¬—→ VM M—→M′
V¬—→ V-con        ()
V¬—→ V-⟨ VM , _ ⟩ (ξ-⟨,⟩₁ M—→M′)    =  V¬—→ VM M—→M′
V¬—→ V-⟨ _ , VN ⟩ (ξ-⟨,⟩₂ _ N—→N′)  =  V¬—→ VN N—→N′
Shift+Enter to run
Agda
PLFA+

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 β-μ
progress (con n)                            =  done V-con
progress (L `* M) with progress L
...    | step L—→L′                         =  step (ξ-*₁ L—→L′)
...    | done V-con with progress M
...        | step M—→M′                     =  step (ξ-*₂ V-con M—→M′)
...        | done V-con                     =  step δ-*
progress (`let M N) with progress M
...    | step M—→M′                         =  step (ξ-let M—→M′)
...    | done VM                            =  step (β-let VM)
progress `⟨ M , N ⟩ with progress M
...    | step M—→M′                         =  step (ξ-⟨,⟩₁ M—→M′)
...    | done VM with progress N
...        | step N—→N′                     =  step (ξ-⟨,⟩₂ VM N—→N′)
...        | done VN                        =  done (V-⟨ VM , VN ⟩)
progress (`proj₁ L) with progress L
...    | step L—→L′                         =  step (ξ-proj₁ L—→L′)
...    | done (V-⟨ VM , VN ⟩)               =  step (β-proj₁ VM VN)
progress (`proj₂ L) with progress L
...    | step L—→L′                         =  step (ξ-proj₂ L—→L′)
...    | done (V-⟨ VM , VN ⟩)               =  step (β-proj₂ VM VN)
progress (case× L M) with progress L
...    | step L—→L′                         =  step (ξ-case× L—→L′)
...    | done (V-⟨ VM , VN ⟩)               =  step (β-case× VM VN)
Shift+Enter to run
Agda
PLFA+

Evaluation

data Gas : Set where
  gas : ℕ → Gas
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
Shift+Enter to run
Agda
PLFA+

Examples

cube : ∅ ⊢ Nat ⇒ Nat
cube = ƛ (# 0 `* # 0 `* # 0)
_ : cube · con 2 —↠ con 8
_ =
  begin
    cube · con 2
  —→⟨ β-ƛ V-con ⟩
    con 2 `* con 2 `* con 2
  —→⟨ ξ-*₁ δ-* ⟩
    con 4 `* con 2
  —→⟨ δ-* ⟩
    con 8
  ∎
exp10 : ∅ ⊢ Nat ⇒ Nat
exp10 = ƛ (`let (# 0 `* # 0)
            (`let (# 0 `* # 0)
              (`let (# 0 `* # 2)
                (# 0 `* # 0))))
_ : exp10 · con 2 —↠ con 1024
_ =
  begin
    exp10 · con 2
  —→⟨ β-ƛ V-con ⟩
    `let (con 2 `* con 2) (`let (# 0 `* # 0) (`let (# 0 `* con 2) (# 0 `* # 0)))
  —→⟨ ξ-let δ-* ⟩
    `let (con 4) (`let (# 0 `* # 0) (`let (# 0 `* con 2) (# 0 `* # 0)))
  —→⟨ β-let V-con ⟩
    `let (con 4 `* con 4) (`let (# 0 `* con 2) (# 0 `* # 0))
  —→⟨ ξ-let δ-* ⟩
    `let (con 16) (`let (# 0 `* con 2) (# 0 `* # 0))
  —→⟨ β-let V-con ⟩
    `let (con 16 `* con 2) (# 0 `* # 0)
  —→⟨ ξ-let δ-* ⟩
    `let (con 32) (# 0 `* # 0)
  —→⟨ β-let V-con ⟩
    con 32 `* con 32
  —→⟨ δ-* ⟩
    con 1024
  ∎
swap× : ∀ {A B} → ∅ ⊢ A `× B ⇒ B `× A
swap× = ƛ `⟨ `proj₂ (# 0) , `proj₁ (# 0) ⟩
_ : swap× · `⟨ con 42 , `zero ⟩ —↠ `⟨ `zero , con 42 ⟩
_ =
  begin
    swap× · `⟨ con 42 , `zero ⟩
  —→⟨ β-ƛ V-⟨ V-con , V-zero ⟩ ⟩
    `⟨ `proj₂ `⟨ con 42 , `zero ⟩ , `proj₁ `⟨ con 42 , `zero ⟩ ⟩
  —→⟨ ξ-⟨,⟩₁ (β-proj₂ V-con V-zero) ⟩
    `⟨ `zero , `proj₁ `⟨ con 42 , `zero ⟩ ⟩
  —→⟨ ξ-⟨,⟩₂ V-zero (β-proj₁ V-con V-zero) ⟩
    `⟨ `zero , con 42 ⟩
  ∎
swap×-case : ∀ {A B} → ∅ ⊢ A `× B ⇒ B `× A
swap×-case = ƛ case× (# 0) `⟨ # 0 , # 1 ⟩
_ : swap×-case · `⟨ con 42 , `zero ⟩ —↠ `⟨ `zero , con 42 ⟩
_ =
  begin
     swap×-case · `⟨ con 42 , `zero ⟩
   —→⟨ β-ƛ V-⟨ V-con , V-zero ⟩ ⟩
     case× `⟨ con 42 , `zero ⟩ `⟨ # 0 , # 1 ⟩
   —→⟨ β-case× V-con V-zero ⟩
     `⟨ `zero , con 42 ⟩
   ∎
Shift+Enter to run
Agda
PLFA+
Exercise More (recommended and practice)

Formalise the remaining constructs defined in this chapter. Make your changes in this file. Evaluate each example, applied to data as needed, to confirm it returns the expected answer:

  • sums (recommended)

  • unit type (practice)

  • an alternative formulation of unit type (practice)

  • empty type (recommended)

  • lists (practice)

Please delimit any code you add as follows:

-- begin
-- end
Agda
Exercise double-subst (stretch)

Show that a double substitution is equivalent to two single substitutions.

postulate
  double-subst :
    ∀ {Γ A B C} {V : Γ ⊢ A} {W : Γ ⊢ B} {N : Γ , A , B ⊢ C} →
      N [ V ][ W ] ≡ (N [ rename S_ W ]) [ V ]
Shift+Enter to run
Agda
PLFA+

Note the arguments need to be swapped and W needs to have its context adjusted via renaming in order for the right-hand side to be well typed.

Test examples

We repeat the test examples from Chapter DeBruijn, in order to make sure we have not broken anything in the process of extending our base calculus.

two : ∀ {Γ} → Γ ⊢ `ℕ
two = `suc `suc `zero
plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
2+2 : ∀ {Γ} → Γ ⊢ `ℕ
2+2 = plus · two · two
Ch : Type → Type
Ch A  =  (A ⇒ A) ⇒ A ⇒ A
twoᶜ : ∀ {Γ A} → Γ ⊢ Ch A
twoᶜ = ƛ ƛ (# 1 · (# 1 · # 0))
plusᶜ : ∀ {Γ A} → Γ ⊢ Ch A ⇒ Ch A ⇒ Ch A
plusᶜ = ƛ ƛ ƛ ƛ (# 3 · # 1 · (# 2 · # 1 · # 0))
sucᶜ : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ
sucᶜ = ƛ `suc (# 0)
2+2ᶜ : ∀ {Γ} → Γ ⊢ `ℕ
2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
Shift+Enter to run
Agda
PLFA+

Unicode

This chapter uses the following unicode:

σ  U+03C3  GREEK SMALL LETTER SIGMA (\Gs or \sigma)
†  U+2020  DAGGER (\dag)
‡  U+2021  DOUBLE DAGGER (\ddag)
Agda

Prev • Index • Next

This work is licensed under a Creative Commons Attribution 4.0 International License. Some changes were made to the original version in order to adapt its contents to nextjournal.

Runtimes (1)