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

Any reason why scala does not explicitly support dependent types?

提问by Ashkan Kh. Nazary

There are path dependent types and I think it is possible to express almost all the features of such languages as Epigram or Agda in Scala, but I'm wondering why Scala does not support thismore explicitly like it does very nicely in other areas (say, DSLs) ? Anything I'm missing like "it is not necessary" ?

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

回答by Miles Sabin

Syntactic convenience aside, the combination of singleton types, path-dependent types and implicit values means that Scala has surprisingly good support for dependent typing, as I've tried to demonstrate in shapeless.

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

Scala's intrinsic support for dependent types is via path-dependent types. These allow a type to depend on a selector path through an object- (ie. value-) graph like so,

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]

In my view, the above should be enough to answer the question "Is Scala a dependently typed language?" in the positive: it's clear that here we have types which are distinguished by the values which are their prefixes.

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

However, it's often objected that Scala isn't a "fully" dependently type language because it doesn't have dependent sum and product typesas found in Agda or Coq or Idris as intrinsics. I think this reflects a fixation on form over fundamentals to some extent, nevertheless, I'll try and show that Scala is a lot closer to these other languages than is typically acknowledged.

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

Despite the terminology, dependent sum types (also known as Sigma types) are simply a pair of values where the type of the second value is dependent on the first value. This is directly representable in 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@e3fabd8

and in fact, this is a crucial part of the encoding of dependent method types which is needed to escape from the 'Bakery of Doom'in Scala prior to 2.10 (or earlier via the experimental -Ydependent-method types Scala compiler option).

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

Dependent product types (aka Pi types) are essentially functions from values to types. They are key to the representation of statically sized vectorsand the other poster children for dependently typed programming languages. We can encode Pi types in Scala using a combination of path dependent types, singleton types and implicit parameters. First we define a trait which is going to represent a function from a value of type T to a type U,

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

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

We can than define a polymorphic method which uses this type,

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

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]

(note the use of the path-dependent type pi.Uin the result type List[pi.U]). Given a value of type T, this function will return a(n empty) list of values of the type corresponding to that particular T value.

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

Now let's define some suitable values and implicit witnesses for the functional relationships we want to hold,

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

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@60681a11

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

And now here is our Pi-type-using function in action,

现在这是我们使用 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]]

(note that here we use Scala's <:<subtype-witnessing operator rather than =:=because res2.typeand res3.typeare singleton types and hence more precise than the types we are verifying on the RHS).

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

In practice, however, in Scala we wouldn't start by encoding Sigma and Pi types and then proceeding from there as we would in Agda or Idris. Instead we would use path-dependent types, singleton types and implicits directly. You can find numerous examples of how this plays out in shapeless: sized types, extensible records, comprehensive HLists, scrap your boilerplate, generic Zippersetc. etc.

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

The only remaining objection I can see is that in the above encoding of Pi types we require the singleton types of the depended-on values to be expressible. Unfortunately in Scala this is only possible for values of reference types and not for values of non-reference types (esp. eg. Int). This is a shame, but not an intrinsic difficulty: Scala's type checker represents the singleton types of non-reference values internally, and there have been a coupleof experimentsin making them directly expressible. In practice we can work around the problem with a fairly standard type-level encoding of the natural numbers.

我能看到的唯一剩下的反对意见是，在上述 Pi 类型的编码中，我们要求依赖值的单例类型是可表达的。不幸的是，在 Scala 中，这仅适用于引用类型的值，而不适用于非引用类型的值（例如 Int）。这是一种耻辱，而不是固有的困难：Scala的类型检查代表内部的单类型的非参考值的，而且已经出现了夫妇的实验中让他们直接表达。在实践中，我们可以通过自然数的相当标准的类型级编码来解决这个问题。

In any case, I don't think this slight domain restriction can be used as an objection to Scala's status as a dependently typed language. If it is, then the same could be said for Dependent ML (which only allows dependencies on natural number values) which would be a bizarre conclusion.

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

回答by Robin Green

I would assume it is because (as I know from experience, having used dependent types in the Coq proof assistant, which fully supports them but still not in a very convenient way) dependent types are a very advanced programming language feature which is really hard to get right - and can cause an exponential blowup in complexity in practice. They're still a topic of computer science research.

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

回答by P. Frolov

I believe that Scala's path-dependent types can only represent Σ-types, but not Π-types. This:

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

trait Pi[T] { type U }

is not exactly a Π-type. By definition, Π-type, or dependent product, is a function which result type depends on argument value, representing universal quantifier, i.e. ?x: A, B(x). In the case above, however, it depends only on type T, but not on some value of this type. Pi trait itself is a Σ-type, an existential quantifier, i.e. ?x: A, B(x). Object's self-reference in this case is acting as quantified variable. When passed in as implicit parameter, however, it reduces to an ordinary type function, since it is resolved type-wise. Encoding for dependent product in Scala may look like the following:

不完全是 Π 型。根据定义，Π-type，或依赖积，是一个结果类型取决于参数值的函数，表示全称量词，即?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 

The missing piece here is an ability to statically constraint field x to expected value t, effectively forming an equation representing the property of all values inhabiting type T. Together with our Σ-types, used to express the existence of object with given property, the logic is formed, in which our equation is a theorem to be proven.

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

On a side note, in real case theorem may be highly nontrivial, up to the point where it cannot be automatically derived from code or solved without significant amount of effort. One can even formulate Riemann Hypothesis this way, only to find the signature impossible to implement without actually proving it, looping forever or throwing an exception.

附带说明一下，在实际情况下，定理可能非常重要，直到它无法从代码中自动导出或在不付出大量努力的情况下解决。人们甚至可以用这种方式来表述黎曼假设，结果却发现签名不可能在没有实际证明的情况下实现，永远循环或抛出异常。

回答by robert_peszek

The question was about using dependently typed feature more directly and, in my opinion, there would be a benefit in having a more direct dependent typing approach than what Scala offers.
Current answers try to argue the question on type theoretical level. I want to put a more pragmatic spin on it. This may explain why people are divided on the level of support of dependent types in the Scala language. We may have somewhat different definitions in mind. (not to say one is right and one is wrong).

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

This is not an attempt to answer the question how easy would it be to turn Scala into something like Idris (I imagine very hard) or to write a library offering more direct support for Idris like capabilities (like singletonstries to be in Haskell).

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

Instead, I want to emphasize the pragmatic difference between Scala and a language like Idris.
What are code bits for value and type level expressions? Idris uses the same code, Scala uses very different code.

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

Scala (similarly to Haskell) may be able to encode lots of type level calculations. This is shown by libraries like shapeless. These libraries do it using some really impressive and clever tricks. However, their type level code is (currently) quite different from value level expressions (I find that gap to be somewhat closer in Haskell). Idris allows to use value level expression on the type level AS IS.

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

The obvious benefit is code reuse (you do not need to code type level expressions separately from value level if you need them in both places). It should be way easier to write value level code. It should be easier to not have to deal with hacks like singletons (not to mention performance cost). You do not need to learn two things you learn one thing. On a pragmatic level, we end up needing fewer concepts. Type synonyms, type families, functions, ... how about just functions? In my opinion, this unifying benefits go much deeper and are more than syntactic convenience.

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

Consider verified code. See:
https://github.com/idris-lang/Idris-dev/blob/v1.3.0/libs/contrib/Interfaces/Verified.idr
Type checker verifies proofs of monadic/functor/applicative laws and the proofs are about actual implementations of monad/functor/applicative and not some encoded type level equivalent that may be the same or not the same. The big question is what are we proving?

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

The same can me done using clever encoding tricks (see the following for Haskell version, I have not seen one for Scala)
https://blog.jle.im/entry/verified-instances-in-haskell.html
https://github.com/rpeszek/IdrisTddNotes/wiki/Play_FunctorLaws
except the types are so complicated that it is hard to see the laws, the value level expressions are converted (automatically but still) to type level things and you need to trust that conversion as well. There is room for error in all of this which kinda defies the purpose of compiler acting as a proof assistant.

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

(EDITED 2018.8.10) Talking about proof assistance, here is another big difference between Idris and Scala. There is nothing in Scala (or Haskell) that can prevent from writing diverging proofs:

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

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

while Idris has totalkeyword preventing code like this from compiling.

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

A Scala library that tries to unify value and type level code (like Haskell singletons) would be an interesting test for Scala's support of dependent types. Can such library be done much better in Scala because of path-dependent types?

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

I am too new to Scala to answer that question myself.

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