异域编程思想：第3部分（效果系统）

继续我们关于奇异编程思想的系列，我们将探索效果的主题。在许多主流编程语言中发现了效果标记的形式较弱，但是，在整个效果系统中使用编程来定义语法以定义和标记表面语法中的效果区域仍然是语言设计中的空白。

首先，我们应该定义一种效果。我们将采用函数式编程学科中常用的定义，这仅仅是因为它具有一个精确的定义，而口语用法通常是不常用的。首先，纯函数是一个代码单元，其返回值完全由其输入确定，除了简单地返回一个值外没有其他可观察到的效果。纯函数是编程中的函数，其行为类似于数学中的函数。例如，在Python代码中，我们表示一个称为f的“函数”：

在此定义中有几点要提及。首先是我们对效果的分析中的视角问题。该Python函数编译为一系列字节码，这些字节码可操作堆栈变量，在堆上m分配兆字节的数据，调用垃圾收集器，并在CPU的寄存器中交换出数十万个值，所有这些都对应于对PyObject结构内的任意大小的整数。从基础实现的角度来看，所有这些都是非常有效的，但是我们无法从普通语言中观察这些内部组件的功能。

纯函数式编程的主要思想是编程将不可避免地由纯逻辑和有效（有时称为不纯）逻辑组成。另外，我们认为表面语言的一个有用特性是能够区分具有效果的逻辑单元，并能够对这些类型的效果进行分类，以便更多地考虑程序组成。

替代方法是在大多数语言中找到的模型，在该模型中，所有逻辑都被分解成巨大的效果，并依赖于程序员的直觉和内部思维模型来区分哪些代码可以执行效果（内存分配，副通道等）。 ）和逻辑。对效果系统的研究从根本上讲是将我们对正确程序效果综合的直觉规范化为正式模型，编译器可以代表我们进行推理并以符合人体工程学的方式与开发人员工具进行交互。

在过去十年的大部分时间里，像Idris，Haskell，F *等功能语言和其他一些研究语言一直在探索设计空间。诸如monads之类的概念在划分纯逻辑和不纯逻辑方面已进行了初步探索，但由于该模型在实用性方面遇到了障碍，因此近年来有所下降。主动探索的最常见领域是一个称为代数效应处理程序的领域，它允许采用一种易于处理的推理算法来检查有效逻辑，同时又不会引入任何运行时开销。

没有使用该模型的主流语言，但是Microsoft研究实验室提供了一种称为Koka的学术语言，它提供了这些想法的最先进的实现。据我所知，没有人将这种语言用于任何事物，但是，探索这些想法是可以下载的并且非常有用。我们将在Koka中编写所有示例代码。

在Koka中，没有任何效果表示为效果总数。计算函数f的唯一结果就是简单地返回其输入的平方。

但是，我们可以通过使用控制台效果标记它来编写一种有效的功能，例如从屏幕读取的功能。然后，该函数的主体可以调用诸如println之类的函数，并且在调用它们的函数的签名中捕获了thees函数的调用结果。返回类型（）表示单位类型，在类C语言中称为void。

值得注意的是，标准库提供的println函数具有以下类型签名，其本身包括效果。

这样，编译器就知道了它所带来的效果，并且可以编写以下功能而无需注释，并且效果推断将推断出适当的签名，而无需用户指定。还可以使用常规类型推断技术来推断返回类型。

除了输入/输出，大多数编程中发现的最常见的效果类型是失败的能力。通常，语言运行时将使用某些异常来实现此功能，这些异常执行非本地跳转到处理该异常或展开调用堆栈并中止的逻辑。显然，这是一种可以建模的效果，我们可以创建一个类似于其他语言中已检查异常的接口。

throw函数将采用错误总和类型，并产生以exn标记的效果。虽然try函数将使用导致exn类型并返回错误的函数。错误类型可以是Error或成功执行时可以。

可以将错误处理函数编写为使用和处理带有exn效果标记的函数的高阶函数。

fun throw（err：error ）：exn afun try（action：（）-> a）：e error fun may（t：error ）：也许

例如，我们可以做经典的案例，处理mero的除法运算，然后将算术错误包装在一个可能为sum的类型中，该类型处理零的情况为空。

有趣的除法（a：int，b：int）：exn int {match（b）{0-> throw（“除以零”）; _-> return（a / b）; }}有趣的safeDiv（a：int，b：int）：也许 {也许（试试{divid（a，b）}）;}

在编译器中精心设计模式匹配可以推断出不完整的模式，并推断应该向模式匹配的类型添加一个异常，该异常可能在运行时失败。

有趣的不公正（m：也许）：exn a {match（m）{Just（x）-> x}}

有趣的unmaybe（m：可能，默认值：a）：总计{{match（m）{Just（x）-> x Nothing-> default}}

根据上面关于效果的定义，调用函数的唯一可观察到的结果就是返回结果值。因此，不计算值并无限运行的函数不是函数，并且具有称为发散的副作用。在一般情况下，确定给定功能是否为合计并非易事，但是，由逻辑单元组成的功能，这些逻辑单元全部独立地为合计，其本身就必须合计。

在许多简单的情况下，我们可以通过简单地分析呼叫站点来立即推断出非总计。例如，下面的函数会自动重复，因此会自动用div效果标记。

效果检查器可以推断出相互可重复定义之间的总数，因此相互调用的函数本身必须完全是总数，或者在组成上可能有所不同。

fun f1（）：div int {返回1 + f2（）;} fun f2（）：div int {返回2 + f1（）;}

尽管单独标记各个效果本身就很有用，但大范围编程需要我们将逻辑组合在一起，因此我们需要一种综合效果组合的方法。在Koka中，这表示为一排效果。这用方括号语法表示：

用数学的语言来说，效果行是可交换单线体，其操作扩展由管道表示，并且表示不存在效果的中性元素（总计或<>）。交换性和关联性允许对签名中的效果进行规范排序。

| e2 = | e3 = | <> = | e1 = =

例如，我们可以写下一个函数，该函数调用具有不确定性ndet的随机数生成器，并引发具有exn的异常。两者的综合现在是行。

效果系统表示可以使用以下别名将可能分散或引发异常的函数视为纯函数。

在Haskell效果方法中，有一个不透明的IO monad，它驻留在可以执行任何类型的控制台输入，输出或系统操作的任何动作中。但是，效果系统更丰富的语言可以更精细地建模IO层次结构。例如，Koka为了提高表达力，定义了以下三个IO效果层。

//执行任意IO操作的函数//但在不引发异常的情况下终止//别名io-total = > //执行任意IO操作的函数//但不引发异常io-noexn = //执行任意IO操作的函数。别名io =

状态是编程的重要组成部分，它本质上是有效的。重要的是，我们想谈一谈在给定范围内我们能够写入哪些内存或逻辑区域。为此，我们需要能够将给定内存区域上的效果称为效果的参数。该语言允许我们使用括号符号使用堆参数对效果进行参数化。标准库提供了三种核心状态效应：

fun ref（value：a）：（alloc ）ref fun set（ref：ref ，assigned：a）：（write ）（）fun（！）（ ref：ref ）： | e> a

如果未在参数类型或返回类型中引用引用的类型，则内部引用没有可观察到的泄漏的函数可以标记为总计。因此，局部状态可以嵌入到纯函数内部。例如，即使内部使用可变引用，以下函数也是合计的：

fun localState（）：总int {val z = ref（0）;设置（z，10）;设置（z，20）; return（！z）;}

编译器本身也具有一定水平的语法糖，可用于引用。 val引入了一个不可变的命名变量，但是var语法可以用来简洁地定义一个可变引用。

fun bottleOfBeer（）{var i：= 0;而{i> = 99} {println（i）i：= i + 1}}

引用可以作为函数的参数传递，堆参数可以作为类型变量量化，从而使我们能够编写可对任何类型的引用进行操作的泛型函数。

fun addRefs（a：forall ref ，b：forall ref ）：total（）{a：= 10; b：= 20； return（！a +！b）;}

读取，写入和分配功能的组合在标准库中命名为st，以表示状态计算。

使用这种效果系统跟踪参考可以为我们提供强大的抽象，用于表示具有读障碍和写障碍并以机器可检查的方式将突变与纯逻辑分离的逻辑区域。将来在编译时具有这种信息的语言可以使用它来将局部突变区域的编译通知为更有效的高效代码，同时仍然保证纯逻辑的边界。

最后，我们还希望能够编写更高阶的函数，这些函数可以接受有效或纯净的参数，并将其效果纳入输出类型的一部分。通用映射函数是一个高阶函数，它接受一个列表并将给定的函数参数应用于列表的每个元素。要使用具有效果系统的语言来编写此代码，我们需要能够将函数参数的效果引用为类型变量（在此示例中为e），并将其用作map的输出类型。

有趣的地图（xs：list ，f：（a）-> e b）：e list

如果我们在列表上应用总算术函数，则只需返回一个整数列表。在IO情况下，我们可以应用诸如println之类的函数，该函数将把每个整数单独打印到控制台，结果类型是单位列表。在抽象效果类型变量上使用此参数多态性，两个用例都由同一函数包含。

val e1 = map（[1，2，3，4]，println）; //控制台列表 val e2 = map（[1，2，3，4]，dbl）; // list fun dbl（x：int）：总计int {return（x + x）}

效果系统研究仍处于初期阶段我想推动未来工作的主要收获是，观察到旨在提高人体工程学和效果建模性能的语言不能简单地将整个系统推入库中。对于集成效果类型和表面语言中的注释，都需要语言级别的支持，以标记子表达式并提示类型推断。在Haskell，Scala等中，许多这样做的方法不可避免地会因这个简单的事实而注定了不良的人机工程学。

不仅可以通过推断类型来构建静态分析工具的全新级别，而且还可以在我们的代码之上提供全新级别的静态信息，否则这些静态信息将被编译器抛弃。这是一项非常令人兴奋的技术，我希望它在未来十年中能硕果累累。