114

有路径依赖类型，我认为可以在 Scala 中表达 Epigram 或 Agda 等语言的几乎所有特性，但我想知道为什么 Scala 不更明确地支持这一点，就像它在其他领域做得很好（比如, DSL) ? 我错过了什么，比如“没有必要”？

4

4 回答 4

160

除了语法便利之外，单例类型、路径依赖类型和隐式值的组合意味着 Scala 对依赖类型的支持非常好，正如我试图在shapeless中演示的那样。

Scala 对依赖类型的内在支持是通过路径依赖类型。这些允许类型依赖于通过对象（即值）图的选择器路径，如下所示，

scala> class Foo { class Bar }
defined class Foo

scala> val foo1 = new Foo
foo1: Foo = Foo@24bc0658

scala> val foo2 = new Foo
foo2: Foo = Foo@6f7f757

scala> implicitly[foo1.Bar =:= foo1.Bar] // OK: equal types
res0: =:=[foo1.Bar,foo1.Bar] = <function1>

scala> implicitly[foo1.Bar =:= foo2.Bar] // Not OK: unequal types
<console>:11: error: Cannot prove that foo1.Bar =:= foo2.Bar.
              implicitly[foo1.Bar =:= foo2.Bar]

在我看来，以上内容应该足以回答“Scala 是一种依赖类型的语言吗？”这个问题。积极的一面：很明显，这里我们有类型，这些类型通过作为它们的前缀的值来区分。

然而，人们经常反对 Scala 不是一种“完全”依赖类型的语言，因为它没有在 Agda、Coq 或 Idris 中发现的依赖求和和乘积类型作为内在函数。我认为这在一定程度上反映了对形式而非基础的固执，不过，我将尝试证明 Scala 比通常公认的更接近这些其他语言。

尽管有术语，但依赖和类型（也称为 Sigma 类型）只是一对值，其中第二个值的类型取决于第一个值。这在 Scala 中可以直接表示，

scala> trait Sigma {
     |   val foo: Foo
     |   val bar: foo.Bar
     | }
defined trait Sigma

scala> val sigma = new Sigma {
     |   val foo = foo1
     |   val bar = new foo.Bar
     | }
sigma: java.lang.Object with Sigma{val bar: this.foo.Bar} = $anon$1@e3fabd8

事实上，这是依赖方法类型编码的关键部分，需要在 Scala 2.10 之前（或更早通过实验性的 -Ydependent-method types Scala 编译器选项）逃离“末日面包店” 。

依赖产品类型（又名 Pi 类型）本质上是从值到类型的函数。它们是表示静态大小的向量和其他依赖类型编程语言的典型代表的关键。我们可以使用路径相关类型、单例类型和隐式参数的组合在 Scala 中对 Pi 类型进行编码。首先，我们定义一个特征，它将表示一个从 T 类型的值到 U 类型的函数，

scala> trait Pi[T] { type U }
defined trait Pi

我们可以定义一个使用这种类型的多态方法，

scala> def depList[T](t: T)(implicit pi: Pi[T]): List[pi.U] = Nil
depList: [T](t: T)(implicit pi: Pi[T])List[pi.U]

pi.U（注意在结果类型中使用路径相关类型List[pi.U]）。给定类型 T 的值，此函数将返回与该特定 T 值对应的类型的值的（n 个空）列表。

现在让我们为我们想要保持的功能关系定义一些合适的值和隐含的见证，

scala> object Foo
defined module Foo

scala> object Bar
defined module Bar

scala> implicit val fooInt = new Pi[Foo.type] { type U = Int }
fooInt: java.lang.Object with Pi[Foo.type]{type U = Int} = $anon$1@60681a11

scala> implicit val barString = new Pi[Bar.type] { type U = String }
barString: java.lang.Object with Pi[Bar.type]{type U = String} = $anon$1@187602ae

现在这是我们使用 Pi 类型的函数，

scala> depList(Foo)
res2: List[fooInt.U] = List()

scala> depList(Bar)
res3: List[barString.U] = List()

scala> implicitly[res2.type <:< List[Int]]
res4: <:<[res2.type,List[Int]] = <function1>

scala> implicitly[res2.type <:< List[String]]
<console>:19: error: Cannot prove that res2.type <:< List[String].
              implicitly[res2.type <:< List[String]]
                    ^

scala> implicitly[res3.type <:< List[String]]
res6: <:<[res3.type,List[String]] = <function1>

scala> implicitly[res3.type <:< List[Int]]
<console>:19: error: Cannot prove that res3.type <:< List[Int].
              implicitly[res3.type <:< List[Int]]

（请注意，这里我们使用 Scala 的<:<子类型见证运算符，而不是=:=因为res2.typeandres3.type是单例类型，因此比我们在 RHS 上验证的类型更精确）。

然而，在实践中，在 Scala 中，我们不会从编码 Sigma 和 Pi 类型开始，然后像在 Agda 或 Idris 中那样从那里开始。相反，我们将直接使用路径相关类型、单例类型和隐式。你可以找到很多关于这如何在无形中发挥作用的例子：大小的类型、可扩展的记录、全面的 HLists、废弃你的样板文件、通用拉链等。

我能看到的唯一剩下的反对意见是，在上述 Pi 类型的编码中，我们要求依赖值的单例类型是可表达的。不幸的是，在 Scala 中，这仅适用于引用类型的值，而不适用于非引用类型的值（尤其是 Int）。这是一种耻辱，但不是一个内在的困难：Scala 的类型检查器在内部表示非引用值的单例类型，并且已经进行了一些实验以使它们可以直接表达。在实践中，我们可以通过对自然数进行相当标准的类型级编码来解决这个问题。

无论如何，我不认为这种轻微的域限制可以用来反对 Scala 作为依赖类型语言的地位。如果是这样，那么对于 Dependent ML（它只允许依赖于自然数值）也可以这样说，这将是一个奇怪的结论。

于 2012-10-17T15:27:43.750 回答
6

我认为这是因为（根据我的经验，在 Coq 证明助手中使用了依赖类型，它完全支持它们但仍然不是以一种非常方便的方式）依赖类型是一种非常高级的编程语言特性，它真的很难做对了——并且在实践中可能导致复杂性呈指数级增长。它们仍然是计算机科学研究的主题。

于 2012-10-18T07:21:09.667 回答
3

我相信 Scala 的路径依赖类型只能表示 Σ-types，而不能表示 Π-types。这个：

trait Pi[T] { type U }

不完全是 Π 型。根据定义，Π型或依存积是结果类型取决于参数值的函数，表示全称量词，即∀x: A, B(x)。然而，在上面的例子中，它只依赖于类型 T，而不依赖于这个类型的某个值。Pi trait 本身是一个 Σ 型，一个存在量词，即∃x: A, B(x)。在这种情况下，对象的自引用充当量化变量。但是，当作为隐式参数传入时，它会简化为普通类型函数，因为它是按类型解析的。Scala 中依赖产品的编码可能如下所示：

trait Sigma[T] {
  val x: T
  type U //can depend on x
}

// (t: T) => (∃ mapping(x, U), x == t) => (u: U); sadly, refinement won't compile
def pi[T](t: T)(implicit mapping: Sigma[T] { val x = t }): mapping.U

这里缺少的部分是将字段 x 静态约束到期望值 t 的能力，有效地形成一个表示类型 T 中所有值的属性的方程。与我们的 Σ 类型一起，用于表示具有给定属性的对象的存在，形成逻辑，其中我们的方程是一个需要证明的定理。

附带说明一下，在实际情况下，定理可能非常重要，以至于它无法从代码中自动推导出来，或者在没有大量工作的情况下无法解决。甚至可以用这种方式制定黎曼假设，只是发现签名不可能在没有实际证明的情况下实现，永远循环或抛出异常。

于 2017-04-10T21:23:40.550 回答
1

问题是关于更直接地使用依赖类型的特性，在我看来，拥有比 Scala 提供的更直接的依赖类型方法会有好处。
当前的答案试图在类型理论层面上争论这个问题。我想对其进行更务实的旋转。这可以解释为什么人们在 Scala 语言中对依赖类型的支持程度存在分歧。我们可能有一些不同的定义。（不是说一个是对的，一个是错的）。

这并不是试图回答将 Scala 变成 Idris 之类的东西有多么容易（我想很难）或编写一个库来为 Idris 之类的功能提供更直接的支持（就像singletons尝试在 Haskell 中一样）。

相反，我想强调 Scala 和 Idris 之类的语言之间的语用差异。
什么是值和类型级别表达式的代码位？Idris 使用相同的代码，Scala 使用非常不同的代码。

Scala（类似于 Haskell）可能能够编码大量类型级别的计算。这由像shapeless. 这些库使用一些非常令人印象深刻和聪明的技巧来做到这一点。但是，它们的类型级别代码（当前）与值级别表达式完全不同（我发现在 Haskell 中这种差距更接近一些）。Idris 允许在类型级别 AS IS 上使用值级别表达式。

明显的好处是代码重用（如果您在两个地方都需要它们，则不需要将类型级别表达式与值级别分开编写）。编写价值级别的代码应该更容易。不必处理像单例这样的黑客应该更容易（更不用说性能成本了）。你不需要学两件事你学一件事。在务实的层面上，我们最终需要更少的概念。类型同义词，类型族，函数，......函数怎么样？在我看来，这种统一的好处要深入得多，而且不仅仅是语法上的便利。

考虑经过验证的代码。请参阅：
https
://github.com/idris-lang/Idris-dev/blob/v1.3.0/libs/contrib/Interfaces/Verified.idr 类型检查器验证单子/仿函数/应用定律的证明，证明是关于实际的monad/functor/applicative 的实现，而不是一些可能相同或不同的编码类型级别等价物。最大的问题是我们在证明什么？

我也可以使用聪明的编码技巧来完成同样的事情（请参阅下面的 Haskell 版本，我还没有看到 Scala 的版本）
https://blog.jle.im/entry/verified-instances-in-haskell.html
https:// github.com/rpeszek/IdrisTddNotes/wiki/Play_FunctorLaws
除了类型非常复杂以至于很难看到规律，值级别表达式被转换（自动但仍然）到类型级别的东西，你也需要相信这种转换. 所有这些都存在错误的余地，这有点违背编译器作为证明助手的目的。

（2018.8.10 编辑）谈到证明辅助，这是 Idris 和 Scala 之间的另一个重大区别。Scala（或 Haskell）中没有任何东西可以阻止编写不同的证明：

case class Void(underlying: Nothing) extends AnyVal //should be uninhabited
def impossible() : Void = impossible()

而 Idris 有total关键字阻止这样的代码编译。

尝试统一值和类型级别代码的 Scala 库（如 Haskell singletons）将是对 Scala 对依赖类型的支持的有趣测试。由于路径相关的类型，这样的库在 Scala 中可以做得更好吗？

我对 Scala 太陌生，无法自己回答这个问题。

于 2018-08-06T02:40:03.357 回答