你怎么知道我去ICFP2025了？

起因

半年前uu鼓励我把我阶段性的成果（真的有吗？）发表一下，也获得一些反馈，候选TyDe，ICFP和SPLASH的SRC。最后是参加ICFP了的SRC，我还从来没有参加过类似的活动，更是无法想象我还能因此去ICFP的，我印象里ICFP是只有中了牛逼论文才能去的牛逼会议。不过意外的是（？）我的SRC paper被accepted了，这意味着我真可以去ICFP了！其实至此我已经很知足了，但是uu说：你给我拿个奖回来，你不想我还想呢！

博客复活是怎么一回事呢？其实就是我看这个站有很多不喜欢的黑历史，所以一并清理掉了！

几百年前就想入门OCaml了，但是一直咕咕，现在终于下定决心学习一下。

前段时间入了个树莓派zero 2w玩玩，因为性能比较捉急，所以没有装桌面环境。

最近被问到了关于ADT的事情呢，于是想写一篇速通关于ADT、递归类型是怎么回事.

本文是POPL2022同名文章的中文翻译，無断転載禁止。

关于match types的Scala文档：https://docs.scala-lang.org/scala3/reference/new-types/match-types.html

Type-level programming在FP越来越流行，但type-level programming和subtyping的组合还没有充分的探索。这篇文章中的match types等价于类型层面的pattern matching，在基于system F$_{<:}$的一个演算上形式化了match type这个feature，证明了它的soundness。在Scala3的reference compiler上实现了match types的系统。

本文为Type Theory and Formal Proof : An Introduction 的笔记，纯个人向（

之前我们遇到了以下的依赖关系：

• 依赖于项的项：$\lambda_\to$.
• 依赖于项的项$+$依赖于类型的项：$\lambda2$.
• 依赖于项的项$+$依赖于类型的类型：$\lambda\underline{\omega}$.

显然有一个扩展缺失了：

• 依赖于项的项$+$依赖于项的类型：$\lambda{\rm P}$.

最近在尝试用Haskell实现Peter Shirley的Ray Tracing in a Weekend一书，发现了这个问题，并琢磨出了一些解法，看起来像是发现了一种设计模式，不过不知道叫什么名字（

本文为Type Theory and Formal Proof : An Introduction 的笔记，纯个人向（

类型构造子

之前我们从项$\lambda x:\sigma.x$中由类型变量抽象出$\lambda \alpha:\ast.\lambda x:\alpha.x$. 类似的，我们也可以从类型上抽象. 如类型$\beta\to\beta,\ \gamma\to\gamma,\ (\gamma\to\beta)\to(\gamma\to\beta),\ \dots$，都有$\Diamond\to\Diamond$这样的结构.

本文为Type Theory and Formal Proof : An Introduction 的笔记，纯个人向（

类型抽象和类型应用（Type-abstraction and type-application）

对于抽象这个过程，我们有项$M$，其中可能有自由变量$x$，假设$x$有类型$\sigma$，我们从$M$中抽象$x$，可以得到项$\lambda x : \sigma.M$，同时，所有在$M$中的自由变量$x$被绑定了，我们说：

项$\lambda x:\sigma.M$依赖于项$x$.

因此，$\lambda{\to}$中可以构造依赖于项的项（terms depending on terms）.

相应的是应用，对于$MN$的构造，我们可以把$M$应用到$N$，也得到一个项.

这称为一阶（first order）抽象，或一阶依赖，因为这个抽象是在项上进行的. 同时应用也是一阶的.

现在我们引入依赖于类型的项（terms depending on types），称二阶运算（second order operations）或二阶依赖（second order dependency）.

得到的这一系统称二阶类型lambda演算（second order typed lambda calculus），或$\lambda 2$.