路径依赖类型和依赖类型之间有什么区别?

rig*_*old 9 scala path-dependent-type dependent-type

Scala具有路径依赖类型,但据说Scala不支持依赖类型.路径依赖类型和依赖类型之间有什么区别?

据我所知,路径依赖类型是一种依赖类型.

Luk*_*ytz 6

依赖类型是依赖于值的类型。路径依赖类型是一种特定类型的依赖类型,其中类型依赖于路径。

我不确定 Scala 社区之外是否存在术语“路径依赖类型”。无论如何,问题是,什么是路径?对于 Scala,这是在语言规范中定义的:基本上它是a.b.c...对非变量值的选择序列。

路径依赖类型是具有路径的类型,例如a.T

class A { type T; def f: T }
def f(a: A): a.T = a.f
Run Code Online (Sandbox Code Playgroud)

还有其他类型的依赖类型。例如,在 Scala 中,有一个未决的提案是向语言添加基于文字的类型,以便您可以编写val x: 42.type = 21 + 21.

为了对使用依赖类型的程序进行类型检查,类型系统(和编译器)需要了解这些值的语义及其操作。Scala 编译器知道选择的语义,可以决定两条路径是否相同。对于使用基于文字的类型的示例,需要扩展编译器以了解+对整数的操作意味着什么。