B522-PL-Foundations

Course Webpage for B522 Programming Language Foundations, Spring 2020, Indiana University

View the Project on GitHub jsiek/B522-PL-Foundations

module GradualTyping where

Gradually Typed Lambda Calculus

Imports

import Syntax
open import Data.Bool renaming (Bool to 𝔹)
open import Data.List using (List; []; _∷_)
open import Data.Nat using (β„•; zero; suc)
open import Data.Product using (_Γ—_; Ξ£; Ξ£-syntax; βˆƒ; βˆƒ-syntax; proj₁; projβ‚‚)
   renaming (_,_ to ⟨_,_⟩)
open import Relation.Binary.PropositionalEquality
  using (_≑_; _β‰’_; refl; sym; cong; congβ‚‚)
open import Relation.Nullary using (Β¬_)

Primitives

The idea here is to use Agda values as primitive constants. We include natural numbers, Booleans, and Agda functions over naturals and Booleans.

The Base and Prim data types describe the types of constants.

data Base : Set where
  B-Nat : Base
  B-Bool : Base

data Prim : Set where
  base : Base β†’ Prim
  _β‡’_ : Base β†’ Prim β†’ Prim

The base-rep and rep functions map from the type descriptors to the Agda types that we will use to represent the constants.

base-rep : Base β†’ Set 
base-rep B-Nat = β„•
base-rep B-Bool = 𝔹

rep : Prim β†’ Set
rep (base b) = base-rep b
rep (b β‡’ p) = base-rep b β†’ rep p

Types

data BaseTy : Set where
  Nat : BaseTy
  Bool : BaseTy

data Type : Set where
  `_    : BaseTy β†’ Type
  ⋆     : Type
  _β‡’_   : Type β†’ Type β†’ Type
  _`Γ—_  : Type β†’ Type β†’ Type
  _`⊎_  : Type β†’ Type β†’ Type

Consistency and Join

infix  5  _~_
data _~_ : Type β†’ Type β†’ Set where
  unk~L : βˆ€ {A} β†’ ⋆ ~ A
  unk~R : βˆ€ {A} β†’ A ~ ⋆
  base~ : βˆ€{ΞΉ} β†’ ` ΞΉ ~ ` ΞΉ
  fun~ : βˆ€{A B A' B'}
    β†’ A' ~ A  β†’  B ~ B'
      -------------------
    β†’ (A β‡’ B) ~ (A' β‡’ B')
  pair~ : βˆ€{A B A' B'}
    β†’ A ~ A'  β†’  B ~ B'
      -------------------
    β†’ (A `Γ— B) ~ (A' `Γ— B')
  sum~ : βˆ€{A B A' B'}
    β†’ A ~ A'  β†’  B ~ B'
      -------------------
    β†’ (A `⊎ B) ~ (A' `⊎ B')

⨆ : βˆ€{A B : Type} β†’ (c : A ~ B) β†’ Type
⨆ {.⋆} {B} unk~L = B
⨆ {A} {.⋆} unk~R = A
⨆ {(` ΞΉ)} {.(` _)} base~ = ` ΞΉ
⨆ {.(_ β‡’ _)} {.(_ β‡’ _)} (fun~ c d) = (⨆ c) β‡’ (⨆ d)
⨆ {.(_ `Γ— _)} {.(_ `Γ— _)} (pair~ c d) = (⨆ c) `Γ— (⨆ d)
⨆ {.(_ `⊎ _)} {.(_ `⊎ _)} (sum~ c d) = (⨆ c) `⊎ (⨆ d)

Terms

We use the abstract-binding-trees library to represent terms.

data Op : Set where
  op-lam : Type β†’ Op
  op-app : Op
  op-const : (p : Prim) β†’ rep p β†’ Op
  op-pair : Op
  op-fst  : Op
  op-snd : Op
  op-inl : Op
  op-inr : Op
  op-case : Op

sig : Op β†’ List β„•
sig (op-lam A) = 1 ∷ []
sig op-app = 0 ∷ 0 ∷ []
sig (op-const p k) = []
sig op-pair = 0 ∷ 0 ∷ []
sig op-fst = 0 ∷ []
sig op-snd = 0 ∷ []
sig op-inl = 0 ∷ []
sig op-inr = 0 ∷ []
sig op-case = 0 ∷ 1 ∷ 1 ∷ []

open Syntax using (Rename; _β€’_; ↑; id; ext; ⦉_⦊)

open Syntax.OpSig Op sig
  using (`_; _β¦…_⦆; cons; nil; bind; ast)
  renaming (ABT to Term)

infixl 7  _Β·_

pattern $ p k      = (op-const p k) β¦… nil ⦆
pattern Ζ›_Λ™_ A N    = op-lam A       β¦… cons (bind (ast N)) nil ⦆
pattern _Β·_ L M    = op-app         β¦… cons (ast L) (cons (ast M) nil) ⦆
pattern pair L M   = op-pair        β¦… cons (ast L) (cons (ast M) nil) ⦆
pattern fst M      = op-fst         β¦… cons (ast M) nil ⦆
pattern snd M      = op-snd         β¦… cons (ast M) nil ⦆
pattern inl M      = op-inl         β¦… cons (ast M) nil ⦆
pattern inr M      = op-inr         β¦… cons (ast M) nil ⦆
pattern case L M N = op-case        β¦… cons (ast L) (cons (bind (ast M))
                                                   (cons (bind (ast N)) nil)) ⦆

Type of a primitive

typeof-base : Base β†’ Type
typeof-base B-Nat = ` Nat
typeof-base B-Bool = ` Bool

typeof : Prim β†’ Type
typeof (base b) = typeof-base b 
typeof (b β‡’ p) = typeof-base b β‡’ typeof p

Contexts

data Context : Set where
  βˆ…   : Context
  _,_ : Context β†’ Type β†’ Context

infix  4  _βˆ‹_⦂_

data _βˆ‹_⦂_ : Context β†’ β„• β†’ Type β†’ Set where

  Z : βˆ€ {Ξ“ A}
      ------------------
    β†’ Ξ“ , A βˆ‹ 0 ⦂ A

  S : βˆ€ {Ξ“ x A B}
    β†’ Ξ“ βˆ‹ x ⦂ A
      ------------------
    β†’ Ξ“ , B βˆ‹ (suc x) ⦂ A

Type Matching

data _β–Ή_β‡’_ : Type β†’ Type β†’ Type β†’ Set where
  matchβ‡’β‡’ : βˆ€{A B} β†’ (A β‡’ B) β–Ή A β‡’ B
  match⇒⋆ : ⋆ β–Ή ⋆ β‡’ ⋆

data _β–Ή_Γ—_ : Type β†’ Type β†’ Type β†’ Set where
  matchΓ—Γ— : βˆ€{A B} β†’ (A `Γ— B) β–Ή A Γ— B
  match×⋆ : ⋆ β–Ή ⋆ Γ— ⋆

data _β–Ή_⊎_ : Type β†’ Type β†’ Type β†’ Set where
  match⊎⊎ : βˆ€{A B} β†’ (A `⊎ B) β–Ή A ⊎ B
  matchβŠŽβ‹† : ⋆ β–Ή ⋆ ⊎ ⋆

Typing judgement

infix  4  _⊒G_⦂_

data _⊒G_⦂_ : Context β†’ Term β†’ Type β†’ Set where

  -- Axiom 
  ⊒` : βˆ€ {Ξ“ x A}
    β†’ Ξ“ βˆ‹ x ⦂ A
      -----------
    β†’ Ξ“ ⊒G ` x ⦂ A

  -- β‡’-I 
  βŠ’Ζ› : βˆ€ {Ξ“ N A B}
    β†’ Ξ“ , A ⊒G N ⦂ B
      -------------------
    β†’ Ξ“ ⊒G (Ζ› A Λ™ N) ⦂ A β‡’ B

  -- β‡’-E
  ⊒· : βˆ€ {Ξ“ L M A A₁ Aβ‚‚ B}
    β†’ Ξ“ ⊒G L ⦂ A
    β†’ Ξ“ ⊒G M ⦂ B
    β†’ A β–Ή A₁ β‡’ Aβ‚‚
    β†’ A₁ ~ B
      --------------
    β†’ Ξ“ ⊒G L Β· M ⦂ Aβ‚‚

  ⊒$ : βˆ€{Ξ“ p k A}
     β†’ A ≑ typeof p
       -------------
     β†’ Ξ“ ⊒G $ p k ⦂ A

  ⊒pair : βˆ€ {Ξ“ A B}{M N : Term}
    β†’ Ξ“ ⊒G M ⦂ A  β†’  Ξ“ ⊒G N ⦂ B
      -----------------------
    β†’ Ξ“ ⊒G (pair M N) ⦂ A `Γ— B
    
  ⊒fst : βˆ€ {Ξ“ A A₁ Aβ‚‚}{M : Term}
    β†’ Ξ“ ⊒G M ⦂ A
    β†’ A β–Ή A₁ Γ— Aβ‚‚
      -------------------------
    β†’ Ξ“ ⊒G fst M ⦂ A₁

  ⊒snd : βˆ€ {Ξ“ A A₁ Aβ‚‚}{M : Term}
    β†’ Ξ“ ⊒G M ⦂ A
    β†’ A β–Ή A₁ Γ— Aβ‚‚
      -------------------------
    β†’ Ξ“ ⊒G (snd M) ⦂ Aβ‚‚

  ⊒inl : βˆ€ {Ξ“ A}{M : Term}
    β†’ (B : Type)
    β†’ Ξ“ ⊒G M ⦂ A
      -----------------------
    β†’ Ξ“ ⊒G (inl M) ⦂ A `⊎ B

  ⊒inr : βˆ€ {Ξ“ B}{M : Term}
    β†’ (A : Type)
    β†’ Ξ“ ⊒G M ⦂ B
      -----------------------
    β†’ Ξ“ ⊒G (inr M) ⦂ A `⊎ B

  ⊒case : βˆ€{Ξ“ A A₁ Aβ‚‚ B B₁ Bβ‚‚ C C₁ Cβ‚‚}{L M N : Term}
    β†’ Ξ“ ⊒G L ⦂ A
    β†’ Ξ“ ⊒G M ⦂ B
    β†’ Ξ“ ⊒G N ⦂ C
    β†’ {ma : A β–Ή A₁ ⊎ Aβ‚‚ }
    β†’ {mb : B β–Ή B₁ β‡’ Bβ‚‚ }
    β†’ {mc : C β–Ή C₁ β‡’ Cβ‚‚ }
    β†’ {ab : A₁ ~ B₁}
    β†’ {ac : Aβ‚‚ ~ C₁}
    β†’ {bc : Bβ‚‚ ~ Cβ‚‚}
      ----------------------------------
    β†’ Ξ“ ⊒G (case L M N) ⦂ ⨆ bc

Cast Calculus

data cc-Op : Set where
  op-cc-lam : cc-Op
  op-cc-app : cc-Op
  op-cc-const : (p : Prim) β†’ rep p β†’ cc-Op
  op-cc-pair : cc-Op
  op-cc-fst  : cc-Op
  op-cc-snd : cc-Op
  op-cc-inl : cc-Op
  op-cc-inr : cc-Op
  op-cc-case : cc-Op
  op-cc-cast : Type β†’ Type β†’ cc-Op
  op-cc-blame : cc-Op

cc-sig : cc-Op β†’ List β„•
cc-sig op-cc-lam = 1 ∷ []
cc-sig op-cc-app = 0 ∷ 0 ∷ []
cc-sig (op-cc-const p k) = []
cc-sig op-cc-pair = 0 ∷ 0 ∷ []
cc-sig op-cc-fst = 0 ∷ []
cc-sig op-cc-snd = 0 ∷ []
cc-sig op-cc-inl = 0 ∷ []
cc-sig op-cc-inr = 0 ∷ []
cc-sig op-cc-case = 0 ∷ 1 ∷ 1 ∷ []
cc-sig (op-cc-cast A B) = 0 ∷ []
cc-sig op-cc-blame = []

open Syntax using (Rename; _β€’_; ↑; id; ext; ⦉_⦊)

open Syntax.OpSig cc-Op cc-sig
  using (_[_]; Subst; βŸͺ_⟫; ⟦_⟧; exts; rename)
  renaming (`_ to ^_; _β¦…_⦆ to _γ€–_γ€—; ABT to cc-Term;
  cons to cc-cons; nil to cc-nil; bind to cc-bind; ast to cc-ast)

pattern ! p k      = (op-cc-const p k)γ€– cc-nil γ€—
pattern Ζ› N      = op-cc-lam        γ€– cc-cons (cc-bind (cc-ast N)) cc-nil γ€—
pattern app L M    = op-cc-app        γ€– cc-cons (cc-ast L) (cc-cons (cc-ast M) cc-nil) γ€—
pattern cc-pair L M   = op-cc-pair    γ€– cc-cons (cc-ast L) (cc-cons (cc-ast M) cc-nil) γ€—
pattern cc-fst M      = op-cc-fst     γ€– cc-cons (cc-ast M) cc-nil γ€—
pattern cc-snd M      = op-cc-snd     γ€– cc-cons (cc-ast M) cc-nil γ€—
pattern cc-inl M      = op-cc-inl     γ€– cc-cons (cc-ast M) cc-nil γ€—
pattern cc-inr M      = op-cc-inr     γ€– cc-cons (cc-ast M) cc-nil γ€—
pattern cc-case L M N = op-cc-case    γ€– cc-cons (cc-ast L) (cc-cons (cc-bind (cc-ast M))
                                                   (cc-cons (cc-bind (cc-ast N)) cc-nil)) γ€—
pattern _⟨_⇛_⟩ M A B = op-cc-cast A B γ€– cc-cons (cc-ast M) cc-nil γ€—
pattern blame = op-cc-blame  γ€– cc-nil γ€—

infix  4  _⊒_⦂_

data _⊒_⦂_ : Context β†’ cc-Term β†’ Type β†’ Set where

  -- Axiom 
  ⊒^ : βˆ€ {Ξ“ x A}
    β†’ Ξ“ βˆ‹ x ⦂ A
      -----------
    β†’ Ξ“ ⊒ ^ x ⦂ A

  -- β‡’-I 
  βŠ’Ζ› : βˆ€ {Ξ“ A B}{N : cc-Term}
    β†’ Ξ“ , A ⊒ N ⦂ B
      -------------------
    β†’ Ξ“ ⊒ Ζ› N ⦂ A β‡’ B

  -- β‡’-E
  ⊒· : βˆ€ {Ξ“ L M A B}
    β†’ Ξ“ ⊒ L ⦂ A β‡’ B
    β†’ Ξ“ ⊒ M ⦂ A
      --------------
    β†’ Ξ“ ⊒ app L M ⦂ B

  ⊒! : βˆ€{Ξ“ p k A}
     β†’ A ≑ typeof p
       -------------
     β†’ Ξ“ ⊒ ! p k ⦂ A

  ⊒pair : βˆ€ {Ξ“ A B}{M N : cc-Term}
    β†’ Ξ“ ⊒ M ⦂ A  β†’  Ξ“ ⊒ N ⦂ B
      -----------------------
    β†’ Ξ“ ⊒ (cc-pair M N) ⦂ A `Γ— B
    
  ⊒fstΓ— : βˆ€ {Ξ“ A B}{M : cc-Term}
    β†’ Ξ“ ⊒ M ⦂ A `Γ— B
      -------------------------
    β†’ Ξ“ ⊒ cc-fst M ⦂ A

  ⊒sndΓ— : βˆ€ {Ξ“ A B}{M : cc-Term}
    β†’ Ξ“ ⊒ M ⦂ A `Γ— B
      -------------------------
    β†’ Ξ“ ⊒ (cc-snd M) ⦂ B

  ⊒inl : βˆ€ {Ξ“ A}{M : cc-Term}
    β†’ (B : Type)
    β†’ Ξ“ ⊒ M ⦂ A
      -----------------------
    β†’ Ξ“ ⊒ (cc-inl M) ⦂ A `⊎ B

  ⊒inr : βˆ€ {Ξ“ B}{M : cc-Term}
    β†’ (A : Type)
    β†’ Ξ“ ⊒ M ⦂ B
      -----------------------
    β†’ Ξ“ ⊒ (cc-inr M) ⦂ A `⊎ B

  ⊒case : βˆ€{Ξ“ A B C}{L M N : cc-Term}
    β†’ Ξ“ ⊒ L ⦂ A `⊎ B
    β†’ Ξ“ ⊒ M ⦂ A β‡’ C
    β†’ Ξ“ ⊒ N ⦂ B β‡’ C
      ----------------------------------
    β†’ Ξ“ ⊒ (cc-case L M N) ⦂ C

  ⊒cast : βˆ€ {Ξ“ A B}{M : cc-Term}
    β†’ Ξ“ ⊒ M ⦂ A
    β†’ A ~ B
      -----------------------
    β†’ Ξ“ ⊒ M ⟨ A ⇛ B ⟩ ⦂ B

  ⊒blame : βˆ€ {Ξ“ A}
      -------------
    β†’ Ξ“ ⊒ blame ⦂ A

Compile from GTCL to CC

compile : βˆ€{Ξ“ A}{M : Term} β†’ Ξ“ ⊒G M ⦂ A β†’ cc-Term
compile (⊒` {x = x} x∈) = ^ x
compile (βŠ’Ζ› {N = N} ⊒N) = Ζ› (compile ⊒N)
compile (⊒· {L = L}{M}{A}{A₁}{Aβ‚‚}{B} ⊒L ⊒M m cn) =
   let L' = (compile ⊒L) ⟨ A ⇛ (A₁ β‡’ Aβ‚‚) ⟩ in
   let M' = (compile ⊒M) ⟨ B ⇛ A₁ ⟩ in
   app L' M'
compile (⊒$ {p = p}{k} eq) = ! p k
compile (⊒pair ⊒L ⊒M) =
   let L' = compile ⊒L in
   let M' = compile ⊒M in
   cc-pair L' M'
compile (⊒fst {A = A}{A₁}{Aβ‚‚} ⊒M m) =
   let M' = (compile ⊒M) ⟨ A ⇛ (A₁ `Γ— Aβ‚‚) ⟩ in
   cc-fst M'
compile (⊒snd {A = A}{A₁}{Aβ‚‚} ⊒M m) =
   let M' = (compile ⊒M) ⟨ A ⇛ (A₁ `Γ— Aβ‚‚) ⟩ in
   cc-snd M'
compile (⊒inl B ⊒M) = cc-inl (compile ⊒M)
compile (⊒inr B ⊒M) = cc-inr (compile ⊒M)
compile (⊒case {Ξ“}{A}{A₁}{Aβ‚‚}{B}{B₁}{Bβ‚‚}{C}{C₁}{Cβ‚‚} ⊒L ⊒M ⊒N 
          {ma}{mb}{mc}{ab}{ac}{bc}) =
      let L' = (compile ⊒L) ⟨ A ⇛ (A₁ `⊎ Aβ‚‚) ⟩
                ⟨ (A₁ `⊎ Aβ‚‚) ⇛ (B₁ `⊎ C₁) ⟩ in
      let M' = (compile ⊒M) ⟨ B ⇛ (B₁ β‡’ Bβ‚‚) ⟩
                ⟨ (B₁ β‡’ Bβ‚‚) ⇛ (B₁ β‡’ ⨆ bc) ⟩ in
      let N' = (compile ⊒N) ⟨ C ⇛ (C₁ β‡’ Cβ‚‚) ⟩
                ⟨ (C₁ β‡’ Cβ‚‚) ⇛ (C₁ β‡’ ⨆ bc) ⟩ in
      cc-case L' M' N'

Cast Calculus Reduction

data Value : cc-Term β†’ Set where

  V-Ζ› : {N : cc-Term}
      -----------
    β†’ Value (Ζ› N)

  V-const : βˆ€ {p k}
      -------------
    β†’ Value (! p k)

  V-pair : βˆ€ {V W : cc-Term}
    β†’ Value V β†’ Value W
      -----------------
    β†’ Value (cc-pair V W)

  V-inl : βˆ€ {V : cc-Term}
    β†’ Value V
      --------------------------
    β†’ Value (cc-inl V)

  V-inr : βˆ€ {V : cc-Term}
    β†’ Value V
      --------------------------
    β†’ Value (cc-inr V)

  V-cast : βˆ€ {A : Type}{V : cc-Term}
    β†’ Value V
      ---------------
    β†’ Value (V ⟨ A ⇛ ⋆ ⟩)

data Frame : Set where

  F-·₁ : 
      cc-Term
    β†’ Frame

  F-Β·β‚‚ : 
      (M : cc-Term) β†’ Value M
    β†’ Frame

  F-×₁ : 
      cc-Term
    β†’ Frame

  F-Γ—β‚‚ :
      cc-Term
    β†’ Frame

  F-fst : Frame

  F-snd : Frame

  F-inl : Frame

  F-inr : Frame

  F-case : 
      cc-Term
    β†’ cc-Term
    β†’ Frame

  F-cast :
      Type β†’ Type
    β†’ Frame

plug : cc-Term β†’ Frame β†’ cc-Term
plug L (F-·₁ M)      = app L M
plug M (F-Β·β‚‚ L v)      = app L M
plug L (F-×₁ M)      = cc-pair M L
plug M (F-Γ—β‚‚ L)      = cc-pair M L
plug M (F-fst)      = cc-fst M
plug M (F-snd)      = cc-snd M
plug M (F-inl)      = cc-inl M
plug M (F-inr)      = cc-inr M
plug L (F-case M N) = cc-case L M N
plug M (F-cast A B) = M ⟨ A ⇛ B ⟩

infix 2 _β€”β†’_
data _β€”β†’_ : cc-Term β†’ cc-Term β†’ Set where

  ΞΎ : βˆ€ {M Mβ€² : cc-Term} {F : Frame}
    β†’ M β€”β†’ Mβ€²
      ---------------------
    β†’ plug M F β€”β†’ plug Mβ€² F

  ΞΎ-blame : {F : Frame}
      ---------------------
    β†’ plug blame F β€”β†’ blame

  Ξ² : βˆ€ {N W : cc-Term}
    β†’ Value W
      ----------------------
    β†’ app (Ζ› N) W β€”β†’ N [ W ]

  Ξ΄ : βˆ€ {p}{b} {f : base-rep b β†’ rep p} {k : base-rep b}
      -------------------------------------------------------
    β†’ app (! (b β‡’ p) f) (! (base b) k) β€”β†’ ! p (f k)

  Ξ²-fst :  βˆ€ {V W : cc-Term}
    β†’ Value V β†’ Value W
      --------------------
    β†’ cc-fst (cc-pair V W) β€”β†’ V

  Ξ²-snd :  βˆ€ {V : cc-Term} {W : cc-Term}
    β†’ Value V β†’ Value W
      --------------------
    β†’ cc-snd (cc-pair V W) β€”β†’ W

  Ξ²-caseL : βˆ€ {V L M : cc-Term}
    β†’ Value V
      ---------------------------------
    β†’ cc-case (cc-inl V) L M β€”β†’ app L V

  Ξ²-caseR : βˆ€ {V L M : cc-Term}
    β†’ Value V
      ---------------------------------
    β†’ cc-case (cc-inr V) L M β€”β†’ app M V

  castβ‡’ : βˆ€ {V : cc-Term} {A B C D : Type}
    β†’ (v : Value V)
      ----------------------------------------------------------------
    β†’ V ⟨ (A β‡’ B) ⇛ (C β‡’ D) ⟩ β€”β†’ Ζ› (app V ((^ 0) ⟨ C ⇛ A ⟩)) ⟨ B ⇛ D ⟩

  cast⋆ : βˆ€ {V : cc-Term} {A B : Type}
    β†’ (v : Value V) β†’ A ~ B
      ------------------------------------
    β†’ V ⟨ A ⇛ ⋆ ⟩ ⟨ ⋆ ⇛ B ⟩ β€”β†’ V ⟨ A ⇛ B ⟩

  cast-fail : βˆ€ {V : cc-Term} {A B : Type}
    β†’ (v : Value V) β†’ Β¬ (A ~ B)
      ------------------------------
    β†’ V ⟨ A ⇛ ⋆ ⟩ ⟨ ⋆ ⇛ B ⟩ β€”β†’ blame

  castΓ— : βˆ€ {V : cc-Term} {A B C D : Type}
    β†’ (v : Value V)
      -----------------------------------------------------------
    β†’ V ⟨ (A `Γ— B) ⇛ (C `Γ— D) ⟩ β€”β†’ cc-pair ((cc-fst V) ⟨ A ⇛ C ⟩)
                                           ((cc-snd V) ⟨ B ⇛ D ⟩)

  cast-inl : βˆ€ {V : cc-Term} {A B C D : Type}
    β†’ (v : Value V)
      --------------------------------------------------------
    β†’ cc-inl V ⟨ (A `⊎ B) ⇛ (C `⊎ D) ⟩ β€”β†’ cc-inl (V ⟨ A ⇛ C ⟩)

  cast-inr : βˆ€ {V : cc-Term} {A B C D : Type}
    β†’ (v : Value V)
      --------------------------------------------------------
    β†’ cc-inr V ⟨ (A `⊎ B) ⇛ (C `⊎ D) ⟩ β€”β†’ cc-inr (V ⟨ B ⇛ D ⟩)

infix  2 _β€”β† _
infixr 2 _β€”β†’βŸ¨_⟩_
infix  3 _∎

data _β€”β† _ : cc-Term β†’ cc-Term β†’ Set where
  _∎ : βˆ€ (M : cc-Term)
      ---------
    β†’ M β€”β†  M

  _β€”β†’βŸ¨_⟩_ : βˆ€ (L : cc-Term) {M N : cc-Term}
    β†’ L β€”β†’ M
    β†’ M β€”β†  N
      ---------
    β†’ L β€”β†  N