Allgemeine Programmierung über Effekte

Question

In den Idris Effects Bibliothek Effekte werden als

vertreten

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

Wenn wir zulassen, dass Ressourcen Werte sein und die ersten beiden Argumente tauschen, erhalten wir (der Rest des Codes ist in Agda)

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

Nachdem einige grundlegende Art-Kontext-Mitgliedschaft Maschinen

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

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

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

können wir E ncode lambda Begriffe Konstruktoren wie folgt:

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 σ τ) 

In TermE i r i′i ist ein Ausgangsindex (z.B. Lambda-Abstraktionen (Lam) Konstrukt Funktionstypen (σ ⇒ τ) (zur Erleichterung der Beschreibung werde ich ignorieren, dass Indizes auch Kontexte neben Typen enthalten)), r stellt eine Reihe von induktiven Positionen (Var nicht (⊥) erhalten jede TermE, Lam empfängt einen (⊤), App empfängt zwei (Bool) - eine Funktion und sein Argument) und i′ berechnet einen Index an jeder induktiven Position (zB der Index an der ersten induktiven Position App ist σ ⇒ τ und der Index an der zweiten ist , Dh wir können nur dann eine Funktion auf einen Wert anwenden, wenn der Typ des ersten Arguments der Funktion dem Typ des Wertes entspricht.

Um einen echten Lambda-Term zu konstruieren, müssen wir den Knoten mit etwas wie einem W Datentyp binden. Hier ist die Definition:

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′′ 

Es ist die indexierte Variante der Freer Oleg Kiselyov Monade (Effekte Sachen wieder), aber ohne return. Mit diesem können wir die übliche Konstrukteurs erholen:

_<∨>_ : ∀ {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) 

Die gesamte Codierung ist sehr ähnlich wie die corresponding encoding in Bezug auf indexed containers: Effect entspricht IContainer und Wer entspricht ITree (die Art von Petersson-Synek Bäumen). Die obige Kodierung erscheint mir jedoch einfacher, weil Sie nicht über Dinge nachdenken müssen, die Sie in Formen setzen müssen, um Indizes an induktiven Positionen wiederherstellen zu können. Stattdessen haben Sie alles an einem Ort und der Codierungsprozess ist wirklich unkompliziert.

Also, was mache ich hier? Gibt es eine echte Beziehung zum Ansatz indizierter Container (abgesehen von der Tatsache, dass diese Codierung die gleiche extensionality problems hat)? Können wir auf diese Weise etwas Nützliches tun? Ein natürlicher Gedanke ist es, ein effektives Lambda-Kalkül zu erstellen, da wir Lambda-Terme mit Effekten beliebig mischen können, da ein Lambda-Term selbst nur ein Effekt ist, aber es ist ein externer Effekt und wir brauchen andere Effekte auch external wir können nichts sagen wie tell (var vz), denn var vz ist kein Wert - es ist eine Berechnung) oder wir müssen diesen Effekt und die ganze Effektmaschinerie irgendwie internalisieren (was bedeutet, dass ich nicht weiß was).

The code used.

Answer 1

Interessante Arbeit!Ich weiß nicht viel über Effekte und ich habe nur ein grundlegendes Verständnis von indizierten Containern, aber ich mache Sachen mit generischer Programmierung, also hier ist meine Sicht darauf.

Der Typ von TermE : Con × Type → (A : Set) → (A → Con × Type) → Set erinnert mich an den Typ der Beschreibungen, die verwendet werden, um indexierte Induktionsrekursion in [1] zu formalisieren. Das zweite Kapitel dieses Artikels zeigt uns, dass es eine Gleichwertigkeit zwischen Set/I = (A : Set) × (A → I) und I → Set gibt. Dies bedeutet, dass der Typ TermE äquivalent zu Con × Type → (Con × Type → Set) → Set oder (Con × Type → Set) → Con × Type → Set ist. Letzteres ist ein indizierter Funktor, der im polynomialen Funktorstil ('sum-of-products') der generischen Programmierung verwendet wird, beispielsweise in [2] und [3]. Wenn Sie es noch nie zuvor gesehen, sieht es so etwas wie diese:

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 ⟩ 

So ist die Fixpoint μ direkt auf Ihren Wer Datentyp entspricht, und die interpretierten Beschreibungen (mit ⟦_⟧) Ihren TermE entsprechen. Ich schätze, dass ein Teil der Literatur zu diesem Thema für Sie relevant sein wird. Ich erinnere mich nicht, ob indizierte Container und indizierte Funktoren wirklich gleichwertig sind, aber sie sind definitiv verwandt. Ich verstehe Ihre Bemerkung über nicht ganz, aber könnte das mit der Internalisierung von Fixpunkten in diesen Beschreibungen zusammenhängen? In diesem Fall kann dir vielleicht [3] dabei helfen.

• [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