区块链与函数式编程｜特约专家推文

Posted 2021-04-12 每日币经

前言：

作者简介

yihuang：每日币经特约专家，前腾讯区块链专家，在游戏领域有多年一线开发经验，拥有自己个人专属的区块链游戏引擎，可在移动设备上实现源生APP，H5,3D落地。

---

正文：

区块链是对软件正确性要求极高的领域。过去软件bug和安全漏洞带来的损失，一般就是停机维护，被拖个库就已经是很重大的影响了。而区块链软件的漏洞被利用，那将是灾难性的，因为上面跑的都是真金白银。随着区块链技术对传统经济领域渗透的加深，这种风险将会大大提升。

传统软件工程只重视产品的快速上线快速迭代，从来没有把软件的正确性摆在一个优先级很高的位置，究其根本还是传统领域软件出bug带来的成本不高。

行业里其实已经有一些关键领域是对软件的正确性要求极高的，比如航天系统，金融领域一些核心系统等。1962年软件bug造成火箭偏航，损失1850万美元；1978年CAD软件bug造成体育竞技场倒塌，损失上亿美元；1985年放射机软件bug导致病人受到大量辐射，1987年金融交易软件bug导致美国股灾，等等。

这些问题促使人们去思考如何保证软件正确性，而这些年来业界针对这种对软件正确性要求高的领域，也确实发展了一套技术手段来支持，形式验证、类型系统、纯函数式编程等。这些方法对程序员要求更高，开发时间也更长，所以在大部分编程领域，这种方法显得不是那么经济，换句话说大部分程序员其实并不了解这个领域的技术。而现在传统程序员开始进入区块链软件的开发，如果不能在思维、流程、工具各方面作出相应调整的话，是很危险的事情。

但是真正的形式验证成本巨大，只好用来解决一些最核心的问题。而另一种同时兼顾实用性的方案是函数式编程（函数式编程这个词语这些年有些定义模糊，这里特指静态类型纯函数式语言，基本上就是ML一族的语言），而Haskell是其中的佼佼者，也是Cardano项目使用的开发语言。

    

Haskell是一门 纯函数式 静态类型 惰性求值的语言，这里关键字有几个：

• 纯函数式是说，函数除了将输入转换为输出以外，不能有其他副作用（比如执行IO操作、修改全局变量、或者发射个导弹啥的），并且对于相同的输入永远返回相同的输出。这意味着不存在变量的概念，数据结构也都是immutable的。显然这样的函数会有很多良好的性质：好测试, 线程安全, 代码可重用, 可读性强等等。另外这样的代码还有一个性质是可证明，因为你可以机械地把函数的调用替代成函数的实现，而不改变其语意，所以你可以形式地证明比如说两个函数等价。还有一些其他的好处，比如一些代码重构工具能够自动调整代码，编译器也可以更激进地对代码进行优化，因为他们能够确保对程序的语意没有影响。

如果在*纯*的基础上，再加上total的约束，那就更好了，total是说函数对参数的所有取值都有定义，相对应的partial的函数可能对某些输入没有定义。 不过有点遗憾的是，函数是否total无法静态地检测出来，因为从程序语意的角度，未定义和死循环是一样的，所以检测total性和停机问题是一样的。 （但是如果我们愿意牺牲图灵完备性的话，是可以支持total检查的，这样的语言里可以没有死循环和partial函数， 智能合约语言就非常需要这样的设计，而Cardano的智能合约语言Plutus正是这么设计的）

• 静态类型系统，按照“柯里-霍华德同构”定理，类型对应于命题，而程序对应于证明。当我们把问题的模型编码成类型后，编译器通过类型检查可以保证程序的正确性。在实践中，类型是可以逐步细化的，越细化，能够通过编译的实现就越少，甚至可能细化到只剩下一个有意义的实现，这种情况下甚至可以通过工具实现自动生成实现代码。类型系统还带来其他一些便利的工具，比如hoogle，可以根据类型签名搜索现有库提供的函数实现。

关于Haskell语言其实可以说的还有很多，未来会继续写一些具体的编程模式，尤其是与区块链相关的，以及它在Cardano项目中的具体实践，敬请期待。

【声明：原创文章，已获作者本人授权，转载请联系我们】

http://dwz.cn/7zdgWZ

（知乎APP内搜索“函数式编程与区块链”）

【每日币经】

作为币圈内少有的保持中立的自媒体，每日币经欢迎大家投稿；

投稿方式参见文章：

投稿文章和意见，一定要原创，不得抄袭，文章长度不限，100字以上即可；

若您的投稿达到一定的阅读量，我们会发送奖励，直接点的就是微信红包，表现突出的，直接给以太坊ETH或者比特币了；

我们是欢迎大家各抒己见的，只要不违背法律、法规的，都可以。

往期精彩文章链接：

扫码申请加入每日币经资讯交流2群