柯里化的前生今世(十一):Pure and Lazy

语言的作用

语言可以用来交流想法,描述概念,
当前使用了什么语言,取决于我们有什么样的需要。

为了理解词法作用域,闭包,和continuation,
前文中,我们借助了Racket。

现在,为了理解代数数据类型(algebraic data type),多态(polymorphism),参数化类型(parameterized type),类型类(type class),我们要学习Haskell了。

编程也是如此,它是关于思想的,
编程语言只是描述这种思想的工具罢了。

非严格语义(non-strict semantics)

在Haskell规范中,并没有要求使用惰性求值策略(evaluation strategy),
只是规定它是一种非严格的语言(non-strict language),
具体的求值策略取决于实现。

那么,什么才能叫做non-strict呢?
non-strict与lazy有什么关系呢?
还要从数学上函数的严格性(strictness)说起。

程序中的function与数学函数之间的关系,
是指称语义中的内容。(指称语义是形式语义的一种,它将每一段代码,与一个数学对象相对应,用来研究程序的含义。

在数学上,如果一个函数对定义域中的某些参数,没有定义值,
就称为该函数为部分函数(partial function)。

程序中的function,对应着数学上的部分函数。

此外,程序中某一类型的全体值,也不能简单的对应于数学上的集合,
例如,程序中的全体整数类型的值,并不对应于整数集,
因为返回整型值的function,取某些参数时,程序可能不会终止。

为了给这样的function和返回值找到指称,
我们给每个集合增加一个新的值:,读作bottom。

f(⊥) = ⊥

一个数学函数,如果参数是,那么结果就一定是
这样的函数称为严格函数(strict function)。

反之,如果参数包含,但是结果不一定是
这样的函数就称为非严格函数(non-strict function)。

如果程序语言中function的指称语义是非严格函数,
那么这样的语言,就称为非严格的语言(non-strict language)。

注:
严格性是指称语义中的概念,而求值是操作语义中的概念。
并且指称语义对于操作语义具有可靠性(soundness),
即,如果一个表达式根据操作语义求值为另一个,那么,它们必定具有相同的指称。

因此,对于non-strict language,求值策略可能并不唯一,
对Haskell来说,GHC是最流行的编译器,
它使用了惰性求值(lazy evaluation)。

在没有歧义的情况下,人们常用lazy暗指non-strict,
lazy更直观更有利于沟通。

引用透明性

An expression is said to be referentially transparent if it can be replaced with its corresponding value without changing the program's behavior.

即,引用透明性(referential transparency)指的是,
程序中的表达式总是可以用它的值来代替。

而程序中的纯函数(pure function),指的是,
(1)这个函数对相同参数总是输出相同结果
(2)这个函数没有副作用(side effect)
因此,纯函数具有引用透明性。

此外,语言采用了惰性求值,意味着表达式的求值方式是按需确定的,
所以,依靠副作用来得到计算结果就不可行了,
我们不知道计算在什么时候发生。

因此,一旦语言拥抱了惰性求值,就不得不保证引用透明性,
反之则不一定,具有引用透明性的语言,可能不必是惰性求值的。

至于,纯函数是不是解决问题的最佳方式,目前尚无定论,
但至少它是为了追求优雅性,对通常编程方式的一种挑战。

历史上的纯函数式惰性语言

在20世纪70年代末,Gerry Sussman和Guy Steele发明了Scheme,它是Lisp的一个方言,与lambda演算很相似,并支持了词法作用域。
几乎同时,Robin Milner为了进行自动定理证明发明了ML,其中使用了多态类型系统。
但是Scheme)和ML)都是基于严格语义的语言(strict language)。

到了80年代,人们燃起了对非严格语义的(non-strict),或者说是按需求值的(call-by-need)函数式语言的研究热情。
这方面的研究理所当然的吸引了很多人,首先,函数式语言简单而优雅,其次,惰性(lazy)与引用透明性有关,并且还可以处理无穷长的数据结构(infinite data structure)。
在80年代中期,很多研究者都想设计实现一个纯函数式的(pure)惰性语言,Miranda和Lazy ML是其中的两个例子。

1987年波特兰FPCA'87会议之后,与会者想发明一种尚未命名的新语言,
其实一开始,人们想从一门现有的语言开始,逐渐发展迭代,比如说,使用当时最成熟的Miranda)。
Miranda是David Turner的公司Research Software Limited开发的一门语言,它是惰性求值的,包含代数数据类型,使用了Hindley-Milner类型系统,从1985年起用于商业中。Miranda有很好用户接口,对实现的支持良好,还有大量的教材。

可是,与David Turner沟通后,他拒绝了这件事。
我们想要一门用于研究语言特性的语言,因此我们决定任何人都可以扩展和修改语言本身,重新实现或者发行。但是David Turner想维持一份语言规范,让语言具有最好的可移植性,他不想让Miranda出现各种不同的方言。

于是,Haskell的故事就这样开始了。

参考

A History of Haskell
Non-strict semantics
Lazy Evaluation of Haskell
Foundations for Programming Languages

时间: 2024-10-31 00:50:29

柯里化的前生今世(十一):Pure and Lazy的相关文章

柯里化的前生今世(一):函数面面观

关于 本文作为开篇,介绍了出场人物,并形象化的引入了高阶函数, 得到了柯里化的概念. 后续文章,会介绍高阶函数的实现方式,词法作用域和闭包,参数化类型,类型上的柯里化, 敬请期待. 如有不同的认识,或者感兴趣的点,请直接联系我,欢迎指教. 人物介绍 球星库里 库里,Stephen Curry,1988年3月14日出生于美国俄亥俄州阿克伦(Akron, Ohio), 美国职业篮球运动员,司职控球后卫,效力于NBA金州勇士队. 斯蒂芬·库里2009年通过选秀进入NBA后一直效力于勇士队,新秀赛季入选

柯里化的前生今世(八):尾调用与CPS

关于 在上一篇中,我们介绍了continuation的概念,还介绍了Lisp中威力强大的call/cc,它提供了first-class continuation,最后我们用call/cc实现了python中的generator和yield. call/cc赋予了我们很强的表达能力,Lisp中的异常处理机制也很人性化. 例如,Common Lisp: Condition_system, 由于call/cc可以捕捉到异常处的continuation, 我们就可以手动调用这个continuation,

柯里化的前生今世(四):编译器与解释器

关于 在上一篇中,我们提到了形式语言与文法,S表达式与M表达式,同像性. 本文将开始写一个简单的解释器, 通过具体实现,我们来理解求值环境,动态作用域和静态作用域,还有闭包等概念. 当然,一篇文章来写完这些肯定是不够的,我们可以慢慢来,循序渐进. 写完了这个解释器之后,我们会增加一些新的功能. 编译器与解释器 编译器会将源代码转换成另一种语言的代码,然后在支持后一种语言的机器上执行. 而解释器则不同,它会逐行分析源代码,直接执行分析结果. 值得一提的是,编译和解释是执行代码的两种手段, 具体的语

柯里化的前生今世(九):For Great Good

关于 上文第二~八篇中,我们学习了Racket语言,它很有代表性,是一种Lisp方言. 很多概念用Racket描述会更加简便. 我们介绍了高阶函数,词法作用域,闭包以及continuation, 这些概念对理解函数式编程来说十分重要. 然而,偏见却经常起于片面. 只学习一种语言,会让我们对事物的同一个侧面产生习惯. 事实上,我们需要多样化的角度,也需要经常更换思维方式. 这对学习新知识很有帮助, 有些时候,我们理解不了某些概念,很有可能是因为这个概念被描述的不够全面, 我们经常走到深入思考这一特

柯里化的前生今世(十二):多态性

关于 本文借用Haskell介绍了自定义类型,带参数的类型,Ad-hoc多态性,kind, 其中,带参数的类型在类型上可以做"柯里化". 1. 自定义类型 Haskell中使用data自定义类型. data Bool = True | False 其中,Bool是类型名,True和False是该类型的值. 一个值可以包含多种不同类型的字段(field),例如, data BookType = BookValue Int String 其中BookType是类型名,BookValue是值

柯里化的前生今世(十):类型和类型系统

形式化方法 在计算机科学中,尤其在软件工程和硬件工程领域, 形式化方法(Formal method),是一种数学方法,用于软件和硬件系统的描述(specification).开发(development)和验证(verification).旨在能像其它工程学科一样,通过用数学进行分析,来提高设计的可靠性(reliability)和健壮性(robustness). 为了让系统表现的和规范(specification)一致,现代软件工程采用了一系列的形式化方法.其中包括一些强有力的框架,例如,霍尔逻

柯里化的前生今世(三):语言和同像性

按照故事情节的正常发展,我们这一篇该介绍Racket语言的语法了. 可是,在大局观上,我们还没有达成共识. 对于一个概念来说,我们不止要学会怎样描述它,还要学会理解它的内涵. 因此,这篇还是在打基础,俗称,引言.. 关于 在上一篇中,我们提到了Lisp语言家族,看到了关于Lisp最美丽的传说,我们提到了Racket,以及它的IDE,DrRacket. 本文将从目标语言和元语言,同像性(Homoiconicity),引用等这些角度来深入的讨论Lisp, 浅尝辄止,毕竟不是一个好习惯. 目标语言和元

柯里化的前生今世(十三):WHNF

1. 形式系统(Formal system) 在逻辑学与数学中,一个形式系统由两部分组成,一个形式语言加上一套推理规则. 一个形式系统也许是纯粹抽象地制定出来的,只是为了研究其自身. 也可能是为了描述真实现象或客观事实而设计的. 2. λ演算(λ-caculus) λ演算用于研究函数定义.函数应用和递归,它是一些形式系统的总称, 配备不同的推理规则集,就会得到不同的演算系统. λ演算由Alonzo Church和Stephen Cole Kleene在20世纪三十年代引入, Church在193

柯里化的前生今世(六):词法作用域和闭包

关于 在上一篇中,我们介绍了动态作用域,并进行了相关名词的解释. 我们解释了什么是环境,什么是帧,如何在一个环境中对表达式求值. 我们用一个内部结构表示了函数,实现了一个微型的支持动态作用域的解释器. 这一篇,我们将再往前一步,实现词法作用域(lexical scope). 动态作用域 vs 词法作用域 作用域(scope)的概念大家可能比较陌生, 但是闭包(closure)的概念在这几年非常流行,几乎已经没有什么主流语言不支持它了. 从实现角度,和函数一样我们将用另外一种内部结构表示闭包, ;