programmazione generica con effetti

Question

Nelle Idris Effects effetti della biblioteca sono rappresentati come

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

Se permettiamo risorse siano valori e scambiare i primi due argomenti, otteniamo (il resto del codice è in Agda)

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

Avendo alcuni macchinari di base tipo-contesto-adesione

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

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

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

possiamo all'e nCode termini lambda costruttori come segue:

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 è un indice di uscita (ad esempio astrazioni lambda tipi (Lam) funzione construct (σ ⇒ τ) (per facilità di descrizione I ignoreranno che indici contengono anche contesti oltre tipi)), r rappresenta un numero di posizioni induttivi (Var non significa (⊥) ricevono alcun TermE, Lam riceve uno (⊤), App riceve due (Bool) - una funzione e il suo argomento) e i′ calcola un indice per ogni posizione induttiva (ad esempio l'indice nella prima posizione induttiva di App è σ ⇒ τ e l'indice al secondo è σ, cioè possiamo applicare una funzione ad un valore solo se il tipo del primo argomento della funzione è uguale al tipo del valore).

Per creare un termine lambda reale, è necessario eseguire il nodo utilizzando qualcosa come il tipo di dati W. Ecco la definizione:

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

E 'la variante indicizzato di Freer monade del Oleg Kiselyov (roba effetti di nuovo), ma senza return. Usando questo possiamo recuperare i soliti costruttori:

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

Tutta codifica è molto simile alla corresponding encoding in termini di indexed containers: Effect corrisponde IContainer e Wer corrisponde ITree (tipo di Petersson-Synek alberi). Tuttavia la codifica di cui sopra mi sembra più semplice, perché non devi pensare a cose che devi mettere in forma per essere in grado di recuperare indici in posizioni induttive. Invece, hai tutto in un posto e il processo di codifica è davvero semplice.

Quindi cosa ci faccio qui? C'è qualche relazione reale con l'approccio dei contenitori indicizzati (oltre al fatto che questa codifica ha lo stesso extensionality problems)? Possiamo fare qualcosa di utile in questo modo? Un pensiero naturale è di costruire un calcolo lambda efficace poiché possiamo liberamente mescolare termini lambda con effetti, dal momento che un termine lambda è di per sé solo un effetto, ma è un effetto esterno e abbiamo bisogno anche di altri effetti per essere esterni (il che significa che non possiamo dire qualcosa come tell (var vz), perché var vz non è un valore - è un calcolo) o dobbiamo in qualche modo interiorizzare questo effetto e l'intero meccanismo degli effetti (il che significa che non so cosa).

The code used.

Answer 1

Lavori interessanti!Non ne so molto degli effetti e ho solo una conoscenza di base dei contenitori indicizzati, ma sto facendo cose con la programmazione generica quindi ecco la mia opinione su di esso.

Il tipo di TermE : Con × Type → (A : Set) → (A → Con × Type) → Set mi ricorda il tipo di descrizioni utilizzate per formalizzare la ricorsione dell'induzione indicizzata in [1]. Il secondo capitolo di questo articolo ci dice che esiste un'equivalenza tra Set/I = (A : Set) × (A → I) e I → Set. Ciò significa che il tipo di TermE equivale a Con × Type → (Con × Type → Set) → Set o (Con × Type → Set) → Con × Type → Set. Quest'ultimo è un funtore indicizzato, che viene utilizzato nello stile del functor polinomiale ('sum-of-products') della programmazione generica, ad esempio in [2] e [3]. Se non avete visto prima, sembra qualcosa di simile:

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 ⟩ 

Così il punto fisso μ corrisponde direttamente al vostro Wer tipo di dati, e le descrizioni interpretati (usando ⟦_⟧) corrispondono alla tua TermE. Immagino che parte della letteratura su questo argomento sarà rilevante per te. Non ricordo se i contenitori indicizzati e i funtori indicizzati siano realmente equivalenti, ma sono sicuramente correlati. Non capisco completamente la tua osservazione su tell (var vz), ma potrebbe essere correlata all'internalizzazione dei punti di correzione in questi tipi di descrizioni? In tal caso forse [3] può aiutarti in questo.

[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