简介

最近由于正在研究直觉类型论以及同伦类型论, 因此特意挑选了 Scala 的 Dotty 编译器作为研究对象, 而由于 Dotty 所设计的依赖类型相较于 Coq, Agda, Idris 之类的语言来讲十分不直观, 导致写出一些带有大量依赖类型的函数则显得较为绕口, 因此本篇文章主要目的是找出一套通用的编码方式, 亦即找寻出 Scala 与 直觉类型论 之间的对应关系.

在 Dotty 中, Scala 是如何编码依赖类型的?

首先让我们从最简单的例子开始, 假设有一依赖函数类型 \(depfun\):

\[ depfun : \underset{(A : U)}{\Pi} \underset{(C : A \to U)}{\Pi} \underset{(x : A)}{\Pi} C(x) \]

且其表达式为:

\[ depfun_{A, C}(x) = x \]

然后现在我们能于 Scala 中写出这么一段代码:

1
2
3
trait C { type A; val x : A }
type PiType = (c : C) => c.A
val depfun : PiType = c => c.x

于这段代码里, 使用了 trait, type 以及 val 以描述依赖函数类型 depfun, 而 val depfun : PiType = c => c.xPiType 则代表着一个依赖函数类型 (\(\Pi\)-类型), (c : C) => c.x 部分则为一项 (表达式).

为什么 Scala 编码复杂的依赖类型显得如此困难?

没有全类多态的依赖类型

语法设计的问题