Monadic substitution under binders

Question

In the following Agda code, I have a term language based on de Bruijn indices. I can define substitution over terms in the usual de Bruijn indices way, using renaming to allow the substitution to proceed under a binder.

module Temp where

data Type : Set where
   unit : Type
   _⇾_ : Type → Type → Type

-- A context is a snoc-list of types.
data Cxt : Set where
   ε : Cxt
   _∷_ : Cxt → Type → Cxt

-- Context membership.
data _∈_ (τ : Type) : Cxt → Set where
   here : ∀ {Γ} → τ ∈ Γ ∷ τ
   there : ∀ {Γ τ′} → τ ∈ Γ → τ ∈ Γ ∷ τ′
infix 3 _∈_

data Term (Γ : Cxt) : Type → Set where
   var : ∀ {τ} → τ ∈ Γ → Term Γ τ
   〈〉 : Term Γ unit
   fun : ∀ {τ₁ τ₂} → Term (Γ ∷ τ₁) τ₂ → Term Γ (τ₁ ⇾ τ₂)

-- A renaming from Γ to Γ′.
Ren : Cxt → Cxt → Set
Ren Γ Γ′ = ∀ {τ} → τ ∈ Γ → τ ∈ Γ′

extend′ : ∀ {Γ Γ′ τ′} → Ren Γ Γ′ → Ren (Γ ∷ τ′) (Γ′  ∷ τ′)
extend′ f here = here
extend′ f (there x) = there (f x)

-- Apply a renaming to a term.
_*′_ : ∀ {Γ Γ′ : Cxt} {τ} → Ren Γ Γ′ → Term Γ τ → Term Γ′ τ
f *′ var x = var (f x)
f *′ 〈〉 = 〈〉
f *′ fun e = fun (extend′ f *′ e)

-- A substitution from Γ to Γ′.
Sub : Cxt → Cxt → Set
Sub Γ Γ′ = ∀ {τ} → τ ∈ Γ → Term Γ′ τ

extend : ∀ {Γ Γ′ τ} → Sub Γ Γ′ → Sub (Γ ∷ τ) (Γ′ ∷ τ)
extend θ here = var here
extend θ (there x) = there *′ θ x

-- Apply a substitution to a term.
_*_ : ∀ {Γ Γ′ : Cxt} {τ} → Sub Γ Γ′ → Term Γ τ → Term Γ′ τ
θ * var x = θ x
θ * 〈〉 = 〈〉
θ * fun a = fun (extend θ * a)

What I would like to do now is generalise the type of Term into a polymorphic variant, so that I can define a monadic 〉〉= operation and express substitution using that. Here's naive attempt:

data Term (A : Cxt → Type → Set) (Γ : Cxt) : Type → Set where
   var : ∀ {τ} → A Γ τ → Term A Γ τ
   〈〉 : Term A Γ unit
   fun : ∀ {τ₁ τ₂} → Term A (Γ ∷ τ₁) τ₂ → Term A Γ (τ₁ ⇾ τ₂)

Sub : (Cxt → Type → Set) → Cxt → Cxt → Set
Sub A Γ Γ′ = ∀ {τ} → A Γ τ → Term A Γ′ τ

extend : ∀ {A : Cxt → Type → Set} {Γ Γ′ τ} → Sub A Γ Γ′ → Sub A (Γ ∷ τ) (Γ′ ∷ τ)
extend θ = {!!}

_〉〉=_ : ∀ {A : Cxt → Type → Set} {Γ Γ′ : Cxt} {τ} → 
       Term A Γ τ → Sub A Γ Γ′ → Term A Γ′ τ
var x 〉〉= θ = θ x
〈〉 〉〉= θ = 〈〉
fun a 〉〉= θ = fun (a 〉〉= extend θ)

The problem here is that I no longer know how to define extend (which shifts a substitution into a deeper context), because a substitution is a more abstract beast.

Here's something closer, based on the paper Names for Free by Bernardy and Pouillard:

module Temp2 where

open import Data.Unit

data _▹_ (A : Set) (V : Set) : Set where
   here : V → A ▹ V
   there : A → A ▹ V

data Term (A : Set) : Set where
   var : A → Term A
   〈〉 : Term A
   fun : Term (A ▹ ⊤) → Term A

Ren : Set → Set → Set
Ren Γ Γ′ = Γ → Γ′

extend′ : ∀ {Γ Γ′ V : Set} → Ren Γ Γ′ → Ren (Γ ▹ V) (Γ′ ▹ V)
extend′ f (here x) = here x
extend′ f (there x) = there (f x)

Sub : Set → Set → Set
Sub Γ Γ′ = Γ → Term Γ′

_<$>_ : ∀ {Γ Γ′ : Set} → Ren Γ Γ′ → Term Γ → Term Γ′
f <$> var x = var (f x)
f <$> 〈〉 = 〈〉
f <$> fun e = fun (extend′ f <$> e)

extend : ∀ {Γ Γ′ V : Set} → Sub Γ Γ′ → Sub (Γ ▹ V) (Γ′ ▹ V)
extend θ (here x) = var (here x)
extend θ (there x) = there <$> θ x

_〉〉=_ : ∀ {Γ Γ′ : Set} → Term Γ → Sub Γ Γ′ → Term Γ′
var x 〉〉= θ = θ x
〈〉 〉〉= θ = 〈〉
fun a 〉〉= θ = fun (a 〉〉= extend θ)

The idea here is to model the idea of context extension in an explicitly abstract way, allowing extend to be defined for renamings and substitutions even in the polymorphic setting.

Unfortunately, I seem to be too stupid to understand how to extend this approach so that terms are parameterised by a Type, as they are in my first attempt above. I would like to end up with 〉〉= having (approximately) the following type:

_〉〉=_ : ∀ {Γ Γ′ : Set} {τ} → Term Γ τ → (Sub Γ Γ′) → Term Γ′ τ

Can anyone point me in the right direction?

Answer 1

Something like the following perhaps? The important thing is how you represent variables. The answer is that in a typed setting, variables need to be indexed by a type. If you make that change, everything more or less follows...

module Temp2 where

open import Data.Unit
open import Data.Empty
open import Relation.Binary.PropositionalEquality

data Type : Set where
   unit : Type
   _⟶_ : Type → Type → Type

data _▹_ (A : Type → Set) (V : Type → Set) (t : Type) : Set where
   here : V t → (A ▹ V) t
   there : A t → (A ▹ V) t

data Term (A : Type → Set) : Type → Set where
   var : ∀ {t} → A t → Term A t
   〈〉 : Term A unit
   fun : ∀ {t : Type} {T : Type} → Term (A ▹ (_≡_ T)) t → Term A (T ⟶ t)

Ren : (Type → Set) → (Type → Set) → Set
Ren Γ Γ′ = ∀ {t} → Γ t → Γ′ t

extend′ : ∀ {Γ Γ′ V : Type → Set} → Ren Γ Γ′ → Ren (Γ ▹ V) (Γ′ ▹ V)
extend′ f (here x) = here x
extend′ f (there x) = there (f x)

Sub : (Type → Set) → (Type → Set) → Set
Sub Γ Γ′ = ∀ {t} → Γ t → Term Γ′ t

_<$>_ : ∀ {Γ Γ′ : Type → Set} {t} → Ren Γ Γ′ → Term Γ t → Term Γ′ t
f <$> var x = var (f x)
f <$> 〈〉 = 〈〉
f <$> fun e = fun (extend′ f <$> e)

extend : ∀ {Γ Γ′ V : Type → Set} → Sub Γ Γ′ → Sub (Γ ▹ V) (Γ′ ▹ V)
extend θ (here x) = var (here x)
extend θ (there x) = there <$> θ x

_〉〉=_ : ∀ {Γ Γ′ : Type → Set} {t} → Term Γ t → Sub Γ Γ′ → Term Γ′ t
var x 〉〉= θ = θ x
〈〉 〉〉= θ = 〈〉
fun a 〉〉= θ = fun (a 〉〉= extend θ)