GADT G of the paper

This file implements the GADT G presented in Example 2.2 in the paper.

module G where

open import map
open import nat using (Nat[] ; ⊢Nat)
open import list using (List[_] ; ⊢List ; nil[] ; cons[_,_])
open import Data.Unit renaming (tt to ∗)
open import Data.List using ([] ; _∷_ ; [_])
open import Data.Vec renaming ([] to [||] ; _∷_ to _¦_  ; [_] to [|_|] )
open import Data.Product using (_,_)

If we want to use different variables for each data constructors of G, we need six type variables and the corresponding contexts.

α β γ δ γ' δ' : mix-var
α = tvar 0
β = tvar 1
γ = tvar 2
δ = tvar 3
γ' = tvar 4
δ' = tvar 5

Γα Γβ Γγδ Γγ'δ' : type-context {mix-var}
Γα = ⟦ [| α |] ⟧
Γβ = ⟦ [| β |] ⟧
Γγδ = ⟦ γ ¦ δ ¦ [||] ⟧
Γγ'δ' = ⟦ γ' ¦ δ' ¦ [||] ⟧

Now we define G following the definition given in Example 2.2.

G-id : id-TC-var
G-id = 5

G-name : TC-var 1
G-name = TC G-id 1

const-id flat-id inj-id pairing-id projpair-id : id-data-constructor
const-id = 50
flat-id = 51
inj-id = 52
pairing-id = 53
projpair-id = 54

const flat inj pairing projpair : data-constructor 1
const = const-id ∷ [] ⇒ᵀ [| Nat[] |]
flat =
  flat-id ∷
  [
    List[ appᵀ G-name [ [| varᵀ α |] ] ]
  ]
  ⇒ᵀ
  [|
    List[ varᵀ α ]
  |]
inj = inj-id ∷ [ varᵀ β ] ⇒ᵀ [| varᵀ β |]
pairing =
  pairing-id ∷
    (appᵀ G-name [ [| varᵀ γ |] ] ∷  appᵀ G-name [ [| varᵀ δ |] ] ∷ [])
  ⇒ᵀ
    [| varᵀ γ ×ᵀ varᵀ δ |]
projpair = 
  projpair-id ∷
    [ appᵀ G-name [ [| (appᵀ G-name [ [| varᵀ γ' |] ]) ×ᵀ (appᵀ G-name [ [| varᵀ δ' ×ᵀ varᵀ δ' |] ]) |] ] ]
  ⇒ᵀ
    [| varᵀ γ' ×ᵀ varᵀ δ' |]

G : user-defined {mix-var} 1
G = dataᵀ G-name whereᵀ (const ∷ flat ∷ inj ∷ pairing ∷ projpair ∷ [])

G[_] = λ x → data-typeᵀ G [ [| x |] ]
const[] = dc const [||]
flat[_] = λ x → dc flat [| x |]
inj[_] = λ x → dc inj [| x |]
pairing[_,_] = λ x y → dc pairing (x ¦ y ¦ [||])
projpair[_] = λ x → dc projpair [| x |]

Finally, we justify the application of G to a type expression, by first justifying each of its constructors.

⊢const : ∅ ∥ ∅  ⊢ᶜ const
⊢const = dcᵀ-intro {G = G-name} ∗ (⊢Nat , ∗)

⊢flat : Γα ∥ ∅  ⊢ᶜ flat
⊢flat =
  dcᵀ-intro {G = G-name}
  (⊢List (app-intro (var-intro ∋-last , ∗) ∋-last) , ∗)
  (⊢List (var-intro ∋-last) , ∗)

⊢inj : Γβ ∥ ∅  ⊢ᶜ inj
⊢inj = dcᵀ-intro {G = G-name} (var-intro ∋-last , ∗) (var-intro ∋-last , ∗)

⊢pairing : Γγδ ∥ ∅  ⊢ᶜ pairing
⊢pairing =
  dcᵀ-intro {G = G-name}
  (
    app-intro (var-intro (∋-rec ∋-last) , ∗) ∋-last
  , app-intro (var-intro ∋-last , ∗) ∋-last
  , ∗
  )
  (
    ×-intro (var-intro (∋-rec ∋-last)) (var-intro ∋-last)
  , ∗
  )

⊢projpair : Γγ'δ' ∥ ∅  ⊢ᶜ projpair
⊢projpair =
  dcᵀ-intro {G = G-name}
  (
    app-intro (
      ×-intro
      (app-intro (var-intro (∋-rec ∋-last) , ∗) ∋-last)
      (app-intro (×-intro (var-intro ∋-last) (var-intro ∋-last) , ∗) ∋-last)
    , ∗
    ) ∋-last
  , ∗
  )
  (
    ×-intro (var-intro (∋-rec ∋-last)) (var-intro ∋-last)
  , ∗
  )

⊢G : ∀ {Γ χ φ} → _ → Γ ∥ χ ⊢ G[ φ ] 
⊢G ⊢φ =
  data-intro {k = 1} {G = G-name}
  {Γcs = ∅ ∷ Γα ∷ Γβ ∷ Γγδ ∷ Γγ'δ' ∷ []}
  {χcs = ∅ ∷ ∅ ∷ ∅ ∷ ∅ ∷ ∅ ∷ []}
  (⊢const , ⊢flat , ⊢inj , ⊢pairing , ⊢projpair , ∗)
  (⊢φ , ∗)