Substitution monadique sous les classeurs

Question

Dans le code Agda suivant, j'ai un langage de termes basé sur les indices de Bruijn. Je peux définir la substitution sur des termes de la manière habituelle des indices de Bruijn, en utilisant le renommage pour permettre à la substitution de se dérouler sous un classeur.

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) 

Ce que je voudrais faire est maintenant généraliser le type de Term dans une variante polymorphique, afin que je puisse définir une opération 〉〉= monadique et d'exprimer une substitution à l'aide que. Voici tentative naïve:

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

Le problème ici est que je ne sais plus comment définir extend (qui déplace une substitution dans un contexte plus profond), parce qu'une substitution est une bête plus abstraite.

est ici quelque chose de plus, sur la base du papier Names for Free par Bernardy et 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 θ) 

L'idée ici est de modéliser l'idée de l'extension de contexte d'une manière explicite abstraite, ce qui permet extend à définir pour renommages et substitutions même dans le cadre polymorphique.

Malheureusement, je semble être trop stupide pour comprendre comment étendre cette approche afin que les termes soient paramétrés par un Type, comme ils le sont dans ma première tentative ci-dessus. Je voudrais finir avec >> = ayant (environ) du type:

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

Quelqu'un peut-il me diriger dans la bonne direction?

Answer 1

Quelque chose comme ce qui suit peut-être? L'important est de savoir comment vous représentez les variables. La réponse est que dans un paramètre typé, les variables doivent être indexées par un type. Si vous faites ce changement, tout suit plus ou moins ...

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