haskell - trabajo - programacion generica java

Programación genérica vía efectos. (1)

En la biblioteca de efectos de Idris los efectos se representan como

||| 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 permitimos que los recursos sean valores e intercambiemos los dos primeros argumentos, obtenemos (el resto del código está en Agda)

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

Tener alguna maquinaria básica de tipo de contexto de tipo

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

Podemos codificar los constructores de términos lambda de la siguiente manera:

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

En TermE iri′ es un índice de salida (p. Ej., Abstracciones lambda ( Lam ) construye tipos de función ( σ ⇒ τ ) (para facilitar la descripción, ignoraré que los índices también contienen contextos además de tipos)), r representa un número de posiciones inductivas ( Var no ( ⊥ ) recibe ningún TermE , Lam recibe uno ( ⊤ ), App recibe dos ( Bool ) - una función y su argumento) e i′ calcula un índice en cada posición inductiva (por ejemplo, el índice en la primera inductiva la posición de la App es σ ⇒ τ y el índice en el segundo es σ , es decir, podemos aplicar una función a un valor solo si el tipo del primer argumento de la función es igual al tipo del valor).

Para construir un término lambda real, debemos atar el nudo utilizando algo como un tipo de datos W Aquí está la definición:

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 la variante indexada de la mónada Freer Oleg Kiselyov (efectos de nuevo), pero sin return . Usando esto podemos recuperar los constructores habituales:

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

Toda la codificación es muy similar a la codificación correspondiente en términos de contenedores indexados : el Effect corresponde a IContainer y Wer corresponde a ITree (el tipo de árboles de Petersson-Synek). Sin embargo, la codificación anterior me parece más sencilla, ya que no es necesario pensar en las cosas que hay que poner en formas para poder recuperar índices en posiciones inductivas. En su lugar, tiene todo en un solo lugar y el proceso de codificación es realmente sencillo.

Entonces, ¿qué estoy haciendo aquí? ¿Existe alguna relación real con el enfoque de los contenedores indexados (además del hecho de que esta codificación tiene los mismos problemas de extensionalidad )? ¿Podemos hacer algo útil de esta manera? Un pensamiento natural es construir un cálculo lambda efectivo ya que podemos combinar libremente los términos lambda con los efectos, ya que un término lambda es en sí mismo solo un efecto, pero es un efecto externo y necesitamos que otros efectos también sean externos (lo que significa que no podemos decir algo como tell (var vz) , porque var vz no es un valor (es un cálculo) o necesitamos internalizar de alguna manera este efecto y toda la maquinaria de efectos (lo que significa que no sé qué).

El código utilizado .

¡Trabajo interesante! No sé mucho acerca de los efectos y solo tengo una comprensión básica de los contenedores indexados, pero estoy haciendo cosas con programación genérica, así que aquí tengo mi opinión.

El tipo de TermE : Con × Type → (A : Set) → (A → Con × Type) → Set me recuerda el tipo de descripciones usadas para formalizar la recursión de inducción indexada en [1]. El segundo capítulo de ese documento nos dice que hay una equivalencia entre Set/I = (A : Set) × (A → I) y I → Set . Esto significa que el tipo de TermE es equivalente a Con × Type → (Con × Type → Set) → Set o (Con × Type → Set) → Con × Type → Set . Este último es un functor indexado, que se utiliza en el estilo de programación genérica del funtor polinomial ("suma de productos"), por ejemplo, en [2] y [3]. Si no lo has visto antes, se ve algo así:

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 ⟩

Por lo tanto, el punto de referencia μ corresponde directamente a su tipo de datos Wer , y las descripciones interpretadas (usando ⟦_⟧ ) corresponden a su TermE . Supongo que algunas de las publicaciones sobre este tema serán relevantes para usted. No recuerdo si los contenedores indexados y los funtores indexados son realmente equivalentes, pero definitivamente están relacionados. No entiendo completamente su comentario sobre tell (var vz) , pero ¿podría estar relacionado con la internalización de los puntos de corrección en este tipo de descripciones? En ese caso, tal vez [3] pueda ayudarte con eso.