通过效果进行通用编程

Generic programming via effects

在 Idris Effects 库中效果表示为

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

如果我们允许资源为值并交换前两个参数，我们得到（其余代码在 Agda 中）

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

拥有一些基本的类型-上下文-成员机制

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

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

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

我们可以对 lambda 项构造函数进行如下编码：

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

在TermE i r i′ i中是一个输出索引（例如lambda抽象（Lam）构造函数类型（σ ⇒ τ）（为了便于描述我将忽略索引还包含类型之外的上下文)), r 表示许多归纳位置 (Var 不 (⊥) 接收任何 TermE, Lam接收一个 (⊤)，App 接收两个 (Bool) — 一个函数及其参数）并且 i′ 在每个归纳位置计算一个索引（例如在App 的第一个归纳位置是 σ ⇒ τ，第二个位置的索引是 σ，即只有当函数的第一个参数的类型等于值的类型）。

要构造一个真正的 lambda 项，我们必须使用类似 W 的数据类型来打结。这是定义：

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

它是 Oleg Kiselyov 的 Freer monad（又是效果器）的索引变体，但没有 return。使用这个我们可以恢复通常的构造函数：

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

整个编码和corresponding encoding in terms of indexed containers非常相似：Effect对应IContainer，Wer对应ITree（Petersson-的类型Synek 树）。然而，上面的编码对我来说看起来更简单，因为你不需要考虑你必须放入形状中的东西才能在归纳位置恢复索引。相反，您可以将所有内容集中在一个地方，并且编码过程非常简单。

那我来这里做什么？与索引容器方法有什么真正的关系（除了这个编码具有相同的 extensionality problems 的事实）？我们可以这样做一些有用的事情吗？一个自然的想法是建立一个有效的 lambda 演算，因为我们可以自由地将 lambda 项与效果混合，因为 lambda 项本身只是一个效果，但它是一个外部效果，我们要么需要其他效果也是外部的（这意味着我们不能说 tell (var vz) 之类的东西，因为 var vz 不是一个值——它是一个计算）或者我们需要以某种方式内化这种效果和整个效果机制（这意味着我不知道是什么).

The code used.

有趣的作品！我对效果知之甚少，我对索引容器只有基本的了解，但我正在用泛型编程做一些事情，所以这是我的看法。

TermE : Con × Type → (A : Set) → (A → Con × Type) → Set 的类型让我想起了 [1] 中用于形式化索引归纳递归的描述类型。该论文的第二章告诉我们 Set/I = (A : Set) × (A → I) 和 I → Set 之间存在等价关系。这意味着 TermE 的类型等同于 Con × Type → (Con × Type → Set) → Set 或 (Con × Type → Set) → Con × Type → Set。后者是一个索引函子，用于泛型编程的多项式函子 ('sum-of-products') 风格，例如 [2] 和 [3]。如果你以前没见过它，它看起来像这样：

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 ⟩

因此固定点 μ 直接对应于您的 Wer 数据类型，解释的描述（使用 ⟦_⟧）对应于您的 TermE。我猜关于这个主题的一些文献可能与您相关。我不记得索引容器和索引仿函数是否真的等价，但它们肯定是相关的。我不完全理解您关于 tell (var vz) 的评论，但这是否与这些描述中的定点内在化有关？在那种情况下，也许 [3] 可以帮助你。