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

Question

有路径依赖的类型,我认为这是可能的,表达了这样的语言作为警句或阿格达Scala中的几乎所有功能,但我不知道为什么斯卡拉不支持此更明确地像它非常漂亮,在其他领域(比如,DSLs)？我缺少的任何东西都像"没有必要"？

Answer 1

除了语法上的便利之外,单例类型,路径依赖类型和隐式值的组合意味着Scala对依赖类型的支持非常好,因为我试图在无形状中进行演示.

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

事实上,这是依赖方法类型编码的一个关键部分,它是在2.10之前逃离 Scala中的'面包末日'所需的(或者更早通过实验-Ydependent方法类型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.type和res3.type是单类型,因此比我们正在核实在RHS类型更精确).

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

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

在任何情况下,我都不认为这种轻微的域名限制可以用作对Scala作为依赖类型语言的地位的反对.如果是,那么对于Dependent ML(它只允许依赖于自然数值)也可以这样说,这将是一个奇怪的结论.

Answer 2

我认为这是因为(据我所知,在Coq校对助手中使用了依赖类型,它完全支持它们但仍然不是非常方便的)依赖类型是一种非常高级的编程语言功能,这很难做得对 - 并且可能导致实践中复杂性的指数爆炸.它们仍然是计算机科学研究的主题.