2020中文学生开源年会压轴讲者专访：ICE1000/千里冰封

2020中文学生开源年会压轴讲者专访：ICE1000/千里冰封

2020中文学生开源年会将于10月18日上午九点于bilibili 22566724直播间开启直播，在本次活动之前，开源年会组委会特别推出讲者系列专访：从即日起至10月18日，我们将为每位讲者推出一篇独家专访。

本次专访为此次2020中文学生开源年会系列专访唯一的线下专访，受访者千里冰封/ICE1000（以下以“冰冰”简称）不仅带来了这期质量极高的访谈，同时也作为一位“成都土著”，带领笔者游览了许多成都市中心鲜为人知的好去处。

与冰冰见面是在通惠门地铁站，笔者的第一感觉是：大佬的头像确实是素颜出镜（笑）。

冰冰带领笔者去了一家冒菜馆子。他透露，这馆子的老板与他是老熟人，老板曾见证过冰冰见过的四位网友，笔者是老板所见证的第五位。这个馆子的味道也的确上乘，冰冰介绍的几种冒菜料十分美味，为笔者开启了新世界。

饭后，我们穿过宽窄巷子、穿过人民公园、穿过昏黄的灯光，来到泡桐树街，成都不为人知的一面展现在笔者的眼前。我们在一家酒吧开始了采访，席间，冰冰授权我们为他拍下了几张照片，留作纪念。

专访，正式开始。

Q1: 感谢您能抽空接受我们的采访，请问您能先做一个自我介绍吗？

ICE1000：OK，我是最老的那一届00后，是个水货，写过一些微不足道的代码，做过一些微小的贡献。在技术方面，我对复杂编程语言的类型系统的实现和设计以及各种编程工具链，包括IDE的开发非常感兴趣。

Q2:请问“千里冰封/ICE1000”这个ID是从何而来呢？

ICE1000：“千里冰封”这个名字的来源是很早很早的事情，是小学的时候看到赛尔号的一个服务器的名字叫千里冰封，我个人很喜欢这个名字，于是就把它变成了我的全网ID；但在某些只支持英文字符的网站上这个ID是不可用的，于是我就想整一个翻译；但这个词组无论怎么翻译都是一个非常长的词组，这不利于我功成名就之后让别人记住我的名字，ICE1000就是这么被翻译出来并使用至今的。后来我给自己起了个更像人名的网名，Tesla Ice Zhang。原因是我非常喜欢Nikola Tesla这位科学家，同时也有很多人喜欢叫我ICE，冰冰等等，这个身份和我的三次元身份强相关了，ICE便成为了这个ID的中间名了。

Q3: 请问能向我们简要地介绍一下您的演讲的内容吗？

ICE1000：​我的研究方向是编程语言，其中我比较感兴趣的方向是复杂的类型系统，但这次我可能不会去讲复杂的类型系统，因为这样面向的群体实在太小了；而简单的类型系统也有许多可讲之处，尤其是Java系语言的类型系统与Haskell系语言的类型系统，这两者是有着比较结构化的区别的。这些东西可以辅助你从一个更meta(元)的角度看待编程语言与编程这件事本身。另外一个方向就是设计模式，但这个东西被误解的很厉害，所以这次我想从我自己的角度讲讲。我一直抱有这样的一个观念：每一种设计模式都有一个相对应的语言特性。例如Java这种语言特性很少的语言，它的设计模式就会相对比较多；而特性比较多的语言则会把一些设计模式做成语言特性。编程语言要么做得很简单，将编写设计模式的权限留给用户；要么做得很复杂，将设计模式做成语言特性。但无论怎样，设计者无法阻止用户来手写设计模式，当语言特性不满足用户的需求的时候，用户又会回到之前原始的方式去手写设计模式。

Q4: 目前有相当一部分人认为用上设计模式之后代码会变得复杂与冗余，但是也有原教旨主义者觉得什么都应该用设计模式，请问您如何看待这个问题的呢？

ICE1000：对于前一种观点，我个人感觉不是这么一回事。首先，IDE可以帮助用户建立设计模式的模型，将所有成员变量都建立好；但是也会有人认为自动写起来方便，读起来却很麻烦。在我看来，设计模式的代码其实都是一个模子里刻出来的，一个几百行的文件，有的时候读到前三行你就能知道代码的全貌。这意味着如果作者严格遵循设计模式，不仅能够提升代码的可读性，还能够降低整个代码的维护成本。对于后一种观点，我们可以站在类型系统的角度来解释。这个问题能够通过不同的类型系统来解决：不同的类型系统下会拥有不同的设计模式，在我看来设计模式就是就是你想完成一件事，然后把代码写成一个特定的格式，这是一个感性的定义。比如说异常在一般语言中是语言特性，但是在Haskell和Rust中没有这个语言特性，它们都是用库完成的。设计模式我个人感觉都可以是在学编程时自己发现的，因为有的设计模式实在是太简单了，以至于Haskell社区许多时候都不把这些东西叫做设计模式，而是单独使用名字来称呼他们，比如 Profunctor Lens, Tagless Final, MTL, Extensible Effects还有 Agda 那边的totally free等。有一些复杂的设计模式可能难以自行发明，这时候可能才就需要去学习这些前人总结的设计模式。

Q5: 请问您研究类型系统的的契机是什么呢？

ICE1000：本来只是想研究类型系统能够强大到什么程度，然后发现前沿的类型系统确实牛逼，“但是类型系统它牛逼到一定程度之后就没啥实际用途了”后来我了解到类型系统的应用场景是有限的，所以我就放弃了“有用”，去研究没用但是好玩的类型系统了，尤其是那些对推导不友好，但是本身更强大的类型系统，也就是dependent type。然后我了解到这个理论也可以用于做形式化验证，于是我就天天在网上吹形式化验证好牛逼，因为这是最复杂的类型系统的实际应用。然而后来我经历了一些事情，发现形式化验证其实并不适合dependent type去解决，这是另外一个话题了。2019年我在知乎上发了一篇文章，叫《看个头》（look ahead），就是展望未来的意思。其中大概表述了一下我的心态转变：形式化验证不应该用dependent type类型系统，而是应该用另外一种叫做自动证明的手段。形式化验证应该用一种对于验证更友好的方法，而不是用 Dependent type这种更加形式化的方法；我认为Refinement Type非常形式化，它是 decidedly correct（绝对正确）的。首先它具有decidable（可判定性），可以在多元素复杂度内解决问题，至少自动证明的type checking（类型检查）是decidable的。同时它也是correct的，意思是行为是确定的。确定的意思是其的算法与行为是可以被准确描述的，不像机器学习与自动证明有着各种神秘优化；但dependent type不一样，他是decidable与correct的，我个人不喜欢undecidable not correct的东西。而类型系统的这种dependent type就是我喜欢的decidable correct的，我个人感觉它很干净：它的type checking能够在多项式复杂度内确定代码是type correct（类型正确），还是type error（类型错误）的。让它来做数学定理的验证的以及数学的形式化我感觉再合适不过了。这很有意义，首先是因为它能解决数学行业的一些问题：数学中的一般的证明都是用自然语言描述的，而如果使用类型系统去描述，其将会使用语法树，由机器可以验证，当我们说服了机器，证明你进行验证过程对了，其他人就只需要看结论就好了，因为它是可以无数次被机器所复现的，而且还有一点代码是可以进行一些变换的，譬如在机器证明中，lemma（引理）是一个函数，传输一些条件给函数，它就能返回一个定理。函数是有函数体的，函数体是一个很大的表达式，那么，当我写了一个数学证明，里面调了一堆lemma，可以清晰的表达出我的证明思路，这种方式就可以被用于零知识证明。零知识证明是指：当我有一个很精妙的证明，我不想告诉别人我的证明思路，但我想让别人知道我已经证明了这个问题，那该怎么办呢？首先，我们都知道这个命题本身是什么，这个命题本身应该是个类型签名，命题是用类型签名表达的，这个命题的证明是符合类型的一个函数体，一个函数体就是一个表达式，一个值，但是我不能把它告诉别人，不然其他人就能看出我的proof technique（证明技巧）。我怎么让你知道我有这个证明呢？我可以unfold（解压缩）这个proof，把所有的lemma全部展开成最底层的形式，得到一个上GB级别的巨型证明，它可以被机器check它的正确性，但是对人类来说没有可读性，光是从头到尾读一遍，就要花上一个月的时间。

Q6:这个过程能否被“反编译”呢？

ICE1000：这需要refold（重新压缩），这很明显是undecidable（不可判定的）的，例如，我们想象一个递归函数，递归了100次，我们是没有办法去让它回到初始状态的。而每一层我们又去调用了很多别的递归函数，这个过程基本无解了。因此这件事在数学上是有很多意义的。

Q7:请问您能再详细说说您对数学本身的看法吗？

ICE1000：数学本身已经无数次证明了，即使看似没有用的数学，它总归在一个时候会变得有用。欧拉研究的神秘的数学结构，后来导致了弦论的产生。在代数拓扑学研究的纤维丛之类的结构现在也被用到了物理学中，被不被用起来，只是一个时间问题而已。更有趣的是，数学在没有被用起来的时候，看起来一定是没有用的。所以说我们就没有办法在研究数学的时候评价它的实用性。纵观历史，只有一个人能做到在研究非数学领域时发明数学工具去解决问题，其他人都是利用现有的数学工具解决问题。因此，我们一定要先把数学研究到当下的极致。也正是这个原因，我个人认为研究辅助数学的意义不亚于形式化验证。如果用类型系统能把它做好，就可以解决数学中最大的一个痛点：一个真正的数学foundation（基础）。它与集合论不同，集合论其实是我们假装在用这个foundation，但实际上还是像高斯或者欧拉这样的那种靠直觉的方式去做数学。那个年代的数学家，都是靠直觉的：我认为三角形是这样的，那就是这样的。他们不会去想平面几何应该基于怎样的框架，譬如欧几里得几何中的平行线永远不相交，也就是第五公理。必须得先对公理进行规定，之后才能够用公理去证明三角形的内角加起来是180度。那些数学家们不会声明这些公理的存在，他们只会说我觉得这样移动一下，是不是就证明了这个问题？但是他们其实隐式的使用了一些东西。
​在这里我想聊聊数学基础：数学基础是一种概念，譬如希尔伯特自然演绎、 ZFC，它的意义在于提供了一个讨论数学的框架，数学界将数学基础设计了出来，但是在使用时却还是凭直觉出发：比如他们眼中的函数还只是一个公式，而不是一个笛卡尔积的子集。数学基础强迫我们思考讨论数学时最最基础的假设。而类型论作为数学基础，打开了计算机世界的大门，给了我们 “与计算机讨论数学” 的机会。为什么这个机会如此重要呢？因为计算机可以比人类更快更准确地检查这些定义和证明的正确性，而且如果证明有问题，它还可以提示人类哪里有问题。缺点就是你需要告诉计算机几乎所有的证明细节，但是这又可以借助一些叫做 proof engineering 的手段解决。而研究类型论本身的意义就在于修改它，使它变得更好用、能更直观地表达数学结构。就像数学基础可以被修改一样。比如说我把欧几里得几何平行线均线永远不相交修改，两条平行的直线，有可能相交会怎么样呢？有三角形三个内角加起来不等于180度是怎样的？我们得到了非欧几何，我们还得到了黎曼几何，就有了不一样的数学。当我们在研究几何图形的时候，我们假设不关心长度，不关心大小，不关心直的还是弯的，我们只关心connectivity（连通性），比如说两条看起来不一样的直线，我们认为它们是一样的。进一步地，我们可以研究更general的性质：比如研究一个线段，一个点，可以有点与点之间的线段吗？线段与线段之间可以有线段，也就是面。我们还可以把一个线段的左右2点和他自己连起来，我们也可以把它做两点先转过来，得到了莫比乌斯环，然后我们还可以让一个点可以绕着一个圆转。我们还可以把一个圆绕着一个圆转，这得到了什么？得到甜甜圈，甜甜圈是一个很经典的拓扑结构，因为它同构于两个圆圈上的点的地方，这个同构关系用HoTT（同伦类型论）写的非常直观，HoTT比起传统类型的意义，就在于它使得描述这种连续的结构，包括甜甜圈圆圈，这种东西变得非常方便，在计算机中非常方便，所以我在计算机中可以表达1个甜甜圈，因为甜甜圈就是1个有4个构造函数的1个类型。就如前面所说的，数学一定要发展得更快，这样才能够最好地去解决其他问题。然后才说人们一定会觉得数学有用。如果研究数学是有用的，那么解决数学的问题就一定是有用的，所以类型系统就是值得研究的，让我觉得可以去搞一搞，其次是这个东西可以帮助你编程，对于写代码本身也很有意义。

Q8:请问就您自己而言，开源为您带来了什么呢？

ICE1000：开源的风气影响了学术社区，所以大家也倾向于分享代码。另外开源社区形成了一些不成文的共识，这使得我们这些玩小众技术的人管理和维护自己的社区也变得很方便了。在我的学习早期我借助那个啥啥啥 Hub 学到了很多姿势，后来我在技术比较成熟的时候也反哺了社区，没有开源的风气这些都是无法做到的。

Q9:请问您还想对读者说一些什么呢？

ICE1000：希望大家保持对写代码的热爱坚持下去吧，开源社区这种几乎实现了共产主义的小型社会仅存于技术圈子，是我们编程爱好者们的骄傲。同时也希望大家也能为开源世界的繁荣尽自己的一份力，保持谦逊和友善，开源项目的维护者也都是普通人，我们享受了别人的付出也应该尊重他们才对。

 

#本次专访结束#

 

以下通信方式为学生开源年会的官方联络方式，敬请关注。

本次活动官方网站: 2020zh.sosconf.org

学生开源年会官方网站: sosconf.org
电报英文群组：https://t.me/sosconf
官方微博：https://weibo.com/sosconf
电报中文群组：https://t.me/soscon
中文交流QQ群：738852894

微信公众号：学生开源年会