Монадическое замещение под связующими

Question

В следующем коде Agda у меня есть термин язык, основанный на индексах де Брюйна. Я могу определить замену по терминам обычным способом индексов де Брюйна, используя переименование, чтобы позволить замене проходить под связующим.

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)

То, что я хотел бы сделать сейчас, это обобщить тип Term в полиморфный вариант, так что я могу определить монадический 〉〉= операция и экспресс-замена с использованием этого. Вот наивная попытка:

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 θ)

Проблема в том, что я больше не знаю, как определить extend (который переносит замену в более глубокий контекст), потому что замещение является более абстрактным зверем.

Вот что-то ближе, основываясь на статье " Имена бесплатно " Бернарди и Пуйяра:

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 θ)

Идея здесь состоит в том, чтобы смоделировать идею расширения контекста явно абстрактным образом, позволяя extend быть определенным для переименований и замен даже в полиморфных условиях.

К сожалению, я, кажется, слишком глуп, чтобы понять, как расширить этот подход, чтобы параметры определялись Type, как они в моей первой попытке выше. Я хотел бы закончить с 〉〉 = (примерно) следующего типа:

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

Может кто-то указать мне верное направление?

Answer 1

Что-то вроде следующего возможно? Важно то, как вы представляете переменные. Ответ заключается в том, что в типизированном параметре переменные должны быть проиндексированы по типу. Если вы сделаете это изменение, все более или менее следует...

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 θ)