haskell - 通过效果进行通用编程

Question

在 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 项，我们必须使用类似 σ 的东西来打结。数据类型。这是定义:

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 的 W 的索引变体monad(再次影响东西)，但没有 Freer .使用它我们可以恢复通常的构造函数:

_<∨>_ : ∀ {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 非常相似根据 indexed containers : return对应于 Effect和 IContainer对应于 Wer (Petersson-Synek 树的类型)。然而，上面的编码对我来说看起来更简单，因为你不需要考虑你必须放入形状中的东西才能在归纳位置恢复索引。相反，您将所有东西都放在一个地方，并且编码过程非常简单。

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

The code used .

Answer 1

有趣的工作!我对效果了解不多，对索引容器只有基本的了解，但我正在使用通用编程做一些事情，所以这是我的看法。
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] 可以帮助您。

[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