简介
最近由于正在研究直觉类型论以及同伦类型论, 因此特意挑选了 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
3trait 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.x 的 PiType 则代表着一个依赖函数类型 (\(\Pi\)-类型), (c : C) => c.x 部分则为一项 (表达式).
