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

关于

本文作为开篇,介绍了出场人物,并形象化的引入了高阶函数,
得到了柯里化的概念。

后续文章,会介绍高阶函数的实现方式,词法作用域和闭包,参数化类型,类型上的柯里化,
敬请期待。
如有不同的认识,或者感兴趣的点,请直接联系我,欢迎指教。

人物介绍

球星库里


库里,Stephen Curry,1988年3月14日出生于美国俄亥俄州阿克伦(Akron, Ohio),
美国职业篮球运动员,司职控球后卫,效力于NBA金州勇士队。

斯蒂芬·库里2009年通过选秀进入NBA后一直效力于勇士队,新秀赛季入选最佳新秀第一阵容;
2014-15赛季随勇士队获得NBA总冠军;
两次当选常规赛MVP,两次入选最佳阵容第一阵容,三次入选全明星赛西部首发阵容。

Haskell Curry


这次我们说的不是NBA的库里,而是美国著名的数学家,逻辑学家Haskell Curry,它在组合子逻辑方面有杰出贡献。
Curry本科就读于哈佛大学医学专业,业余选修了数学,1917年转到了数学系。
毕业后,在通用电气找到了一份电气工程师工作,继续在麻省理工进修电气工程,但意识到自己更适合做理论研究,而非应用科学。
1922年转专业到了物理学,但物理学哈佛会更好些,于是作为助教回到了哈佛,1924年拿到了物理硕士学位。
随后,在哈佛攻读数学博士学位。

1924年,他最开始的研究方向是微分方程理论,与此同时他接触了一些逻辑学。
阅读了罗素和怀特海的《数学原理》之后,他产生了使用组合子来分析代换规则的设想。
于是,放弃了微分方程的研究,准备撰写一篇逻辑方面的博士论文。
1929年,他的第一篇论文《逻辑代换的分析》在《美国数学报》发表。

之后,Curry在宾夕法尼亚大学担任教员直至1966年退休,期间曾担任国家研究委员,普林斯顿的高级学会会员。
发表的论文包括,《组合子逻辑的全称量词》《组合子理论的补遗》《显式变量的组合逻辑观点》《组合逻辑中相等性及推导的几个性质》。
1942年,Curry作为符号逻辑学会会长,发表了离职演说《数理逻辑的组合子基础》。
Curry阐明了组合子逻辑与Chruch的lambda演算之间的密切联系,
建立了一套类似于Church和Rosser的完备系统。

第二次世界大战期间,Curry又开始研究应用数学,1943年发表了《Heaviside演算》。
1946年,Curry在应用物理实验室工作后,去了阿伯丁实验场,发布了《使用ENIAC的逆向插值法研究》和《使用ENIAC的四阶插值法研究》。

主要著作有,《组合逻辑》和《数理逻辑基础》。
注:这里说的这么仔细,是有原因的。组合子逻辑和lambda演算 ,我们多多少少也会提到。

柯里化

名字的由来

以下是维基百科关于Currying的定义:
In mathematics and computer science, currying is the technique of translating the evaluation of a function that takes multiple arguments (or a tuple of arguments) into evaluating a sequence of functions, each with a single argument.

Currying这个概念,首先是由Gottlob Frege引入的,以逻辑学家Haskell Curry命名。
虽然,这个概念是Moses Schönfinkel发明的。

表达式的值和类型


为了说明Currying我们先引入类型的概念。
我们知道编程语言中的表达式是有值的,我们常说,表达式的值为1,值为'a'
他们在内存中的存储方式是一样的,都是二进制方式。

但是,感觉上,他们应该是不同的东西,于是,我们用不同的类型加以区分。
我们称值1的类型是Int,整型,
'a'的类型是Char,字符型。

于是,我们就在值的概念上建立了一层抽象,不同的值因此有了不同的属性。
用数学语言来说,类型作为值集上的一种等价关系,诱导出了对该值集的一种划分,
相同类型的值构成了一个等价类。
注:我们后面将会看到函数类型的引入,让事情变得不是这么简单了。

函数面面观

函数用来将一个或多个值变成另一个值,函数也是一种值,它同样具有类型。
例如,加法函数add是把两个整型值变成一个整型值,假如我们已经定义好了add函数,我们可以这样调用它。

注:我们这里使用的编程语言,函数调用是不用加括号的,具有最高优先级。add 1 2类似于add(1,2)

add 1 2
= 3

现在我们考虑一个问题,如果我们只给add提供一个参数,结果是什么呢?
即,add 1是什么?

我们可以形象化的这样考虑,先考虑add
add就像一台有两个插槽的机器,
如果两个插槽分别提供了12,那么它会弹出结果3

问,如果只有一个插槽提供了1,那它是什么?
很显然,它还是一台机器,只不过只有一个插槽罢了。
因此,add 1还是一个函数,只不过它只接受一个参数罢了,
它返回参数值加1的结果,它的类型我们可以记为,

add 1 :: Int -> Int

我们再回过头来考虑add的类型,我们看到,
add接受1作为参数,返回add 1这个函数。
因此,我们对add就有另外一种看法了,
它是一台有一个插槽的机器,接受参数1后,
弹出的结果是另一台有一个插槽的机器add 1

因此add的类型我们可以记为,

add :: Int -> (Int -> Int)

为了书写方便,我们假定->具有右结合律,因此,

add :: Int -> Int -> Int

高阶函数

事实上,Currying指的是这样的一个高阶函数,

curry :: ((a, b) -> c) -> (a -> b -> c)

它把函数f变成函数g

f :: ((a, b) -> c)
g :: a -> b -> c

g = curry f
f = uncurry g

使得任意的x,y,满足,

f (x, y) = g x y

注:
这里curry函数的定义用到了“类型参量”,涉及到多态性,
详见柯里化的前生今世(十二):多态性

参考

柯里生平
Haskell Curry
Currying
Currying - HaskellWiki

时间: 2024-10-13 15:46:14

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

柯里化的前生今世(八):尾调用与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)一致,现代软件工程采用了一系列的形式化方法.其中包括一些强有力的框架,例如,霍尔逻

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

语言的作用 语言可以用来交流想法,描述概念, 当前使用了什么语言,取决于我们有什么样的需要. 为了理解词法作用域,闭包,和continuation, 前文中,我们借助了Racket. 现在,为了理解代数数据类型(algebraic data type),多态(polymorphism),参数化类型(parameterized type),类型类(type class),我们要学习Haskell了. 编程也是如此,它是关于思想的, 编程语言只是描述这种思想的工具罢了. 非严格语义(non-stri

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

按照故事情节的正常发展,我们这一篇该介绍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)的概念在这几年非常流行,几乎已经没有什么主流语言不支持它了. 从实现角度,和函数一样我们将用另外一种内部结构表示闭包, ;