为什么scala没有明确支持依赖types的任何原因？
有依赖于path的types，我认为可以在Scala中expression几乎所有像Epigram或Agda这样的语言的特性，但是我想知道为什么Scala不能更明确地支持这个语言，就像在其他领域做的很好（比如说，DSL）？ 我错过了什么，像“这是没有必要的”？
除了单纯的句法，单身types，path依赖types和隐式值的组合意味着Scala对依赖types的支持非常好，正如我试图用无定形的方式演示的。
Scala对依赖types的内在支持是通过path依赖的types 。 这些允许一个types依赖于一个select器path通过像这样的对象（即值）图，
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] 在我看来，以上应该足以回答“斯卡拉是一种依赖型语言吗？”这个问题。 在积极的方面：很明显，在这里我们有types是由它们的前缀的值区分。
然而，人们经常反对Scala并不是一个“完全”依赖types的语言，因为它不具有在Agda或Coq或Idris中作为内在函数发现的依赖和和产品types 。 我认为这在某种程度上反映了对基础的forms的固定，但是我会试着certificateScala比其他语言更接近于通常所承认的语言。
尽pipe有术语，依赖和types（也称为西格玛types）只是一对值，其中第二个值的types取决于第一个值。 这在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
事实上，这是依赖方法types编码的一个关键部分， 它需要从 2.10之前的Scala中的“Doom面包” （或更早的通过实验 – 独立方法typesScala编译器选项）中逃脱。
相关产品types（又名Pitypes）实质上是从值到types的函数。 它们对于静态大小的向量以及用于依赖types编程语言的其他海报儿童的表示是关键的。 我们可以使用path依赖types，单例types和隐式参数的组合来对Scala中的Pitypes进行编码。 首先我们定义一个将要从T型值到U型值的函数，
scala> trait Pi[T] { type U } defined trait Pi
我们可以定义一个使用这种types的多态方法，
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]
（注意在结果typesList[pi.U]使用path相关typespi.U ）。 给定一个typesT的值，这个函数将返回一个（n空）与那个特定的T值对应的types值的列表。
现在让我们为我们想要保留的函数关系定义一些合适的值和隐含的见证人，
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型使用function，
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的<:<子types见证运算符而不是=:=因为res2.type和res3.type是单例types，因此比我们在RHS上validation的types更精确。
然而，在实践中，在Scala中，我们不会从编码Sigma和Pitypes开始，然后像在Agda或Idris中那样继续。 相反，我们会直接使用path依赖types，单例types和implicits。 你可以find很多这样的例子，如何在无形中发挥作用： 大小的types ， 可扩展的logging ， 全面的HList ， 废弃样板 ， 通用拉链等。
我能看到的唯一剩余的反对意见是，在Pitypes的上述编码中，我们要求可以表示依赖值的单例types。 不幸的是，在Scala中，这只能用于引用types的值，而不能用于非引用types的值（特别是.Int）。 这是一个耻辱，但不是一个固有的困难：Scala的types检查器在内部表示非参考值的单例types，并且已经进行了一些直接可expression的实验 。 在实践中，我们可以用相当标准的自然数的types级编码来解决这个问题。
无论如何，我不认为这种轻微的域名限制可以用来作为斯卡拉作为一种依赖型语言的地位的反对意见。 如果是这样，那么对于依赖ML（它只允许依赖于自然数值）也可以这么说，这将是一个奇怪的结论。
我认为这是因为（正如我从经验中所知道的，在Coqcertificate助手中使用依赖types，完全支持它们，但仍然不是非常方便的方式）依赖types是非常高级的编程语言特性，得到正确的 – 在实践中可能会导致复杂的指数式爆炸。 他们仍然是计算机科学研究的主题。
我相信，斯卡拉的path依赖types只能表示Σ型，而不是Π型。 这个：
trait Pi[T] { type U }
不完全是一个Π型。 根据定义，Π型或依赖型产品是一个函数，其结果types取决于参数值，表示通用量词，即∀x：A，B（x）。 但是，在上面的情况下，它只依赖于typesT，而不是这个types的某个值。 Pi特征本身是一个Σ型，一个存在量词，即∃x：A，B（x）。 在这种情况下，对象的自我引用是作为量化的variables。 当作为隐含参数传入时，它会减less为普通types的函数，因为它是按types分解的。 在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的能力，有效地形成了代表所有居住typesT的值的属性的方程。与我们的Σ-types一起用来表示具有给定属性的对象的存在，逻辑形成，其中我们的方程是一个要certificate的定理。
在一个侧面说明，在实际情况下，定理可能是非常平凡的，直到它不能自动从代码中派生出来，或者在没有大量努力的情况下解决。 甚至可以用这种方式来制定黎曼假说，只有find不实际certificate的签名，永远循环或抛出exception，才能实现。
