∞-type Café Summer School TuT

∞-type Café 暑期学校 2023

∞-type Café 暑期学校 2023将会在2023年7月2日正式举行。这次活动偶然源于一个提议，是否可以举办一个关于类型论暑期活动？ 由于当下国内研究类型论的学者非常少，相关资料也寥寥无几。于是我们决定尝试一下！

什么是类型论？ 它生于逻辑，长于数学，开花于计算机科学，结果于程序语言。它横跨了几个学科，彼此紧密。它在数学中作为新的数学基础出现，与集合论和范畴论并称。在计算机科学中，当提到类型的时候，我们会在第一时间想到各种编程语言，它可以帮助编译器或者解释器实现编译期的检查。柯里霍华德同构的出现使得我们重新开始审视类型，在命题即类型的观点下诞生了基于类型的交互式证明助手。把某个具体问题的证明当做程序来写成了现实，但是想要写出这样的程序，首先需要接受并熟悉它所对应的语言。在这一点上，无论是数学系还是计算机科学的学生都面临种种的问题。数学系的同学可需要先迈过编程这个坎，而计算机科学的同学要理解其背后的数学基础也并不太容易。到最后你历尽千辛万苦终于写出了可以被证明助手通过的程序，你是否问过自己它真的是一个证明吗？ 其中定义的那些函数是否是 well-defined? 其中构造的 objects 是否合理？ 其中使用的某些技巧是否正确？ 这些问题会推着你逐渐往前走，越走越远…

在某一天一个初学者偶然了解到类型论并开始了摸索，那么他的学习路径一定是充满了曲折的，因为我们当初也是这样走过来的。借助这次活动希望能帮助到更多想要学类型论的同学或者想要了解类型的同学，反过来我们也能交到更多的朋友，这是就是我们的简单而单纯的愿景。

引用Infinity Type Café群主狗先生的一句话:

在寒冷的夜晚，两个孩子生起了篝火，越来越多迷路的孩子来到了火堆边。他们感到无比幸福。
天亮了，孩子们慢慢地找到了自己的路，于是一个个地远去了。但他们永远不会忘记那个曾经给予过他们温暖的篝火。

Thorsten Altenkirch 对类型论的一个简短介绍:

暑校的浮光掠影

从7月2日到7月31日；从第一节课的100+人，到逐渐稳定到30+人；从暑校群不到100人，到如今的500人；从b站的0关注到1000关注 (无穷类型咖啡B站账号大约是永久封存了) …

这里特别感谢各位讲师，说实在的，如果没有他们自发地站出来，暑校不会如此绮丽丰富.

还记得在暑校征集演讲主题的时候，子鱼是第一个站出来要讲东西的人，紧接着就是oCaU，这让我们在暑校组织之初就收集到了两个演讲主题，让暑校有了往下做下去的信心。其中oCaU在暑校中一个人讲了一门基础课程和两个演讲主题，要知道ocau是一个非常忙的打工人和奶爸，要做到这一点很不容易，因此他的演讲时间段，往往是在晚上和周末。

接着就是我们café实力担当Trebor，在群里面你总是可以看见他在帮群友解决各种问题，而你只能感叹Trebor真的懂的太多了。Trebor在暑校中一个人讲了一门基础课程和三个演讲主题，恐怖如斯。还记得Trebor在最开始讲的时候处于感冒的后期，你可以从他讲的状态中感受到他本人并不好受，但还是坚持地按期讲完了所有东西。

再然后就是千里冰封带着他的演讲内容走来了，是他带动了课程讲义的必要性，使得出现了一份份精美的课程讲义. 千里冰封在暑校中一个人讲了一门基础课程和一个演讲主题，由于他本人在国外，所以为了平衡时间差，他讲东西的时间段在晚上，但是对于他而言却是早八。

最初是没有基础课程这环节的，但是考虑到所有的观众，这个环节还是非常有必要的。oCau，Trebor和千里冰封是最早确定要讲课的人。再然后就是Alias Qli和无懈可击99自发地站出来确定了另外两门课。此时还剩下一个比较关键的课程没有人讲，面皮站了出来，解了燃眉之急。最后就是qxr(天生万物以养人)临时上阵和kang带来的新课程。还记得Alias Qli通宵做幻灯片，他说这是暑校第一课，也是很关键的一课，他有责任讲好。还记得无懈可击99说的，要写出最好的中文HoTT教程。还记得面皮那将近30mb的讲义。还记得qxr自称类型论军哥。还记得kang的小黄鸭和经常讲着讲着就绷不住了的愉快课堂氛围。

这次暑校包含了13个演讲主题，其中12个都源于演讲者自发，剩下一个是来自于邀请。我们通过邮件地方式邀请了来自台湾的子篆，过程是出奇的顺利，最后也没有来得及好好的感谢。最后三位演讲者Anqur, 游客账户0x0, 魔理沙大概带来的演讲主题大概是对计算机方向的同学最为友好的。这也是这次暑校暑校想要追求一个小平衡，能带更多的人一些有趣知识。最后的最后就是狗先生了，大家能在聚在一起都是因为他创建的café，也是在他的鼓励之下才有了我们这次暑校。我们相信这些讲师付出巨大时间和精力制作的讲义，幻灯片和讲课内容终会影响一批又一批后来人！

另外也特别感谢我们的组织者，afu对演讲主题的收集，暮秋对每一次会议记录的处理，茗洛提供的无限制腾讯会议，conway提供的无穷类型咖啡B站账号，LiangHillon对每一次会议的记录，toaster后期的暑校组织工作。

以上，应该提到了所有参与暑校的可爱的相关人员，当然还有陪伴我们一个月之前的观众，我们都记得！

以下，是部分观众，讲师和组织者留下的一些话:

非常感谢所有的工作人员和讲师，感谢你们的慷慨付出和耐心解答。很难想象中国这么大只有不到500人投身于此，但也正是如此未来的前景才更加广阔，希望类型论能给数学和工程带去新的方向！ – 来自不知名的某某

Type “(me : 5eqn) → (上了暑校 me → 0) → 是民科 me” is inhabited 写成这种形式只是图一乐，沾了自然语言本来也不会太严谨罢，就别太深究定义了…… 只是暑校的确让我少走了不少弯路，作为例子，如果没暑校的话我不好说得花多久才能整出元变量求解……这样的例子还有不少 暑校成功让我在（至少目前）最喜欢的领域步入正轨，好的工作。 – 5eqn

十分感谢本次的暑校(组织者和老师) 给想了解类型论的人提供了一个平台(^-^) 不然自己看书可能效率极低 也希望以后能有更多类似的活动 最后给大家拜个早年吧～ – BYNT

真的很开心能参加这个活动！我从遇见自然数游戏开始接触这个领域，后来在多位朋友的帮助下才知道类型论，知道有这个活动——其间多有曲折辗转，走了许多弯路，好在最终找到了自己最初想要找的东西。十分感谢帮助过我的朋友和这次暑校的组织者和讲师，要是没有你们我会错过多么美妙的东西！出于感激，我在暑校的后半程参与了一点组织安排工作，略尽绵薄之力。希望以后能有更多这样的活动，也祝愿像我一样迷途的旅客们终能前往心中所向：） – 来自不知名的某某

本人粗通数学，了解些许范畴论，但于逻辑，计算机算不上粗通，这次暑校让我对这些课题及关系有初步了解，幸甚！ 辛苦了！主持人和讲师们，多谢！ – 来自不知名的某某

本次暑校的课程内容相当精彩，并且前置知识要求不多，小学生都能听懂，实在是泰裤辣！尤其是综合同伦论/同论类型论，让不懂拓扑的人也能了解同伦论的一些直觉。 除开课程外，还有本次暑校演讲，一些演讲作为课程的扩展和启发相当不错，比如游客账户的 mltt 实现，让人觉得一看就会，一写就废。 Trebor 的范畴论讲的也很不错，可惜学不会。 –来自不知名的某某

感谢各位讲师的付出，有各位讲师带着学习和精心准备的讲义比起自己学习要更有效率也更有趣。希望这样有意义有价值的学习交流活动能每年都有。– 来自不知名的某某

同伦类型论是非常小众的领域，中文的资料也很稀缺。然而，正是这份神秘和罕见，使得它显得格外令人惊奇。正是为了探索这个令人着迷的领域，我们才举办了这个暑期学校。 大多数人最终并不会深入接触同伦类型论，但这从来就不是最终的目的。我们希望这个学校能为大家带来一些启发和乐趣，还有不要忘记：即便世界可能变得多么暗淡，无论何时，总有人在那些你意识不到的角落里创造着令人惊叹的闪光点。 – kang

café的火堆非常温暖，讲师和同学带来的亮光照亮了深邃知识宇宙的一角，这已经成为我人生中最值得感谢和难以忘却的一段时光。 – 来自不知名的某某

目睹过国内外太多“网师”做基础教育，起初免费而后要么停更要么背离初心推出收费课与“学习方法课”割韭菜。相比之下，暑校在做到完全公益的前提下分享这么偏前沿而又有深度的内容，同时维持一个并不小的体量，实属不易。由于时间原因从未看过直播，回放也只看了两三节，但我能感受到暑校各位老师的用心和各位老师的热忱。 相比暑校使我接触到的前沿理论，我想暑校带给我的还有更重要的东西——做专业领域公益课，不怕短时间播放量低的坚定，以及开拓前人未走之路，分享专业知识的勇气。我也曾经做过公益课（当时讲的是数论），可是一个视频过了一周100播放量不到真的很打击人，最后由于时间原因不想讲了。看到暑校办的这么好，我想我可能要重新开始尝试录点公益课了。 祝暑校越办越好！ – 学数学的wunderlich 寅卯年六月十八

结束是另外一个开始，期待下一次的暑校！

相关重要信息

面向怎样的听众

  • 想要了解类型论的同学;
  • 想要学习并使用类型论的同学;
  • 具有一定类型论基础，想要往前再走一步的同学;
  • 熟悉类型论，并想和我们讨论过去，当下，未来的同学。

基础课程

考虑每一个听众可能对类型论有不同的了解程度，并且这也是第一次暑校活动，所以我们专门地邀请了七位讲师给大家来一次贴心”补课”。以下课程参考了学习类型论的常规路径和本次暑校中talks要求的前置知识，课程讲解顺序从上至下。

希望以下课程能在不同程度上帮助到每一位听众，并且我们鼓励听众提前学习。如果在此过程中碰到问题，可以将其先存起来，然后在相应课程开始之后，直接向讲师提问。

Don’t sweat the stuff you don’t understand immediately. Keep moving!

你可以查看我们未完成的 如何学习类型 作为进一步学习的参考。

课程对应的日程表如下:

7月2日-7月12日课程安排:

日期 下午2点-4点 晚上8点-9点
7月2日 Alias Qli
λ演算和简单类型入门
视频1 视频2 视频3

STLC 的入门 (第一节)
STLC 的延伸 (第二节)		 无
7月3日 面皮
依值类型入门 (第一节和第二节)
视频1 视频2 视频3 视频4 视频5		 Alias Qli
λ演算和简单类型入门 (习题答疑1)
7月4日 kang
一点儿综合同伦论 (第一节和第二节)
视频1 视频2		 面皮
依值类型入门 (习题答疑1)
7月5日 无 oCaU
Agda使用入门 (第一节)
视频1
7月6日 天生万物以养人
Coq和Lean入门介绍 (第一节和第二节)
视频1		 oCaU
Agda使用入门 (第二节)
视频2
7月7日 无懈可击99
同伦类型论(HoTT)入门 (第一节和第二节)
视频1 视频2		 oCaU
Agda使用入门 (第三课)
视频3
7月8日 无 无
7月9日 Trebor
范畴论与范畴语义

范畴-函子-自然变换 (第一节)
视频1		 无懈可击99
同伦类型论(HoTT)入门 (习题答疑1)
视频1
7月10日 无懈可击99
同伦类型论(HoTT)入门 (第三节和第四节)
视频3 视频4		 oCaU
Agda使用入门 (习题答疑2)
视频1

Trebor
范畴论与范畴语义 (习题答疑1)
7月11日 kang
一点儿综合同伦论 (第三节和第四节)
视频3 视频4		 无
7月12日 Trebor
范畴论与范畴语义

伴随-米田引理 (第二节)
视频2		 无懈可击99
同伦类型论(HoTT)入门 (习题答疑2)

Trebor
范畴论与范畴语义 (习题答疑2)

7月13日-7月15日课程安排:

日期 晚上8点-10点
7月13日 千里冰封
立方类型论(Cubical)入门 (第一节和第二节)
视频1 视频2
7月14日 千里冰封
立方类型论(Cubical)入门 (第三节和第四节)
视频3 视频4 视频5
7月15日 千里冰封
立方类型论(Cubical)入门 (习题答疑1)

注: 是否有习题主要看讲师自己是否有相关的安排，并且习题答疑也包含了讨论和提问的环节。

夏末演讲会

7月13日-7月15日演讲安排: 时间段安排上与基础课程基本相同, 注意13日到15日，白天是演讲，晚上是课程。

日期 下午2点-4点 晚上8点-10点
7月13日 Trebor
范畴语义基础
视频 幻灯片		 无
7月14日 林子篆
WASI 与 component model，跨语言的资源共享问题
视频		 无
7月15日 oCaU
Agda 佐恩引理
视频		 无
7月16日 Anqur
心灵鸡汤: 你能从依赖类型版 JS 中获得什么
视频 幻灯片		 游客账户0x0
手把手教你实现 MLTT
视频
7月17日 Trebor
综合数学综述与数学基础多元主义
视频 幻灯片		 kang
综合同伦论之π₁(S¹)
视频
7月18日    
7月19日   Trebor
有效意象：构造主义与可计算性的桥梁
（又名：如何编译你的证明）
视频 幻灯片
7月20日    
7月21日    
7月22日 子鱼
LLM自动定理证明的进展
视频		 千里冰封
实现类型论中的高级特性与不那么 cool 的 coolt
视频
7月23日   oCaU
Agda综合哥德尔不完备
视频
7月24日    
7月25日   魔理沙
Partial eval, Staging, Compiler and NBE
视频
7月31日 Gestellmensch
集合论已死,类型论当立
视频		  
  • oCaU,
    • Agda 佐恩引理

      佐恩引理是经典数学中最基础的定理之一。 然而，作为直觉主义数学的前沿之一，同伦类型论 (HoTT) 在经典领域的扩展并未获得太多研究关注。本讲旨在填补这一空白，我们在HoTT的框架下展示对佐恩引理这一经典定理的证明，并顺带介绍其中涉及到的Agda语法和HoTT基本概念。 (知乎入口).

      前置知识: Agda
      注: 看需求可以顺带讲其中涉及到的 Agda 的语法，HoTT 的基本概念。

    • Agda综合哥德尔不完备

      这是对哥德尔不完备定理的超简短形式化。我们在HoTT中引入邱奇-图灵论题（公理），建立综合递归论环境，以此直达哥德尔不完备定理论证的核心，而无需涉及复杂的计算模型和编码细节。

      前置知识: Agda + 数理逻辑的基础知识。

  • 子鱼, LLM自动定理证明的进展

    大语言模型驱动的自动定理证明的最新方法和结果的科普。

    前置知识: 几乎没有。
    注: 跟类型论关系不大，可当做 appetizer 或者 dessert。

  • Trebor,
    • 范畴语义基础

      依值类型论是丛的语言。以此为主线，由浅入深讲解范畴语义的大框架，并且介绍范畴语义如何实际用于解决问题。

      前置知识: 熟悉依值类型论与范畴论基础。
      注: 可以分多次（越多次讲得越深，前置知识越少）。

    • 综合数学综述

      我们习惯将每种数学对象都由更基本的数学对象表示：用Cauchy列编码实数，再用实数构造平面，进而研究平面几何。但是Euclid在《几何原本》中则是直接使用公理刻画想要研究的对象，从而构建了一个极其方便的研究几何的语言，正如编程语言中的DSL一样。本讲讲述一些综合数学的实例与应用。 nlab入口

      前置知识: 熟悉依值类型论与范畴论基础。
      注: 几个题目可以选一个讲，有时间可以都讲。

    • 有效意象：构造主义与可计算性的桥梁 （又名：如何编译你的证明）

      构造主义经常与可计算数学混同起来，然而许多构造主义的系统并没有显然的计算解释。另一方面，通常的可计算性仅仅处理了自然数之间的映射，而数学中常常需要处理其他事物的可计算性。有效意象给出了一套系统的链接构造主义与可计算性的语言。

      前置知识: 无需前置，少许逻辑和范畴的基本定义（如什么是全称命题，范畴的定义等）为佳。
      注: 几个题目可以选一个讲，有时间可以都讲。

    • 数学基础多元主义

      注: 科普性质。

  • 千里冰封 (全部讲座的摘要),
    • 不那么 cool 的 cooltt

      Lamett 项目介绍，根据群友的意愿讲讲其中的组件。

      前置知识: 熟悉 MLTT 的实现(可以参考 Mini-TT 和 elaboration-zoo). 若想要理解其中的代码, 那就还需要基本的 Java 编程。
      注: 如果想听别的也可以直接联系我。

    • 实现类型论中的高级特性

      简要介绍 elaboration-zoo 中介绍的几个高级的例子 (变量求解, 隐式参数等), 如何实现模式匹配。

      前置知识: 对这些被实现的功能本身有充分的理解。
      幻灯片

  • Gestellmensch, 集合论已死,类型论当立

    HoTT,泛等公理的数学背景: 同伦论,模空间,还有很多相关的话题。以及为什么(同论)类型论是更好的数学基础。

    前置知识: 不知道, 可能更多讲很泛泛的东西, 图一乐。

  • Anqur, 心灵鸡汤: 你能从依赖类型版 JS 中获得什么

    RowScript 项目介绍; 如何从最基础 NbE 扩展语言功能; 讲点心灵鸡汤。

    前置知识: 有依赖类型的直觉最好, 没有也没关系。

  • 林子篆, WASI 与 component model，跨语言的资源共享问题

    WASI 是让 WebAssembly 的程序可以操作系统资源而设计的接口，component model 让不同语言实现的模块可以交换资料。如何用 linear type 与 effect system 避免模块见资源交换的错误，实际上又有什么限制呢？

    前置知识: 大概知道不可变的 functional programming 就好了
    注:

    • 在此介绍的方法不一定能进入标准，标准组织中有人有兴趣但是
    • 不会用正式跟数学化的方法介绍，这些模型都是原型，在更确定会进入标准之前我不会进行更深入的检查
  • 魔理沙, Partial eval, Staging, Compiler and NBE

    介绍partial evaluator，并且以这个为基准，引入跟staging, compiler, normalization by evaluation等技术的联系。

    前置知识: 最好懂definitional interpreter。

  • 游客账户0x0, 手把手教你实现 MLTT

    在ocaml中实现Per Martin-Löf type theory。

热烈欢迎各路老师和同学来分享topics!

目前听众希望的talks

  • 类型论的学习路线图 (希望演讲人讲述下自己类型论的学习过程。最好对每段学习过程讲下：难点以及怎么度过难点，推荐学习书籍论文等。)
  • Cubical Agda 的钉子 (请介绍不需要太多前置的好做的漂亮的小众领域。例：https://arxiv.org/pdf/2208.03844.pdf#page22)
  • 类型论的设计哲学：如何判断不同设计的好坏？
  • 从数学哲学或数理逻辑视角对同伦类型论作为数学基础的介绍
  • 类型论的入门知识（零基础适用）
  • 如何用代码实现类型系统（零基础）
  • 范畴语义 (对于 ATP 算法设计; MLTT 和 Cubical 的)
  • HoTT 的进阶 (希望可以讲一些 high level 的东西和比较直观的东西，比如 HoTT 的发展或者构建过程，为什么要引入 homotopy theory, 带了一些什么好的结果等等)
  • Cubical 的入门
  • 类型论的应用 (如《类型论简史》展望部分所提的问题, 以及严肃地考虑类型论在工业界的应用)
  • 类型系统的（高效）实现 (比如 MLTT type check 的实现)
  • 综合数学
  • 同伦类型论以及如何应用到数学里
  • 同伦类型论和 ZFC 比较优点在哪
  • 类型论在计算机安全中的应用 (例如区块链和软件安全等)
  • mathlib 的项目实践

热烈各位观众朋友来分享想要听的 topics!

相关问题

  1. 本次活动是线上还线下？

    线上。

  2. 这次活动是否有录像？

    B站会同步更新。

  3. 这次活动是否会提供课上内容的相关材料？

    ntype-cafe-summer-school 会同步更新课上的讲义，幻灯片，代码和推荐课外内容。

  4. 人在国外有时差，如何参与这次活动？

    我们目前考虑在中国时区的下午和晚上举行，请听众合理地安排一下时间。 如果时间上存在无法避免的冲突，可以参考Q2和Q3。

  5. 课后是否可以留一些练习作业？

    这当然是可以的，我们会与讲师进行沟通。作业后续可能还有答疑环节，这部分活动目前暂定在QQ群进行。

  6. 是否可以对想要入门的同学多一点的照顾？

    这是工具人一直争取的事，初步设计暑校的时候是没有前置课程的，但是工具人觉得这样可能会把很大一部分人排除在外，因此给大家贴心准备了相关前置课程。事实证明确实是这样，因为从问卷的情况来看熟悉类型论的人只有仅仅的%10。

  7. 是否可以充分考虑不同领域方向的听众？

    目前，数学系和计算机系的同学几乎分别占了一大半，我们在尽力平衡talks的相关性，可以看到talks里面有各自领域的东西。

  8. Infinity Type Café是怎样一个组织？

    一个大部分成员都是学生的组织。特别感谢那些在意见中给于我们的支持和鼓励的朋友！

相关人员

讲师

除了课程和 talks 的在线答疑，听众也可以通过上述联系方式联系讲师答疑，或加入暑校群（QQ 群号 791437680）询问问题。寻找讲师答疑即代表您同意我们在暑校相关内容中（包括但不限于录播视频和暑校网站）公开您的问题和答疑内容。

特别演讲人

  • 等一个

组织者

Thanks!