scala为什么不明确支持依赖类型的任何原因？

Question

存在路径依赖类型，我认为可以在 Scala 中表达 Epigram 或 Agda 等语言的几乎所有功能，但我想知道为什么 Scala 不支持this 更明确地喜欢它做得很好在其他领域（例如，DSL）？ 像“没有必要”这样我缺少什么？

Answer 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 还太陌生，无法自己回答这个问题。

Answer 2

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

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 中所有值的属性的方程。与我们的 Σ 类型一起，用于表示给定对象的存在属性，形成逻辑，其中我们的方程是一个需要证明的定理。

在旁注中，在实际情况下，定理可能非常重要，甚至无法从代码中自动推导出来，也无法在不付出大量努力的情况下解决。甚至可以用这种方式制定黎曼假设，结果发现签名不可能在没有实际证明的情况下实现，永远循环或抛出异常。

Answer 3

撇开语法方便不谈，单例类型、路径依赖类型和隐式值的组合意味着 Scala 对依赖类型的支持出奇的好，正如我在 shapeless 中尝试演示的那样。

Scala 对依赖类型的内在支持是通过path-dependent types。这些允许类型依赖于通过对象（即值）图的选择器路径，就像这样，

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 中那样具有 dependent sum and product types 作为内在函数。我认为这在一定程度上反映了对形式而非基础的执着，不过，我将尝试证明 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 之前的 encoding of dependent method types which is needed to escape from the 'Bakery of Doom' 的关键部分（或更早通过实验性的 -Ydependent-method types Scala 编译器选项）。

从属产品类型（又名 Pi 类型）本质上是从值到类型的函数。它们是表示statically sized vectors 和其他依赖类型编程语言的典型代表的关键。我们可以使用路径相关类型、单例类型和隐式参数的组合在 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]

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

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

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.type 和 res3.type 是单例类型，因此比我们在 RHS 上验证的类型更精确）。

然而，在实践中，在 Scala 中，我们不会从编码 Sigma 和 Pi 类型开始，然后像在 Agda 或 Idris 中那样从那里开始。相反，我们将直接使用路径相关类型、单例类型和隐式。你可以找到很多关于这在 shapeless 中如何发挥作用的例子：sized types、extensible records、comprehensive HLists、scrap your boilerplate、generic Zippers 等等。

我能看到的唯一反对意见是，在上述 Pi 类型的编码中，我们要求依赖值的单例类型是可表达的。不幸的是，在 Scala 中，这仅适用于引用类型的值，而不适用于非引用类型的值（尤其是 Int）。这是一个耻辱，但不是一个内在的困难：Scala 的类型检查器在内部表示非引用值的单例类型，并且有一个 couple 或 experiments 使它们可以直接表达。在实践中，我们可以通过fairly standard type-level encoding of the natural numbers 来解决这个问题。

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

Answer 4

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