千里冰封 讲座介绍

SIST 1A104 Mon May 10 2021 18:00:00 GMT+0800

Welcome to GeekPie_HPC 讲座系列! 未来我们将邀请各界科技人士来我校讲座， 敬请关注。

讲座介绍

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

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

本次讲座，将从type system 基础出发，带领大家进入一个type free 的境界。如涉及宗教战争，欢迎来怼。

演讲视频

讲者介绍

Pen State 大三本科生，在知乎等平台非常著名，吸收了一大波程序员成为了向往HoTT type system 的教徒。同时也吸引了一大波同学去打OI。千里冰封的研究方向是编程语言，方向是复杂的类型系统，在Agda/Idris 贡献了一众代码，进入Jetbrain 实习前的代表作是Julia插件。现在更多了，多到无法想象。