Haskell

原文标题：Safe and Efficient, Now 作者：Oleg Kiselyov 原文地址：Lightweight Static Guarantees 本文确立了一种严谨的编程风格（事实上，十多年前就有人确立过）。这一风格通过利用成熟的、实用的语言（如 OCaml、Scala、Haskell 等，某种程度上 Java 和 C++ 也可纳入这一范畴）中的现有类型系统，从而静态地保障一系列广泛的安全性质。 永远不会对空指针解引用，或取空列表的头部元素。 始终对用户提供的输入进行消毒。 只使用数组界内的索引值访问（动态分配的）数组，且数组大小不需要静态可知。 这一技术与模块化开发、分离编译、命令式编程、原生的可变数组、间接索引以及一般递归等编程语言特性兼容。使用这种技术编写的程序所需的运行时检查更少，因此不但更可靠，而且更高效。这一技术并非旨在取代基础的代码形式化验证方法，而是补充并结构化了这种方法：我们可以用形式化方法证明（小而简单的）安全内核的正确性，然后用这一技术将安全内核的静态保障从内核扩展到整个程序。 在研究的过程中，我们发现有两个点令人惊讶：首先，我们上面所列举的内容居然是可行的；其次，这些技术是如此古老（可追溯到 Morris 1973 年的论文），如此简单，但却鲜为人知。 导言 OpenSSL 的心血［Heartbleed］漏洞给人们带来的惨痛回忆已逐渐淡去——毕竟，可被利用的安全漏洞常常都有。但心血漏洞仍然令人瞩目，因为漏洞本身是如此的微不足道，人们却花费了大量精力来修复它的影响。 与许多其他的此类性质的漏洞一样，心血漏洞的出现并未经过太多的酝酿——正如 SSL 的心跳［heartbeat］功能开发者所解释：「我当时正在改进 OpenSSL，提交了大量的漏洞修复，并添加了一些新功能。不幸的是，在其中一个新功能中，我漏了验证某带长度的变量的长度。」而 OpenSSL 的代码审核——「显然也没有注意到这一遗漏。」这位开发者又补充道：「因此这个漏洞从开发分支进入了发布版本。」最终在发布版本中潜藏了两年，一直未被（公开）发现。 最终修复这一漏洞的 OpenSSL 补丁证明：这一漏洞本身确实微不足道，不过是一条语句 memcpy(bp, pl, payload); 这条语句从输入数据包（自指针 pl 开始）中拷贝 payload 大小的数据载荷，然后将拷贝出来的内容放入输出数据包缓冲（自指针 bp 开始）。payload 值是从之前的输入数据包中读取的，当恶意攻击者发送的数据包声明它的载荷量是最大有效值，但实际却没有携带任何数据载荷时，问题就来了：在这种情况下 memcpy 没法从接受到的数据包中拷贝（因为已经结束），反而是从 OpenSSL 输入缓冲区的剩余垃圾中拷贝数据。这些「垃圾」实际上是之前剩余的数据，通常包含密码等敏感信息。 另一个令人不安的点在于：如果禁止程序员直接使用 memcpy 这样的低级函数，而是强制其通过一些封装（例如强制检查 pl + payload 地址是否仍在输入数据包内）来调用，像心血漏洞这样的问题本来很容易避免（因为输入数据包的边界很容易获得）。这种调用限制可以在任何具有模块［module］或命名空间［namespace］抽象机制的语言（C++ 等）中实现，甚至也可以在 C 语言中实现： 「抽象」就是关键所在：通过对内部数据和函数的抽象，迫使程序员使用带有安全检查的公开 API。抽象还能通过「避免外部程序污染内部状态」，从而确保一些已经通过安全检查验证的不变式［invariant］在任何情况下都成立——这样，就不必反复地进行某些安全检查了，甚至可以完全不需要检查。因此我们的口号是：「安全和高效，我全都要。」 这编程风格背后的思想其实稀松平常，甚至可以追溯到计算机的洪荒年代：由硬件保障的内存和设备的访问限制。硬件保护层将计算系统分为（受信任的）内核（在特权模式下运行，可执行底层操作）和用户态［user-level］程序，后者只能通过内核公开的 API（系统调用）访问设备，而内核 API（系统调用）会检查正确性和访问权限。譬如，用户态程序不能随意写入磁盘，它们只能执行 open 系统调用；在经过权限和一系列检查后，系统调用返回一个不透明的标记，即文件描述符［file descriptor］。这一描述符代表了「执行规定的的操作的能力［capability］」，还代表了一种「授权成功」的事实，在进一步的操作中就无需重复验证授权。Jame Morris 1973 年发表的论文 «Protection in Programming Language» 首次将操作系统中的部分理念应用到软件开发中，这些理念包括内存保护、身份验证、整理、作用域控制等等。该论文还展示了软件/语言的保护层是如何帮助我们对程序进行本地化、模块化的推理。而自 1973 年以来，编程语言中的抽象设施变得更加广泛和普及，现在是时候充分利用 Morris 的这一洞见了。...

原文标题：Higher-kinded bounded polymorphism 作者：Oleg Kiselyov 原文链接：Higher-kinded Bounded Polymorphism 为了表达数据集合上的泛型操作，或嵌入有类型的 DSL（尤其是在 tagless-final 方法中），经常需要对类型构造器［type constructor］进行抽象，然后在之后才为类型构造器提供参数。通常情况下，被抽象的类型构造函数不是任意的，而必须是实现了特定的接口（比如抽象序列）——这就是所谓有界多态［bounded polymorphism］。 OCaml 并不直接支持高种类多态［High-Kinded Polymorphism］：OCaml 的类型变量只能包含类型，不能包含类型构造函数；如果不给类型构造函数应用正确数量的参数，它就无法出现在类型表达式中。尽管如此，OCaml 还是可以表达高种类多态的——事实上，有几种或多或少比较麻烦的方式，其中的不那么麻烦的方式尤其鲜为人知，却又不断被重新发现。本文总结了表达（有些时候，是避免）高种类多态的不同方法。这些方法收集自多年以来的学术论文和 Caml-list 邮件列表上的信息，并根据文章的需要进行了调整和重新解释。 导言 Polymorphism abstracts types, just as functions abstract values. Higher-kinded polymorphism takes things a step further, abstracting both types and types constructors, just as higher-order functions abstract both first-order values and functions. 译：多态是类型的抽象，正如函数是值的抽象。而高种类多态则更进一步，它同时抽象了类型和类型构造函数——正如同高阶函数同时抽象了一阶值和函数。——Yallop 与 White（FLOPS 2014） 我们将进一步阐述这一非常精炼的总结，从而说明（有界的）高种类多态是如何产生的。这里介绍的例子将贯穿全文所有章节。 在实践中，经常会出现「对某些数字求和」的情况，对具体的数字类型进行抽象，就可以得到能在任意一个数字集合（列表）上执行的函数： let rec sumi : int list -> int = function [] -> 0 | h :: t -> h + sumi t 我们可以进一步抽象 0 和 + 运算，由于它们本身就是函数（也可以说是一个带参数的值），结果就会得到一个高阶函数：...

译自 Having an Effect。除非特殊说明，下文中的『我』指原文作者 Oleg Kiselyov。 简介 本研究如同一次追寻表象之下草蛇灰线的旅程：Monad，Monad Transformer，Free Monad 以及可扩展副作用（Extensible Effects）的创始论文本质上都是关于所谓『可扩展解释器』问题的研究。一路走来，我们意识到表达式问题（expression problem），稳定指称问题，以及可扩展解释器问题都是同一事物的别称。最终我们找到了组织原则：交互－－客户端与服务器之间的交互、解释器与被解释代码之间的交互、表达式与其上下文之间的交互。 可能用『进程演算（process calculus）』能更好描述交互。而在各种序贯式的演算中，最早的把计算副作用视为交互，并且做出形式化表述的工作则是 Cartwright 与 Felleisen 发表的著作《Extensible Denotation Language Specifications》。 本文用现代的方法重构了 Cartwright 与 Felleisen 方法。得益于 tagless-final 形式，我们重构后的版本更简单，可以直接给计算机运行。 本文也在前人的工作之上做了进一步发展。本文令副作用处理程序变得模块化且可扩展－－它变成程序的一部分，而非永久独立于程序之外。这使得下面的做法成为可能。 尽管整数和一般的一阶子语言不需要变量和环境，Cartwright 与 Felleisen 的方法也必须将变量和环境融入基本语义框架；我们避免特殊对待可变环境和任意高阶编程特性，而是将 Lambda 与 State 一视同仁。动态绑定和词法绑定，以及各种调用约定（按值调用，按需求调用，按名调用）可以视为用不同方式解释副作用『解引用绑定变量』。 对研究领域溯本求源，寻回直达本质的洞见，发掘其沧海遗珠。这一探索过程有助于为我们为程序重新发明副作用。 本演讲稿于 2016 年 8 月 25 日在印第安纳大学信息与计算学院 (SoIC) 计算机科学研讨会上首次发表。我要感谢 Martin Berger 与我进行了许多令人受益匪浅的讨论，特别是解释了进程演算的起源。此外还要感谢穆信成与 Matthias Felleisen 提出的宝贵意见。 版本 当前版本为 2017 年 9 月版 引用资料 EDSLNG.hs 本文所使用的 Haskell 98 代码的完整版 edlsng.ml Cartwright-Felleisen 框架现代重构 OCaml 版本。附带全局状态、动态绑定、按值调用和按需求调 用的词法绑定示例...

译自：Type inference and the undead code。除非特殊声明，下文『我』指原文作者 Oleg Kiselyov。 类型推导算法通常依赖于代码上下文，因而不具有组合性。Hindley-Milner 风格的类型推导的设计中，明确允许了『蒐集类型约束并求解』的过程中上下文影响/确定表达式（如变量）的类型。不过，类型推导算法的非组合性质有时也会给人们带来『惊喜』。例如，类型良好的『明显死代码』会影响整片代码的可赋类型性（typeability），甚至会影响其运行结果。本文的写作动机源于我与 Andreas Abel 自 2012 年 7 月始在 Haskell Cafe 邮件列表的进行的一系列讨论，他希望把讨论期间提出的各种示例记录下来。本文就是为了完成这一愿望－－收集，扩展和完善这些示例并建立它们内在的联系。 『死代码』通常指没有数据流和控制流流过的表达式。本文使用该术语专门表示无关的变量定义：即类型良好且无副作用，也没有数据流和控制流流过的变量定义，这些定义的标识符甚至不能出现在相关的表达式中。 首先从最简单，最广为人知的例子开始。在例子中，无关的定义导致了表达式无法被赋予类型。读者肯定在任何使用 Hindley-Milner 风格的类型推导的语言中都见过这样的例子。下面用 OCaml 的一个简单子集具体展示： let exp = let id = fun u -> u in let f = id id in let z = fun () -> f true in f 1 这段代码无法通过类型检查，检查器报告表达式 f 1 的类型错误。但是，如果我们删除 z 的定义（f 1 中显然没有出现 z），修改后的程序突然就变成类型良好的了。 练习：是否存在其他合法（从动态语义的角度）的代码转换能使 exp 的类型正确？ 在 Haskell 98 及以上版本中，类似的问题常常与臭名昭著的 MonomorphismRestriction 相关：...

译自 Free and Freer Monads: Put Monad Back into Closet 简介 编写 Monad（现在还包括 Applicative 和 Functor）的实例，并确保实例符合 Monad 定律不但是定义 Monad 的重要部分，同时也是数量正在以指数级膨胀的「Monad 教程」的重要部分。而本文认为所有这些实例都不过是 boilerplate－－可以避免的 boilerplate！或许是因为听起来像拉丁语的名字和其引起的人们对顶尖数学的兴趣，这些琐碎的 boilerplate，琐碎的 Monad 定律，毫无新意的「管道」吸引了过多的关注。如果我们能直接思考副作用本身而非这些管道的工作原理，难道不让人耳目一新吗？ Free Monad，以及我们正要提到的 Freer Monad 将把我们从 boilerplate 中解放出来，从而专注于副作用的本质。有了它，我们就可以将解释器这一在编程语言研究和实践中的大杀器引入到副作用编程中－－为副作用定义解释器。 目前，已经有了许多关于 Free Monad 的精彩解释，这些解释往往援引了幺半群、普适代数和范畴论的观点。但最近流行的 Freer Monad 却给我们带来了困境：它的定位是什么？它能让我们更清晰地思考副作用吗？它也是『自由』的吗？如果是，为什么这些数学上的解释都没有预言 Freer Monad 的存在呢？本文接下来将解决这些问题，但唯独最后一个问题，我只能说，人们几次发现 Free Monad 都不是通过范畴论。（事后来看，范畴论上的联系确实存在，而且确实有洞见性）。与许多已有的解释不同，本文采取了通俗的方法，通过具体的例子而非抽象的代数解释 Free Monad（有关范畴论的内容将仅在括号中提及）。 经典 Monad 我们用耳熟能详的 State Monad 举例，该 Monad 代表『访问或更新一个可变状态』的副作用。常见的实现将这个可变状态作为返回值和参数沿着程序传递，然后通过 get 和 put 两个原语来获取/更新变量。 newtype State s a = State{unState :: s -> (a,s)} get :: State s s get = State $ \s -> (s,s) put :: s -> State s () put s = State $ \_ -> ((),s) runState :: State s a -> s -> (a,s) runState = unState get 和 put 操作，State s 蕴涵的定律以及解释器 runState，没有这三者，State s 就不能够作为真正的可变状态副作用计算使用。然而，为了在 Haskell 程序中方便地使用这些操作，我们要编写以下代码。...

大多数情况下，effect都是用Hoare逻辑来描述的。一个Hoare三元组$\{p\}\;S\;\{q\} $， $S$ 是一段程序， $p $ 是执行这段程序的前提条件（状态）， $q$ 是执行完这段程序后的条件（状态）。然后使用这个三元组的一些规则表示语句的一些性质： 空语句： $\frac {} {\{p\}\;skip\;\{p\}}$ 赋值语句： $\frac {} {\{p[u :=t]\}\;u:=t\;\{p\}}$ 顺序语句： $\frac {\{p\}\;S_1\;\{q\}, \{q\}\;S_2\;\{r\}} {\{p\}\;S_1;\,S_2\;\{r\}}$ 等等。这其实恰好是个幺半群——空语句是幺元，顺序语句是乘法。总之，用幺半群来描述作用（语句）是十分合适的。 于是用Monad来描述作用也是很自然的——Monad是自函子范畴上的幺半群。（这句话我就不解释了） 比如用m a表示带作用类型为m的程序，而m (m (m ... m a))表示一系列的作用，对应作用（语句）序列 $S_1, S_2, S_3, S_4 \dots S_n$ ： stms :: Monad m => m (m (m (m ... m a))) -- ^ ^ ^ ^ ^ -- | | | | ... | -- S1 S2 S3 S4... Sn stms = ....

Relens to Lens 之前也写过一篇lens的文章，学了新知识之后，现在看起来觉得不满意，于是打算重新再写一篇。 脚趾头：First Lens to Lenses Lens的设计十分的精妙，是数学指导编程的一个非常典型的案例。 Lens要解决的问题 在Haskell中，只提供了模式匹配的语法来操作数据，操作深层的是一个非常麻烦的事情。比如我们要操作以下数据： data Point = Point { positionX :: Double , positionY :: Double } deriving (Show, Eq) data Segment = Segment { segmentStart :: Point , segmentEnd :: Point } deriving (Show, Eq) p1 = Point 1 2 p2 = Point 3 4 l1 = Segment p1 p2 我们要修改l1的第二个端点的横坐标： l1 {segmentEnd = (segmentEnd l1) {positionX = 10}} -- 如果没有部分修改record的语法，这样的工作会更麻烦，只能用模式匹配一项项填 如果数据结构更加复杂的时候，代码就会变得更冗长。但如果用lens，刚刚的表达式就可以重写为：...

前言 Haskell中有一个很强大的库，叫做Lens。 在Haskell中，只提供了「模式匹配」的语法来访问/修改数据结构。于是处理深层的数据就成为了老大难的问题。 比如在这样的数据结构里： data Point = Point { positionX :: Double , positionY :: Double } deriving (Show, Eq) data Segment = Segment { segmentStart :: Point , segmentEnd :: Point } deriving (Show, Eq) p1 = Point 1 2 p2 = Point 3 4 l1 = Segment p1 p2 我们要修改l1的第二个端点的横坐标： l1 {segmentEnd = (segmentEnd l1) {positionX = 10}} 如果数据结构更加复杂的时候，代码就会变得更冗长。 这时候Lens库就出场了,刚刚那段代码等价于： l1 & endLens . xLens .~ 10 其中endLens ....

本人有个小小的习惯，就是在学习一门语言的开始，为了熟悉这门语言的基础设施，我都会写一个最最简单的parserc（当然那些9012年都没有支持泛型的语言，就不写了）。 这次就试着用Rust来写一个。 从Iterator中来 用过Rust的Iterator的人，一定会觉得这用起来十分的愉悦，这说明Iterator设计得很不错。而parserc的使用方式其实和使用Rust的Iterator的方式十分相似的——先将小的组合子构造成大的组合子，然后再使用，parserc是.parse()，Iterator是.next()。 所以借鉴一下Iterator的思路，Rust版parserc也试着由这几部分构成： parser的trait 一些adapter 自定义一些combinator 组合出来的一些combinator 用起来大概是这样： // a+(b|c) fn aaab_c() -> impl Parser<Target=()> { char('a').some() .and(char('b').or(char('c'))) .map(|_| ()) } fn main() { let mut src = ParseState::new("aaab"); let res = aaab_c().parse(&mut src); assert_eq!(res, Some(())); } Parser trait 先定义parser的一般行为parse，“照搬”Iterator的结构。 #[derive(Clone, Debug)] pub struct ParseState<'a> { src: Chars<'a>, pub col: usize, pub row: usize, } pub trait Parser { type Target; fn parse<'a>(&self, state: &mut ParseState<'a>) -> Option<Self::Target>; } 在Haskell中，最简单的parse function的类型是String -> Maybe (a, String)：吞进去一个String，得到解析结果a，还有未匹配的字符串，或者没有结果，也就是匹配失败。这里也采用了类似的结构，有所不同的是，因为Rust是有mut的，可以直接改变状态，于是可以去掉用返回值表示的状态，改为可变引用；然后，parse的状态加上了行和列，为了方便，用字符迭代器表示要解析的字符串。...

函数式的动态规划 动态规划是一类很常用的算法，在C/C++/Java中一般使用于数组进行记忆化。而函数式编程语言一般无法方便地操作数组这些依赖副作用的数据结构，函数式的记忆化便要另寻他法。 本文就是一个简单的笔记，用一些代码片段展示我所知的函数式动态规划的技巧。 （2020/5/17，时隔五个月后的更新，新增Memocombinators） Course-of-Values Recursion Course-of-Values Recursion是我认为最直观的一种技巧，就是将遍历过的结果当作返回值的一部分保留下来，在递归的时候可以取得运算过的值。 对于递归函数f，定义一个辅助的函数bar $\begin{align} \overline{f}(n) = [f(n), f(n-1),...,f(0)] \end{align}$ 则原递归函数f可以用bar表示出来： $head(\overline{f}(n))$ 斐波那契数列： fibBar :: Int -> [Int] fibBar 0 = [0] fibBar 1 = 1:fibBar 0 fibBar n = let course = fibBar (n-1) in -- [fib(n-1)..fib(0)] let p = course !! 0 in -- fib(n-1) let pp = course !! 1 in -- fib(n-2) p + pp : course -- >>> fibBar 10 -- [55,34,21,13,8,5,3,2,1,1,0] -- Binary Partitions：...