Programmation générique par des effets

Question

Dans les effets de la bibliothèque Idris Effects sont représentés comme

||| This type is parameterised by: 
||| + The return type of the computation. 
||| + The input resource. 
||| + The computation to run on the resource given the return value. 
Effect : Type 
Effect = (x : Type) -> Type -> (x -> Type) -> Type 

Si nous permettons à des ressources comme des valeurs et échanger les deux premiers arguments, nous obtenons (le reste du code est en Agda)

Effect : Set -> Set 
Effect R = R -> (A : Set) -> (A -> R) -> Set 

Ayant quelques machines d'adhésion de type contexte de base

data Type : Set where 
    nat : Type 
    _⇒_ : Type -> Type -> Type 

data Con : Set where 
    ε : Con 
    _▻_ : Con -> Type -> Con 

data _∈_ σ : Con -> Set where 
    vz : ∀ {Γ} -> σ ∈ Γ ▻ σ 
    vs_ : ∀ {Γ τ} -> σ ∈ Γ  -> σ ∈ Γ ▻ τ 

nous pouvons e Les constructeurs nCode lambda comme suit:

app-arg : Bool -> Type -> Type -> Type 
app-arg b σ τ = if b then σ ⇒ τ else σ 

data TermE : Effect (Con × Type) where 
    Var : ∀ {Γ σ } -> σ ∈ Γ -> TermE (Γ , σ ) ⊥  λ() 
    Lam : ∀ {Γ σ τ} ->   TermE (Γ , σ ⇒ τ) ⊤ (λ _ -> Γ ▻ σ , τ   ) 
    App : ∀ {Γ σ τ} ->   TermE (Γ , τ ) Bool (λ b -> Γ  , app-arg b σ τ) 

Dans TermE i r i′i est un index de sortie (par exemple, abstractions lambda (Lam) types de fonctions de construction (σ ⇒ τ) (pour faciliter la description que je vais ignorer que les indices contiennent aussi des contextes en dehors de types)), r représente un certain nombre de positions inductives (Var n'a pas (⊥) reçoivent une TermE, Lam reçoit un (⊤), App reçoit deux (Bool) - une fonction et son argument) et i′ calcule un indice à chaque position inductive (par exemple l'indice à la première position inductive de App est σ ⇒ τ et l'indice à la seconde est σ, c'est-à-dire que nous pouvons appliquer une fonction à une valeur seulement si le type du premier argument de la fonction est égal au type de la valeur).

Pour construire un terme lambda réel, nous devons lier le nœud en utilisant quelque chose comme un type de données W. Voici la définition:

data Wer {R} (Ψ : Effect R) : Effect R where 
    call : ∀ {r A r′ B r′′} -> Ψ r A r′ -> (∀ x -> Wer Ψ (r′ x) B r′′) -> Wer Ψ r B r′′ 

Il est la variante indexée de Freer monade Oleg Kiselyov (stuff effets à nouveau), mais sans return. L'utilisation de ce que nous pouvons récupérer les constructeurs habituels:

_<∨>_ : ∀ {B : Bool -> Set} -> B true -> B false -> ∀ b -> B b 
(x <∨> y) true = x 
(x <∨> y) false = y 

_⊢_ : Con -> Type -> Set 
Γ ⊢ σ = Wer TermE (Γ , σ) ⊥ λ() 

var : ∀ {Γ σ} -> σ ∈ Γ -> Γ ⊢ σ 
var v = call (Var v) λ() 

ƛ_ : ∀ {Γ σ τ} -> Γ ▻ σ ⊢ τ -> Γ ⊢ σ ⇒ τ 
ƛ b = call Lam (const b) 

_·_ : ∀ {Γ σ τ} -> Γ ⊢ σ ⇒ τ -> Γ ⊢ σ -> Γ ⊢ τ 
f · x = call App (f <∨> x) 

L'encodage entier est très similaire à la corresponding encoding en termes de indexed containers: Effect correspond à IContainer et Wer correspond à ITree (le type de Petersson-Synek arbres). Cependant, le codage ci-dessus me semble plus simple, parce que vous n'avez pas besoin de penser à des choses que vous devez mettre en forme pour pouvoir récupérer des indices à des positions inductives. Au lieu de cela, vous avez tout en un seul endroit et le processus d'encodage est vraiment simple.

Alors qu'est-ce que je fais ici? Existe-t-il une relation réelle avec l'approche des conteneurs indexés (outre le fait que cet encodage a le même extensionality problems)? Pouvons-nous faire quelque chose d'utile de cette façon? Une pensée naturelle est de construire un lambda-calcul efficace car nous pouvons mélanger librement des termes lambda avec des effets, car un terme lambda est lui-même un effet, mais c'est un effet externe et nous avons besoin d'autres effets externes (ce qui signifie nous ne pouvons pas dire quelque chose comme tell (var vz), parce que var vz n'est pas une valeur - c'est un calcul) ou nous avons besoin d'internaliser cet effet et toute la machinerie des effets (ce qui veut dire que je ne sais pas quoi).

The code used.

Answer 1

Un travail intéressant!Je ne connais pas grand-chose aux effets et je n'ai qu'une connaissance de base des conteneurs indexés, mais je fais des choses avec la programmation générique, alors voici mon point de vue.

Le type TermE : Con × Type → (A : Set) → (A → Con × Type) → Set me rappelle le type de descriptions utilisées pour formaliser la récursion induite indexée dans [1]. Le deuxième chapitre de cet article nous dit qu'il existe une équivalence entre Set/I = (A : Set) × (A → I) et I → Set. Cela signifie que le type TermE est équivalent à Con × Type → (Con × Type → Set) → Set ou (Con × Type → Set) → Con × Type → Set. Ce dernier est un foncteur indexé, qui est utilisé dans le style de programmation générique du foncteur polynomial ('sum-of-products'), par exemple dans [2] et [3]. Si vous ne l'avez pas vu avant, il ressemble à ceci:

data Desc (I : Set) : Set1 where 
    `Σ : (S : Set) → (S → Desc I) → Desc I 
    `var : I → Desc I → Desc I 
    `ι : I → Desc I 

⟦_⟧ : ∀{I} → Desc I → (I → Set) → I → Set 
⟦ `Σ S x ⟧ X o = Σ S (λ s → ⟦ x s ⟧ X o) 
⟦ `var i xs ⟧ X o = X i × ⟦ xs ⟧ X o 
⟦ `ι o′ ⟧ X o = o ≡ o′ 

data μ {I : Set} (D : Desc I) : I → Set where 
    ⟨_⟩ : {o : I} → ⟦ D ⟧ (μ D) o → μ D o 

natDesc : Desc ⊤ 
natDesc = `Σ Bool (λ { false → `ι tt ; true → `var tt (`ι tt) }) 
nat-example : μ natDesc tt 
nat-example = ⟨ true , ⟨ true , ⟨ false , refl ⟩ , refl ⟩ , refl ⟩ 
finDesc : Desc Nat 
finDesc = `Σ Bool (λ { false → `Σ Nat (λ n → `ι (suc n)) 
        ; true → `Σ Nat (λ n → `var n (`ι (suc n))) 
        }) 
fin-example : μ finDesc 5 
fin-example = ⟨ true , 4 , ⟨ true , 3 , ⟨ false , 2 , refl ⟩ , refl ⟩ , refl ⟩ 

Ainsi, le point fixe μ correspond directement à votre Wer type de données, et les descriptions interprétées (en utilisant ⟦_⟧) correspondent à votre TermE. Je suppose que certains documents sur ce sujet seront pertinents pour vous. Je ne me souviens pas si les conteneurs indexés et les foncteurs indexés sont vraiment équivalents, mais ils sont certainement liés. Je ne comprends pas entièrement votre remarque sur tell (var vz), mais cela pourrait-il être lié à l'internalisation des points fixes dans ce genre de descriptions? Dans ce cas peut-être [3] peut vous aider avec cela.

• [1]: Peter Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, Thorsten Altenkirch - Small Induction Recursion (2013)
• [2]: James Chapman, Pierre-Evariste Dagand, Conor McBride, Peter Morris - The gentle art of levitation (2010)
• [3]: Andres Löh, José Pedro Magalhães - Generic programming with indexed functors