通过效果进行通用编程

Question

在Idris 效果库中,效果表示为

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

In TermE i r i? i是一个输出索引(例如lambda abstractions(Lam)构造函数类型(? ? ?)(为了便于描述,我将忽略索引还包含除类型之外的上下文)),r表示一些归纳位置(Var不?接收任何TermE,)Lam接收一个(?),App接收两个(Bool) - 一个函数及其参数)并i?计算每个归纳位置的索引(例如,Appis 的第一个归纳位置? ? ?的索引和第二个的索引?,即我们可以应用一个函数仅当函数的第一个参数的类型等于值的类型时的值).

要构造一个真正的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的Freermonad 的索引变体(再次效果),但没有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)

整个编码在索引容器方面与相应的编码非常相似:对应于(对应于Petersson-Synek树的类型).然而,上面的编码对我来说看起来更简单,因为您不需要考虑必须放入形状的东西才能在归纳位置恢复索引.相反,您将所有内容放在一个位置,编码过程非常简单.EffectIContainerWerITree

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

使用的代码.

Answer 1

有趣的工作！我对效果了解不多，而且对索引容器只有基本的了解，但我正在使用通用编程来做一些事情，所以这是我的看法。

\n\n

的类型TermE : Con \xc3\x97 Type \xe2\x86\x92 (A : Set) \xe2\x86\x92 (A \xe2\x86\x92 Con \xc3\x97 Type) \xe2\x86\x92 Set让我想起了[1]中用于形式化索引归纳递归的描述类型。Set/I = (A : Set) \xc3\x97 (A \xe2\x86\x92 I)该论文的第二章告诉我们和 之间存在等价关系I \xe2\x86\x92 Set。这意味着 的类型TermE相当于Con \xc3\x97 Type \xe2\x86\x92 (Con \xc3\x97 Type \xe2\x86\x92 Set) \xe2\x86\x92 Setor(Con \xc3\x97 Type \xe2\x86\x92 Set) \xe2\x86\x92 Con \xc3\x97 Type \xe2\x86\x92 Set。后者是一个索引函子，用于泛型编程的多项式函子（“乘积和”）风格，例如[2]和[3]中。如果您以前没有见过它，它看起来像这样：

\n\n

data Desc (I : Set) : Set1 where\n  `\xce\xa3 : (S : Set) \xe2\x86\x92 (S \xe2\x86\x92 Desc I) \xe2\x86\x92 Desc I\n  `var : I \xe2\x86\x92 Desc I \xe2\x86\x92 Desc I\n  `\xce\xb9 : I \xe2\x86\x92 Desc I\n\n\xe2\x9f\xa6_\xe2\x9f\xa7 : \xe2\x88\x80{I} \xe2\x86\x92 Desc I \xe2\x86\x92 (I \xe2\x86\x92 Set) \xe2\x86\x92 I \xe2\x86\x92 Set\n\xe2\x9f\xa6 `\xce\xa3 S x \xe2\x9f\xa7 X o = \xce\xa3 S (\xce\xbb s \xe2\x86\x92 \xe2\x9f\xa6 x s \xe2\x9f\xa7 X o)\n\xe2\x9f\xa6 `var i xs \xe2\x9f\xa7 X o = X i \xc3\x97 \xe2\x9f\xa6 xs \xe2\x9f\xa7 X o\n\xe2\x9f\xa6 `\xce\xb9 o\xe2\x80\xb2 \xe2\x9f\xa7 X o = o \xe2\x89\xa1 o\xe2\x80\xb2\n\ndata \xce\xbc {I : Set} (D : Desc I) : I \xe2\x86\x92 Set where\n  \xe2\x9f\xa8_\xe2\x9f\xa9 : {o : I} \xe2\x86\x92 \xe2\x9f\xa6 D \xe2\x9f\xa7 (\xce\xbc D) o \xe2\x86\x92 \xce\xbc D o\n\nnatDesc : Desc \xe2\x8a\xa4\nnatDesc = `\xce\xa3 Bool (\xce\xbb { false \xe2\x86\x92 `\xce\xb9 tt ; true \xe2\x86\x92 `var tt (`\xce\xb9 tt) })\nnat-example : \xce\xbc natDesc tt\nnat-example = \xe2\x9f\xa8 true , \xe2\x9f\xa8 true , \xe2\x9f\xa8 false , refl \xe2\x9f\xa9 , refl \xe2\x9f\xa9 , refl \xe2\x9f\xa9\nfinDesc : Desc Nat\nfinDesc = `\xce\xa3 Bool (\xce\xbb { false \xe2\x86\x92 `\xce\xa3 Nat (\xce\xbb n \xe2\x86\x92 `\xce\xb9 (suc n))\n                     ; true \xe2\x86\x92 `\xce\xa3 Nat (\xce\xbb n \xe2\x86\x92 `var n (`\xce\xb9 (suc n)))\n                     })\nfin-example : \xce\xbc finDesc 5\nfin-example = \xe2\x9f\xa8 true , 4 , \xe2\x9f\xa8 true , 3 , \xe2\x9f\xa8 false , 2 , refl \xe2\x9f\xa9 , refl \xe2\x9f\xa9 , refl \xe2\x9f\xa9\n

\n\n

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

\n\n

\n
• [1]： Peter Hancock、Conor McBride、Neil Ghani、Lorenzo Malatesta、Thorsten Altenkirch - 小归纳递归 (2013)
\n
• [2]：James Chapman、Pierre-Evariste Dagand、Conor McBride、Peter Morris - 悬浮的温柔艺术 (2010)
\n
• [3]: Andres L\xc3\xb6h, Jos\xc3\xa9 Pedro Magalh\xc3\xa3es - 使用索引函子的通用编程
\n

\n