CSCI B629 Mechanized Proofs for PL Metatheory

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

Gradual Types

data Type : Set where
  β„•    : Type
  β˜…   : Type
  _β‡’_ : Type β†’ Type β†’ Type

-- | Type equality is decidable
_β‰Ÿβ‚œ_ : (A B : Type) β†’ Dec (A ≑ B)
β„• β‰Ÿβ‚œ β„• = yes refl
β„• β‰Ÿβ‚œ β˜… = no (Ξ» ())
β„• β‰Ÿβ‚œ (B β‡’ C) = no (Ξ» ())
β˜… β‰Ÿβ‚œ β„• = no (Ξ» ())
β˜… β‰Ÿβ‚œ β˜… = yes refl
β˜… β‰Ÿβ‚œ (B β‡’ C) = no (Ξ» ())
(A β‡’ B) β‰Ÿβ‚œ β„• = no (Ξ» ())
(A β‡’ B) β‰Ÿβ‚œ β˜… = no (Ξ» ())
(A β‡’ B) β‰Ÿβ‚œ (C β‡’ D) with A β‰Ÿβ‚œ C | B β‰Ÿβ‚œ D
... | yes refl | yes refl = yes refl
... | no A≒C | _ = no (λ { refl → A≒C refl })
... | _ | no B≒D = no (λ { refl → B≒D refl })

Type Consistency

{- On paper we would just write

 ---------   ------------  ------------
   β„• ~ β„•       β˜… ~ A        A ~ β˜…

          A ~ C   B ~ D
      ---------------------
       (A β‡’ B) ~ (C β‡’ D)

This is a more elaborated version that makes it easier
  to write the "coerce" function.
-}
infix 4 _~_

data _~_ : Type β†’ Type β†’ Set where

  ~-β„•  : β„• ~ β„•

  ~-β˜… : β˜… ~ β˜…

  β˜…~β„• : β˜… ~ β„•

  β„•~β˜… : β„• ~ β˜…

  β˜…~β‡’ : βˆ€{A B}
    β†’ A ~ β˜…
    β†’ β˜… ~ B
    β†’ β˜… ~ (A β‡’ B)

  β‡’~β˜… : βˆ€{A B}
    β†’ β˜… ~ A
    β†’ B ~ β˜…
    β†’ (A β‡’ B) ~ β˜…

  ~-β‡’  : βˆ€ {A B C D}
    β†’ C ~ A
    β†’ B ~ D
    β†’ (A β‡’ B) ~ (C β‡’ D)

~-refl : βˆ€ {A} β†’ A ~ A
~-refl {A = β„•}      = ~-β„•
~-refl {A = β˜…}     = ~-β˜…
~-refl {A = A β‡’ B} = ~-β‡’ ~-refl ~-refl

~-sym : βˆ€ {A B} β†’ A ~ B β†’ B ~ A
~-sym ~-β„• = ~-β„•
~-sym ~-β˜… = ~-β˜…
~-sym β˜…~β„• = β„•~β˜…
~-sym β„•~β˜… = β˜…~β„•
~-sym (β˜…~β‡’ A~β˜… β˜…~B) = β‡’~β˜… (~-sym A~β˜…) (~-sym β˜…~B)
~-sym (β‡’~β˜… β˜…~A B~β˜…) = β˜…~β‡’ (~-sym β˜…~A) (~-sym B~β˜…)
~-sym (~-β‡’ C~A B~D) = ~-β‡’ (~-sym C~A) (~-sym B~D)

-- | β˜… is consistent with any type
β˜…~ : βˆ€ A β†’ β˜… ~ A
~β˜… : βˆ€ A β†’ A ~ β˜…

β˜…~ β„• = β˜…~β„•
β˜…~ β˜… = ~-β˜…
β˜…~ (A β‡’ B) = β˜…~β‡’ (~β˜… A) (β˜…~ B)
~β˜… β„• = β„•~β˜…
~β˜… β˜… = ~-β˜…
~β˜… (A β‡’ B) = β‡’~β˜… (β˜…~ A) (~β˜… B)

Typing Contexts

Var = Nat
Ctx = List Type

data _βˆ‹_⦂_ : Ctx β†’ Var β†’ Type β†’ Set where

  Z : βˆ€ {Ξ“ A}
      ---------------------
    β†’ (A ∷ Ξ“) βˆ‹ zero ⦂ A

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

Gradually Typed Lambda Calculus (GTLC)

Syntax

data Term : Set where
  `_    : Var β†’ Term
  $_    : Nat β†’ Term
  Ζ›_Λ™_  : Type β†’ Term β†’ Term
  _Β·_οΌ _   : Term β†’ Term β†’ Nat β†’ Term

Typing Rules


infix 4 _⊒_⦂_

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

  ⊒$ : βˆ€ {Ξ“ n}
      --------------- (T-Const)
    β†’ Ξ“ ⊒ $ n ⦂ β„•

  ⊒` : βˆ€ {Ξ“ x A}
    β†’ Ξ“ βˆ‹ x ⦂ A
      --------------- (T-Var)
    β†’ Ξ“ ⊒ ` x ⦂ A

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

  ⊒· : βˆ€ {Ξ“ L M A Aβ€² B β„“}
    β†’ Ξ“ ⊒ L ⦂ A β‡’ B
    β†’ Ξ“ ⊒ M ⦂ Aβ€²
    β†’ Aβ€² ~ A
      ------------------------------ (T-App)
    β†’ Ξ“ ⊒ (L Β· M οΌ  β„“) ⦂ B

  βŠ’Β·β˜… : βˆ€ {Ξ“ L M A β„“}
    β†’ Ξ“ ⊒ L ⦂ β˜…
    β†’ Ξ“ ⊒ M ⦂ A
      ------------------------------ (T-App⋆)
    β†’ Ξ“ ⊒ (L Β· M οΌ  β„“) ⦂ β˜…

We can prove uniqueness of typing for GTLC.

typing-unique : βˆ€ {Ξ“ M A B}
  β†’ Ξ“ ⊒ M ⦂ A
  β†’ Ξ“ ⊒ M ⦂ B
    ---------------
  β†’ A ≑ B
typing-unique (⊒` βˆ‹x) (⊒` βˆ‹xβ€²) = βˆ‹-unique βˆ‹x βˆ‹xβ€²
  where
  βˆ‹-unique : βˆ€ {Ξ“ x A B} β†’ Ξ“ βˆ‹ x ⦂ A β†’ Ξ“ βˆ‹ x ⦂ B β†’ A ≑ B
  βˆ‹-unique Z Z = refl
  βˆ‹-unique (S βˆ‹x) (S βˆ‹xβ€²) = βˆ‹-unique βˆ‹x βˆ‹xβ€²
typing-unique ⊒$ ⊒$ = refl
typing-unique (βŠ’Ζ› ⊒N) (βŠ’Ζ› ⊒Nβ€²) with typing-unique ⊒N ⊒Nβ€²
... | refl = refl
typing-unique (⊒· ⊒L ⊒M Aβ€²~A) (⊒· ⊒Lβ€² ⊒Mβ€² Cβ€²~C)
    with typing-unique ⊒L ⊒Lβ€²
... | refl = refl
typing-unique (⊒· ⊒L ⊒M Aβ€²~A) (βŠ’Β·β˜… ⊒Lβ€² ⊒Mβ€²)
    with typing-unique ⊒L ⊒Lβ€²
... | ()
typing-unique (βŠ’Β·β˜… ⊒L ⊒M) (⊒· ⊒Lβ€² ⊒Mβ€² Aβ€²~A)
    with typing-unique ⊒L ⊒Lβ€²
... | ()
typing-unique (βŠ’Β·β˜… ⊒L ⊒M) (βŠ’Β·β˜… ⊒Lβ€² ⊒Mβ€²) = refl

Coercions

Coercions are combinators that specify the conversion between two types, so ⊒ c : A β‡’ B.

Syntax of Coercions

infixr 7 _⨟_
infixr 6 _β‡’_

data Coercion : Set where

  id  : Type β†’ Coercion

  -- "injection" (tagging)
  _!   : Type β†’ Coercion

  -- "projection" (tag checking)
  _`?_  : Type β†’ Nat β†’ Coercion

  _β‡’_  : Coercion β†’ Coercion β†’ Coercion

  _⨟_  : Coercion β†’ Coercion β†’ Coercion

Typing Rules for Coercions

-- | We restrict the source of an injection or the target
-- | of a projection to ground types
data Ground : Type β†’ Set where
  G-β„•  : Ground β„•
  G-β‡’ : Ground (β˜… β‡’ β˜…)

infix 4 ⊒_⦂_β‡’_

data ⊒_⦂_β‡’_ : Coercion β†’ Type β†’ Type β†’ Set where

  ⊒id : βˆ€ {A}
      --------------------- (T-Id)
    β†’ ⊒ id A ⦂ A β‡’ A

  ⊒! : βˆ€ {G}
    β†’ Ground G
      --------------------- (T-Inj)
    β†’ ⊒ G ! ⦂ G β‡’ β˜…

  ⊒? : βˆ€ {G β„“}
    β†’ Ground G
      --------------------------------- (T-Proj)
    β†’ ⊒ G `? β„“ ⦂ β˜… β‡’ G

  βŠ’β‡’ : βˆ€ {A B C D c d}
    β†’ ⊒ c ⦂ C β‡’ A
    β†’ ⊒ d ⦂ B β‡’ D
     ------------------------------------ (T-Fun)
    β†’ ⊒ c β‡’ d ⦂ (A β‡’ B) β‡’ (C β‡’ D)

  ⊒⨟ : βˆ€ {A B C c d}
    β†’ ⊒ c ⦂ A β‡’ B
    β†’ ⊒ d ⦂ B β‡’ C
      --------------------- (T-Seq)
    β†’ ⊒ c ⨟ d ⦂ A β‡’ C

The Cast Calculus (CC)

Syntax of CC

data Termᢜ : Set where
  `_       : Var β†’ Termᢜ
  $_       : Nat β†’ Termᢜ
  Ζ›_Λ™_     : Type β†’ Termᢜ β†’ Termᢜ
  _Β·_      : Termᢜ β†’ Termᢜ β†’ Termᢜ
  _⟨_⟩     : Termᢜ β†’ Coercion β†’ Termᢜ
  blame    : (β„“ : Nat) β†’ Termᢜ

Typing Rules for CC

infix 4 _⊒ᢜ_⦂_

data _⊒ᢜ_⦂_ : Ctx β†’ Termᢜ β†’ Type β†’ Set where

  ⊒$ : βˆ€ {Ξ“ n}
      --------------- (T-CC-Const)
    β†’ Ξ“ ⊒ᢜ $ n ⦂ β„•

  ⊒` : βˆ€ {Ξ“ x A}
    β†’ Ξ“ βˆ‹ x ⦂ A
      --------------- (T-CC-Var)
    β†’ Ξ“ ⊒ᢜ ` x ⦂ A

  βŠ’Ζ› : βˆ€ {Ξ“ A N B}
    β†’ (A ∷ Ξ“) ⊒ᢜ N ⦂ B
       --------------------------- (T-CC-Abs)
    β†’ Ξ“ ⊒ᢜ Ζ› A Λ™ N ⦂ (A β‡’ B)

  ⊒· : βˆ€ {Ξ“ L M A B}
    β†’ Ξ“ ⊒ᢜ L ⦂ (A β‡’ B)
    β†’ Ξ“ ⊒ᢜ M ⦂ A
      --------------------- (T-CC-App)
    β†’ Ξ“ ⊒ᢜ L Β· M ⦂ B

  ⊒cast : βˆ€ {Ξ“ M c A B}
    β†’ Ξ“ ⊒ᢜ M ⦂ A
    β†’ ⊒ c ⦂ A β‡’ B
      --------------------------- (T-Cast)
    β†’ Ξ“ ⊒ᢜ M ⟨ c ⟩ ⦂ B

  ⊒blame : βˆ€ {Ξ“ A β„“}
      --------------------------- (T-Blame)
    β†’ Ξ“ ⊒ᢜ blame β„“ ⦂ A

Reduction Semantics for CC

Definitions of values and evaluation contexts

data Value : Termᢜ β†’ Set where
  V-$      : βˆ€ {n}     β†’ Value ($ n)
  V-Ζ›      : βˆ€ {A N}   β†’ Value (Ζ› A Λ™ N)
  V-cast!  : βˆ€ {V G}   β†’ Value V β†’ Value (V ⟨ G ! ⟩)
  V-castβ‡’ : βˆ€ {V c d} β†’ Value V β†’ Value (V ⟨ c β‡’ d ⟩)

data Frame : Set where
  β–‘Β·_     : Termᢜ β†’ Frame
  _Β·β–‘_    : (V : Termᢜ) β†’ Value V β†’ Frame
  β–‘βŸ¨_⟩    : Coercion β†’ Frame

plug : Frame β†’ Termᢜ β†’ Termᢜ
plug (β–‘Β· M) L = L Β· M
plug (V Β·β–‘ v) M = V Β· M
plug (β–‘βŸ¨ c ⟩) M = M ⟨ c ⟩

Renaming, parallel and single substitutions

Rename : Set
Rename = Var β†’ Var

Subst : Set
Subst = Var β†’ Termᢜ

ext : Rename β†’ Rename
ext ρ zero = zero
ext ρ (suc x) = suc (ρ x)

rename : Rename β†’ Termᢜ β†’ Termᢜ
rename ρ (` x) = ` (ρ x)
rename ρ ($ n) = $ n
rename ρ (Ζ› A Λ™ N) = Ζ› A Λ™ rename (ext ρ) N
rename ρ (L · M) = rename ρ L · rename ρ M
rename ρ (M ⟨ c ⟩) = rename ρ M ⟨ c ⟩
rename ρ (blame β„“) = blame β„“

exts : Subst β†’ Subst
exts Οƒ zero = ` zero
exts Οƒ (suc x) = rename suc (Οƒ x)

subst : Subst β†’ Termᢜ β†’ Termᢜ
subst Οƒ (` x) = Οƒ x
subst Οƒ ($ n) = $ n
subst Οƒ (Ζ› A Λ™ N) = Ζ› A Λ™ subst (exts Οƒ) N
subst Οƒ (L Β· M) = subst Οƒ L Β· subst Οƒ M
subst Οƒ (M ⟨ c ⟩) = subst Οƒ M ⟨ c ⟩
subst Οƒ (blame β„“) = blame β„“

Οƒβ‚€ : Termᢜ β†’ Subst
Οƒβ‚€ M zero = M
Οƒβ‚€ M (suc x) = ` x

_[_] : Termᢜ β†’ Termᢜ β†’ Termᢜ
N [ M ] = subst (Οƒβ‚€ M) N

Reduction rules

infix 4 _β€”β†’_

data _β€”β†’_ : Termᢜ β†’ Termᢜ β†’ Set where
  ΞΎΞΎ : βˆ€ {F M N Mβ€² Nβ€²}
    β†’ Mβ€² ≑ plug F M
    β†’ Nβ€² ≑ plug F N
    β†’ M β€”β†’ N
      ---------------
    β†’ Mβ€² β€”β†’ Nβ€²

  -- blame propagation
  ΞΎΞΎ-blame : βˆ€ {F Mβ€² β„“}
    β†’ Mβ€² ≑ plug F (blame β„“)
      ------------------------------
    β†’ Mβ€² β€”β†’ blame β„“

  Ξ²-Ζ› : βˆ€ {A N V}
    β†’ Value V
      ---------------------------------
    β†’ (Ζ› A Λ™ N) Β· V β€”β†’ N [ V ]

  -- rules for casts
  Ξ²-id : βˆ€ {A V}
    β†’ Value V
      ---------------------------
    β†’ V ⟨ id A ⟩ β€”β†’ V

  Ξ²-seq : βˆ€ {V c d}
    β†’ Value V
      ------------------------------------------------------
    β†’ V ⟨ c ⨟ d ⟩ β€”β†’ V ⟨ c ⟩ ⟨ d ⟩

  Ξ²-β‡’ : βˆ€ {V W c d}
    β†’ Value V
    β†’ Value W
      ------------------------------------------------------------
    β†’ (V ⟨ c β‡’ d ⟩) Β· W β€”β†’ (V Β· (W ⟨ c ⟩)) ⟨ d ⟩

  Ξ²-proj-inj-ok : βˆ€ {V G β„“}
    β†’ Value V
      ------------------------------------------------------
    β†’ V ⟨ G ! ⟩ ⟨ G `? β„“ ⟩ β€”β†’ V

  Ξ²-proj-inj-bad : βˆ€ {V G H β„“}
    β†’ Value V
    β†’ G β‰’ H
      ------------------------------------------------------------------
    β†’ V ⟨ G ! ⟩ ⟨ H `? β„“ ⟩ β€”β†’ blame β„“


pattern ξ F M→N  = ξξ {F = F} refl refl M→N
pattern ΞΎ-blame F = ΞΎΞΎ-blame {F = F} refl

Type Safety of CC

Value canonical form lemmas

canonical-β˜…-inj : βˆ€ {V}
  β†’ Value V
  β†’ [] ⊒ᢜ V ⦂ β˜…
    ---------------------------------------------
  β†’ βˆƒ[ G ] βˆƒ[ W ] Value W Γ— (V ≑ W ⟨ G ! ⟩)
canonical-β˜…-inj (V-cast! {V = W} {G = G} w) (⊒cast _ (⊒! _)) =
  ⟨ G , ⟨ W , ⟨ w , refl ⟩ ⟩ ⟩

canonical-β‡’ : βˆ€ {V A B}
  β†’ Value V
  β†’ [] ⊒ᢜ V ⦂ (A β‡’ B)
    ------------------------------------------------------
  β†’ βˆƒ[ N ] V ≑ Ζ› A Λ™ N                                ⊎
     βˆƒ[ W ] βˆƒ[ c ] βˆƒ[ d ] Value W Γ— V ≑ W ⟨ c β‡’ d ⟩
canonical-β‡’ (V-Ζ› {N = N}) (βŠ’Ζ› ⊒N) = inj₁ ⟨ N , refl ⟩
canonical-β‡’ (V-castβ‡’ {V = W} {c = c} {d = d} w) (⊒cast _ (βŠ’β‡’ _ _)) =
  injβ‚‚ ⟨ W , ⟨ c , ⟨ d , ⟨ w , refl ⟩ ⟩ ⟩ ⟩

Progress

data Progress (M : Termᢜ) : Set where
  done  : Value M β†’ Progress M
  step  : βˆ€ {N} β†’ M β€”β†’ N β†’ Progress M
  crash : βˆ€ {β„“} β†’ M ≑ blame β„“ β†’ Progress M  -- trapped errors

progress : βˆ€ {M A} β†’ [] ⊒ᢜ M ⦂ A β†’ Progress M
progress (⊒` ())
progress ⊒$ = done V-$
progress (βŠ’Ζ› ⊒M) = done V-Ζ›
progress (⊒· {L = L} {M = M} ⊒L ⊒M) =
  case progress ⊒L of λ where
  (step L→L′)  → step (ξ (░· M) L→L′)
  (crash refl) β†’ step (ΞΎ-blame (β–‘Β· M))
  (done vL) β†’
    case progress ⊒M of λ where
    (step M→M′)  → step (ξ (L ·░ vL) M→M′)
    (crash refl) β†’ step (ΞΎ-blame (L Β·β–‘ vL))
    (done vM) β†’
      case canonical-β‡’ vL ⊒L of Ξ» where
      (inj₁ ⟨ N , refl ⟩) β†’ step (Ξ²-Ζ› vM)
      (injβ‚‚ ⟨ W , ⟨ c , ⟨ d , ⟨ vW , refl ⟩ ⟩ ⟩ ⟩) β†’ step (Ξ²-β‡’ vW vM)
progress (⊒cast {c = c} ⊒M ⊒c) =
  case progress ⊒M of λ where
  (step Mβ†’Mβ€²)  β†’ step (ΞΎ (β–‘βŸ¨ c ⟩) Mβ†’Mβ€²)
  (crash refl) β†’ step (ΞΎ-blame (β–‘βŸ¨ c ⟩))
  (done vM) β†’
    case ⊒c of λ where
    ⊒id      β†’ step (Ξ²-id vM)
    (⊒! g)   β†’ done (V-cast! vM)
    (βŠ’β‡’ _ _) β†’ done (V-castβ‡’ vM)
    (⊒⨟ _ _) β†’ step (Ξ²-seq vM)
    (⊒? {G = G} {β„“ = β„“} g) β†’
      case canonical-β˜…-inj vM ⊒M of Ξ» where
      ⟨ H , ⟨ W , ⟨ vW , refl ⟩ ⟩ ⟩ β†’
        case H β‰Ÿβ‚œ G of Ξ» where
        (yes refl) β†’ step (Ξ²-proj-inj-ok vW)
        (no H≒G)   → step (β-proj-inj-bad {ℓ = ℓ} vW H≒G)
progress ⊒blame = crash refl

Preservation

_⦂_β‡’Κ³_ : Rename β†’ Ctx β†’ Ctx β†’ Set
ρ ⦂ Ξ“ β‡’Κ³ Ξ“β€² = βˆ€ {x A} β†’ Ξ“ βˆ‹ x ⦂ A β†’ Ξ“β€² βˆ‹ ρ x ⦂ A

_⦂_β‡’Λ’_ : Subst β†’ Ctx β†’ Ctx β†’ Set
Οƒ ⦂ Ξ“ β‡’Λ’ Ξ“β€² = βˆ€ {x A} β†’ Ξ“ βˆ‹ x ⦂ A β†’ Ξ“β€² ⊒ᢜ Οƒ x ⦂ A

⊒ext : βˆ€ {Ξ“ Ξ“β€² A ρ}
  β†’ ρ ⦂ Ξ“ β‡’Κ³ Ξ“β€²
  β†’ ext ρ ⦂ (A ∷ Ξ“) β‡’Κ³ (A ∷ Ξ“β€²)
⊒ext ⊒ρ Z = Z
⊒ext ⊒ρ (S βˆ‹x) = S (⊒ρ βˆ‹x)

rename-preserve
  : βˆ€ {Ξ“ Ξ“β€² M A ρ}
  β†’ ρ ⦂ Ξ“ β‡’Κ³ Ξ“β€²
  β†’ Ξ“ ⊒ᢜ M ⦂ A
  β†’ Ξ“β€² ⊒ᢜ rename ρ M ⦂ A
rename-preserve ⊒ρ (⊒` βˆ‹x) = ⊒` (⊒ρ βˆ‹x)
rename-preserve ⊒ρ ⊒$ = ⊒$
rename-preserve ⊒ρ (βŠ’Ζ› ⊒N) = βŠ’Ζ› (rename-preserve (⊒ext ⊒ρ) ⊒N)
rename-preserve ⊒ρ (⊒· ⊒L ⊒M) = ⊒· (rename-preserve ⊒ρ ⊒L) (rename-preserve ⊒ρ ⊒M)
rename-preserve ⊒ρ (⊒cast ⊒M ⊒c) = ⊒cast (rename-preserve ⊒ρ ⊒M) ⊒c
rename-preserve ⊒ρ ⊒blame = ⊒blame

⊒exts : βˆ€ {Ξ“ Ξ“β€² A Οƒ}
  β†’ Οƒ ⦂ Ξ“ β‡’Λ’ Ξ“β€²
  β†’ exts Οƒ ⦂ (A ∷ Ξ“) β‡’Λ’ (A ∷ Ξ“β€²)
⊒exts βŠ’Οƒ Z = ⊒` Z
⊒exts βŠ’Οƒ (S βˆ‹x) = rename-preserve S (βŠ’Οƒ βˆ‹x)

subst-preserve
  : βˆ€ {Ξ“ Ξ“β€² M A Οƒ}
  β†’ Οƒ ⦂ Ξ“ β‡’Λ’ Ξ“β€²
  β†’ Ξ“ ⊒ᢜ M ⦂ A
  β†’ Ξ“β€² ⊒ᢜ subst Οƒ M ⦂ A
subst-preserve βŠ’Οƒ (⊒` βˆ‹x) = βŠ’Οƒ βˆ‹x
subst-preserve βŠ’Οƒ ⊒$ = ⊒$
subst-preserve βŠ’Οƒ (βŠ’Ζ› ⊒N) = βŠ’Ζ› (subst-preserve (⊒exts βŠ’Οƒ) ⊒N)
subst-preserve βŠ’Οƒ (⊒· ⊒L ⊒M) = ⊒· (subst-preserve βŠ’Οƒ ⊒L) (subst-preserve βŠ’Οƒ ⊒M)
subst-preserve βŠ’Οƒ (⊒cast ⊒M ⊒c) = ⊒cast (subst-preserve βŠ’Οƒ ⊒M) ⊒c
subst-preserve βŠ’Οƒ ⊒blame = ⊒blame

sub-preserve
  : βˆ€ {A B N M}
  β†’ (A ∷ []) ⊒ᢜ N ⦂ B
  β†’ [] ⊒ᢜ M ⦂ A
  β†’ [] ⊒ᢜ N [ M ] ⦂ B
sub-preserve ⊒N ⊒M = subst-preserve (βŠ’Οƒβ‚€ ⊒M) ⊒N
  where
  βŠ’Οƒβ‚€ : βˆ€ {A M} β†’ [] ⊒ᢜ M ⦂ A β†’ Οƒβ‚€ M ⦂ (A ∷ []) β‡’Λ’ []
  βŠ’Οƒβ‚€ ⊒M Z = ⊒M
  βŠ’Οƒβ‚€ ⊒M (S ())

preserve : βˆ€ {M N A}
  β†’ [] ⊒ᢜ M ⦂ A
  β†’ M β€”β†’ N
    ---------------------
  β†’ [] ⊒ᢜ N ⦂ A

frame-preserve : βˆ€ {F M N A}
  β†’ [] ⊒ᢜ plug F M ⦂ A
  β†’ M β€”β†’ N
    ------------------------
  β†’ [] ⊒ᢜ plug F N ⦂ A

frame-preserve {F = β–‘Β· M₁}  (⊒· ⊒L ⊒M) Lβ†’Lβ€² = ⊒· (preserve ⊒L Lβ†’Lβ€²) ⊒M
frame-preserve {F = V Β·β–‘ _} (⊒· ⊒V ⊒M) Mβ†’Mβ€² = ⊒· ⊒V (preserve ⊒M Mβ†’Mβ€²)
frame-preserve {F = β–‘βŸ¨ c ⟩} (⊒cast ⊒M ⊒c) Mβ†’N = ⊒cast (preserve ⊒M Mβ†’N) ⊒c

preserve ⊒M (ΞΎΞΎ refl refl Mβ†’N)    = frame-preserve ⊒M Mβ†’N
preserve (⊒· (βŠ’Ζ› ⊒N) ⊒V) (Ξ²-Ζ› _)  = sub-preserve ⊒N ⊒V
preserve (⊒cast ⊒V ⊒id) (β-id _)  = ⊒V
preserve (⊒cast ⊒V (⊒⨟ ⊒c ⊒d)) (β-seq _) = ⊒cast (⊒cast ⊒V ⊒c) ⊒d
preserve (⊒· (⊒cast ⊒V (βŠ’β‡’ ⊒c ⊒d)) ⊒W) (Ξ²-β‡’ _ _) = ⊒cast (⊒· ⊒V (⊒cast ⊒W ⊒c)) ⊒d
preserve (⊒cast (⊒cast ⊒V (⊒! g)) (⊒? _)) (β-proj-inj-ok vV) = ⊒V
preserve ⊒M (β-proj-inj-bad _ _) = ⊒blame
preserve ⊒M (ξξ-blame refl) = ⊒blame

Compilation from GTLC to CC

The coercion function takes two types that are consistent and returns a coercion. We can prove that the function always well-typed coercions.

coerce : βˆ€ {A B} β†’ Nat β†’ A ~ B β†’ Coercion
coerce β„“ ~-β„• = id β„•
coerce β„“ ~-β˜… = id β˜…
coerce β„“ β˜…~β„• = β„• `? β„“
coerce β„“ β„•~β˜… = β„• !
coerce β„“ (β˜…~β‡’ A~β˜… β˜…~B) = ((β˜… β‡’ β˜…) `? β„“) ⨟ (coerce β„“ A~β˜… β‡’ coerce β„“ β˜…~B)
coerce β„“ (β‡’~β˜… β˜…~A B~β˜…) = (coerce β„“ β˜…~A β‡’ coerce β„“ B~β˜…) ⨟ ((β˜… β‡’ β˜…) !)
coerce β„“ (~-β‡’ c d) = coerce β„“ c β‡’ coerce β„“ d

coerce-wt : βˆ€ {A B} (β„“ : Nat) (A~B : A ~ B) β†’ ⊒ coerce β„“ A~B ⦂ A β‡’ B
coerce-wt β„“ ~-β„• = ⊒id
coerce-wt β„“ ~-β˜… = ⊒id
coerce-wt β„“ β˜…~β„• = ⊒? G-β„•
coerce-wt β„“ β„•~β˜… = ⊒! G-β„•
coerce-wt β„“ (β˜…~β‡’ A~β˜… β˜…~B) = ⊒⨟ (⊒? G-β‡’) (βŠ’β‡’ (coerce-wt β„“ A~β˜…) (coerce-wt β„“ β˜…~B))
coerce-wt β„“ (β‡’~β˜… β˜…~A B~β˜…) = ⊒⨟ (βŠ’β‡’ (coerce-wt β„“ β˜…~A) (coerce-wt β„“ B~β˜…)) (⊒! G-β‡’)
coerce-wt β„“ (~-β‡’ C~A B~D) = βŠ’β‡’ (coerce-wt β„“ C~A) (coerce-wt β„“ B~D)

The semantics of GTLC is given by compilation to the cast calculus CC (for which we have already defined the reduction semantics.)


compile-βˆ‹ : βˆ€ {Ξ“ x A} β†’ Ξ“ βˆ‹ x ⦂ A β†’ Ξ“ βˆ‹ x ⦂ A
compile-βˆ‹ Z = Z
compile-βˆ‹ (S βˆ‹x) = S (compile-βˆ‹ βˆ‹x)

compile : βˆ€ {Ξ“ M A} β†’ Ξ“ ⊒ M ⦂ A β†’ Termᢜ
compile (⊒` {x = x} _) = ` x
compile (⊒$ {n = n}) = $ n
compile (βŠ’Ζ› {A = A} ⊒N) = Ζ› A Λ™ compile ⊒N
compile (⊒· {β„“ = β„“} ⊒L ⊒M Aβ€²~A) = compile ⊒L Β· ((compile ⊒M) ⟨ coerce β„“ Aβ€²~A ⟩)
compile (βŠ’Β·β˜… {A = A} {β„“ = β„“} ⊒L ⊒M) =
  (compile ⊒L ⟨ coerce β„“ (β˜…~ (β˜… β‡’ β˜…)) ⟩) Β· (compile ⊒M ⟨ coerce β„“ (~β˜… A) ⟩)

GTLC is type safe because (1) the compilation from GTLC to CC preserves types and (2) CC is type safe.

compile-preserves : βˆ€ {Ξ“ M A} (⊒M : Ξ“ ⊒ M ⦂ A) β†’ Ξ“ ⊒ᢜ compile ⊒M ⦂ A
compile-preserves (⊒` βˆ‹x) = ⊒` (compile-βˆ‹ βˆ‹x)
compile-preserves (⊒$ {n = n}) = ⊒$
compile-preserves (βŠ’Ζ› {A = A} ⊒N) = βŠ’Ζ› (compile-preserves ⊒N)
compile-preserves (⊒· {β„“ = β„“} ⊒L ⊒M Aβ€²~A) =
  ⊒· (compile-preserves ⊒L)
     (⊒cast (compile-preserves ⊒M) (coerce-wt β„“ Aβ€²~A))
compile-preserves (βŠ’Β·β˜… {A = A} {β„“ = β„“} ⊒L ⊒M) =
  ⊒· (⊒cast (compile-preserves ⊒L) (coerce-wt β„“ (β˜…~ (β˜… β‡’ β˜…))))
     (⊒cast (compile-preserves ⊒M) (coerce-wt β„“ (~β˜… A)))
This site is open source. Improve this page.