形式化科学 & 类型理论

类型论是数学、逻辑和计算机科学以下的一个分支，是研究不同类型系统及其表达形式的学科。某些类型系统适合用作数学基础，取代数学家一般使用的集合论，其中最具影响力的有阿隆佐·邱奇的有类型 $lambda$ 演算和 Martin Lof 的直觉类型论。许多函数式语言和交互式定理验证工具都建立在类型论的基础上，如Agda、Coq、Idris、Lean等等。

类型论的核心概念是，每一条合乎语法规则的表达式（或称“项”）都有其所属的“类型”。通过结合多个基础类型，可以定义更加复杂的类型。如此得出的类型可以表示各种复杂的数学结构，如自然数、群、拓扑空间等等（对于不同类型的数学对象，也有专门的类型理论）。在集合论中，这些结构都是含有元素（或称成员）的集合，它的定义纯粹就是指定其所含的所有元素。在类型论中，这些结构的定义并不罗列属于它的所有项，而是指定如何建构它的项的一套推导规则。集合论需要一套一阶逻辑系统，但是类型论只需要"类型"这个基本概念。

学习路线

• 了解一个定理证明器，比如 Agda / Lean4 / Coq
  • Agda 比较灵活，可以研究类型论；Coq是老牌证明器了，基础资源丰富；Lean4 是微软研究院开发的交互式定理证明器，包含了很多先进的学术成果，近年来也在飞速发展，而且 Lean4 也能当作一门通用的函数式语言学习
  • Agda 入门（也包含了一些PL知识） Programming Language Foundations in Agda
  • Lean 函数式编程 Functional Programming in Lean
  • 顺便宣传一下笔者参与翻译的中文版 Lean 函数式编程
  • Lean 数学证明 Mathematics in Lean
  • Lean 定理证明 Theorem Proving in Lean 4
  • Coq 数学证明入门 Mathematical Components
• 理论知识
  • (可选)：如果你追求更本质的理解（或者学习下面的书籍有困难）：Strucural Proof Theory
  • 非常不错的入门书籍： Type Theory and Formal Proof
  • 想做高维数学 / 去公理化？：Homotopy Type Theory
  • 如果你的大脑可以轻松想象六维空间：Cubical Type Theory 的相关论文
  • 了解一下范畴论的知识也是很有必要的
    • 程序员的范畴论： Category Theory for Programmers
    • 上一本书的进阶：The Dao of Functional Programming
    • 其他范畴论书籍（还有数学前沿领域 Topos）
      • Cakes, Custard and Category Theory: Easy recipes for understanding complex maths — Eugenia Cheng
      • Category Theory, Steve Awodey. pdf course
      • Basic Category Theory for Computer Scientists - Benjamin C. Pierce. Previously available in a draft entitled A taste of category theory for computer scientists
      • Categories for the Working Mathematician — Saunders Mac Lane
      • Conceptual Mathematics A First Introduction to Categories, 2nd Edition - F. William Lawere and Stephen H. Schanuel
      • Category Theory for the Sciences — David I. Spivak. Previously available in a draft entitled Category Theory for Scientists
      • CTCS-2nd Category Theory for Computing Science - Michael Barr and Charles Wells CTCS-1st
      • Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist pdf
      • Topoi, The Categorical Analysis of Logic, Robert Goldblatt Amazon
      • TTT - Toposes, Triples and Theories - Michael Barr and Charles Wells
      • Category Theory Lectures Notes for ESSLLI - Michael Barr and Charles Wells pdf
      • Seven Sketches in Compositionality: An Invitation to Applied Category Theory - Brendan Fong, David I Spivak
      • Applied Category Theory Course - online course conducted by John Baez forum
      • CTFP - Category Theory for Programmers - Bartosz Milewski. The free PDF version was created by Igal Tabachnik. Video lectures based on this material: part 1, part 2, part 3.
      • CT4P Category Theory for Programming — Benedikt Ahrens, Kobe Wullaert
• 研究阶段：类型论在国内研究的人不多，发展潜力很大，你也可以相对轻松遇到前沿理论，在完成上述路线学习后，相信你也找到了自己想要深入的方向。这里推荐一些做类型论的学校 、导师
  • 瑞典：University of Gothenburg / Chalmers
  • 丹麦：Aarhus，Bas Splitter 和 Lars Birkedal
  • 德国：慕尼黑大学
  • 法国：inria
  • 英国：Cambridge
  • 美国：CMU，Robert Harper

推荐书籍 / 论文 / 视频

• Books
  • SF - Software Foundations - Benjamin C. Pierce et al. Available with jsCoq
  • TAPL - Types and Programming Languages - Benjamin C. Pierce
  • PROT Proofs and Types - Jean-Yves Girard, Yves Lafont and Paul Taylor - 1987-90 pdf
  • PFPL - Practical Foundations for Programming Languages (Second Edition) - Robert Harper Online preview edition
  • ATTAPL - Advanced Topics in Types and Programming Languages - Edited by Benjamin C. Pierce
  • CPDT - Certified Programming with Dependent Types - Adam Chlipala
  • SEwPR - Semantics Engineering with PLT Redex - Matthias Felleisen, Robby Findler, and Matthew Flatt. Redex
  • HoTT - Homotopy Type Theory, Univalent Foundations of Mathematics
  • Coq’Art Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions - Yves Bertot, Pierre Castéran.
  • TTFP - Type Theory and Functional Programming - Simon Thompson, 1991
  • PiMLTT - Programming in Martin-Löf’s Type Theory, An Introduction - Bengt Nordström, Kent Petersson, Jan M. Smith
  • Using, Understanding, and Unravelling The OCaml Language — An introduction pdf
  • Polymorphic typing of an algorithmic language (PhD Thesis) - Xavier Leroy pdf
  • ATP - Handbook of Practical Logic and Automated Reasoning - John Harrison
  • Basic Simple Type Theory - J. Roger Hindley pdf paperback@booko
  • Lambda Calculus and Combinators pdf — J. Roger Hindley and Jonathan P. Seldin
  • Semantics with Applications: An Appetizer — Hanne Riis Nielson, Flemming Nielson
  • An Introduction to Lambda Calculi for Computer Scientists - Chris Hankin
  • The Definition of Standard ML (1990) and Commentary on Standard ML (1991) definition (pdf) commentary (pdf)
  • The Definition of Standard ML (Revised) - Milner, Fofte, Harper, and MacQueen
  • Programs and Proofs — Ilya Sergey pdf
  • Type Theory and Formal Proof: An Introduction — Rob Nederpelt, Herman Geuvers
  • Lectures on the Curry-Howard Isomorphism (pdf)
  • Program = Proof — Samuel Mimram pdf
• Papers
  • A Tutorial Implementation of a Dependently Typed Lambda Calculus — Andres Löh, Conor McBride and Wouter Swierstra pdf. Previously published as Simply Easy.
  • ΠΣ: Dependent Types without the Sugar - Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, and Nicolas Oury
  • Lambda Calculi with Types — Henk Barendregt
  • Intuitionistic Type Theory
  • Type Theory - Thierry Coquand
• Videos
  • OPLSS — Oregon Programming Language Summer School
    • OPLSS 2023 — Types, Semantics, and Logic
    • OPLSS 2022 — Types, Semantics, and Program Reasoning
    • OPLSS 2021 — Foundations of Programming and Security
    • OPLSS 2019 — Foundations of Probabilistic Programming and Security
    • OPLSS 2018 — Parallelism and Concurrency
    • OPLSS 2017 — A Spectrum of Types
    • OPLSS 2016 — Types, Logic, Semantics, and Verification
    • OPLSS 2015 — Types, Logic, Semantics, and Verification
    • OPLSS 2014 — Types, Logic, Semantics, and Verification
    • OPLSS 2013 — Types, Logic, and Verification
    • OPLSS 2012 — Logic, Languages, Compilation, and Verification
    • OPLSS 2011 — Types, Semantics and Verification
    • OPLSS 2010 — Logic, Languages, Compilation, and Verification
    • Complete archives 2002-Present
  • HoTTEST — Homotopy Type Theory Summer School 2022
  • ICFP 2012 Monday keynote. Conor McBride: Agda-curious?

参考

• csdiy.wiki
• wikipedia
• zhihu: Jason Hu
• https://steshaw.org/plt/