CODEWITHSUNDEEP
typesagda
cyberglot
cyberglot

Reputation: 385

Formalizing multiple type judgements ⊢ within the same Γ in Agda

I'm an Agda beginner! I have read both Programming language foundations in Agda and Verified functional programming in Agda, and now I want to try to formalize a small language by myself. As I am interested in Algebraic Effects and Handlers, I started with Pretnar's tutorial "An Introduction to Algebraic Effects and Handlers". Pretnar's language has 2 type judgements (Γ ⊢ values and Γ ⊢ computations) as it is usual to follow an approach close to CBPV. Also, as it is suggested in PLPA, I'm trying to use de Bruijn representation.

Some of the code I have:

mutual
  data ValueType : Set where
    ~ℕ      : ValueType
    ~𝔹      : ValueType
    ~⊤      : ValueType
    _⟶_    : ValueType → CompType → ValueType
    _⇒_     : CompType → CompType → ValueType

  data CompType : Set where
    _!_ : ValueType → Δ → CompType

data Type : Set where
  ⋆ : ValueType → Type
  ✪ : CompType → Type

data Context : Set where
  ∅   : Context
  _,_ : Context → Type → Context

data _∋_ : Context → Type → Set where
  Z  : ∀ {Γ A}   → Γ , A ∋ A
  S_ : ∀ {Γ A B} → Γ ∋ B → Γ , A ∋ B

mutual
  data _⊢ₖ_ : Context → CompType → Set where
  -- computation defs go here
  data _⊢ₑ_ : Context → ValueType → Set where
  -- values defs go here

data _⊢_ : Context → Type → Set where
  ~_ : ∀ {Γ A}
     → Γ ∋ A
       -----
     → Γ ⊢ A

  ⋆ : ∀ {Γ} {A : ValueType}
    → Γ ⊢ₑ A
      ------
    → Γ ⊢ ⋆ A

  ✪ : ∀ {Γ} {C : CompType}
    → Γ ⊢ₖ C
      -------
    → Γ ⊢ ✪ C

Then I proceed to prove renaming and substitution, which is where my problem arises: how can I prove them?

mutual
  renameₑ : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) 
      → (∀ {A} → Γ ⊢ₑ A → Δ ⊢ₑ A)
  renameₖ : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
      → (∀ {A} → Γ ⊢ₖ A → Δ ⊢ₖ A)

rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
   → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
rename ρ (~ x) = ~ (ρ x)
rename ρ (⋆ A) = {!!} (renameₑ ρ (⋆ A))
rename ρ (✪ A) = {!!} (renameₖ ρ (✪ A))

I can prove a rename for each of the judgements, but I can seem to find a way to prove the "main" rename function that unifies them. I wonder if this is a correct way to proceed, and I will just need to make my proofs come along (and if so, how?)... or is there another, better way to formalise the language I'm interested in in Agda?

Upvotes: 1

Views: 117

Answers (1)

effectfully
effectfully

Reputation: 12715

If you write

rename ρ (⋆ E) = {!!}

and look at the context in the hole, you'll see that E is of type .Γ ⊢ₑ .A. This can be readily renamed using renameₑ:

renameₑ ρ E

which is of type .Δ ⊢ₑ .A and it only remains to apply ⋆ to the result to get an .Δ ⊢ .A.

The basic idea is that you pattern match on a term, figure out whether it's a value or a computation, apply the corresponding renaming function and wrap the result using the same constructor. I.e. rename maps values to values and computations to computations, but uses different renaming functions for these judgements under the hood.

The code:

rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
       → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
rename ρ (~ x) = ~ (ρ x)
rename ρ (⋆ E) = ⋆ (renameₑ ρ E)
rename ρ (✪ E) = ✪ (renameₖ ρ E)

Upvotes: 1

Related Questions