114

パス依存型があり、Epigram や Agda などの言語のほぼすべての機能を Scala で表現することは可能だと思いますが、他の分野で非常にうまく機能するように、なぜ Scala がこれをより明示的にサポートしないのか疑問に思っています (たとえば、 、DSL) ? 「必要ない」など、私が見逃しているものはありますか？

4

4 に答える 4

160

構文上の利便性はさておき、シングルトン型、パス依存型、および暗黙の値の組み合わせは、私がshapelessで実証しようとしたように、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 に組み込まれている依存型の sum や product 型を持っていないため、Scala は「完全な」依存型言語ではないという反論がよくあります。これはある程度、基本よりも形式に固執していることを反映していると思いますが、Scala が一般に認識されているよりもこれらの他の言語にはるかに近いことを示してみます。

用語にかかわらず、従属合計型 (シグマ型とも呼ばれます) は、2 番目の値の型が最初の値に依存する単純な値のペアです。これは 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-method types Scala コンパイラ オプションを介して)の「Bakery of Doom」から逃れるために必要な依存メソッド型のエンコーディングの重要な部分です。

従属プロダクト タイプ (別名 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]]

(ここでは、 andがシングルトン型であるため、RHS で検証している型よりも正確であるという理由では<:<なく、Scala のサブタイプ監視演算子を使用していることに注意してください)。=:=res2.typeres3.type

しかし実際には、Scala では、Agda や Idris のように Sigma や Pi の型をエンコードすることから始めて、そこから先に進むことはありません。代わりに、パス依存型、シングルトン型、および暗黙型を直接使用します。これが shapeless でどのように機能するかを示す多数の例を見つけることができます:サイズ化された型、拡張可能なレコード、包括的な HLists、ボイラープレートを破棄する、一般的な Zippersなど。

私が見ることができる唯一の異議は、上記の Pi​​ 型のエンコーディングでは、依存する値のシングルトン型を表現可能にする必要があるということです。残念ながら、Scala では、これは参照型の値に対してのみ可能であり、非参照型 (特に Int など) の値に対しては可能ではありません。これは残念ですが、本質的な問題ではありません。Scala の型チェッカーは非参照値のシングルトン型を内部的に表現しており、それらを直接表現できるようにするための実験がいくつか行われています。実際には、自然数のかなり標準的な型レベルのエンコーディングで問題を回避できます。

いずれにせよ、このわずかなドメイン制限が依存型言語としての Scala の地位に対する反論として使用できるとは思いません。もしそうなら、奇妙な結論である従属ML（自然数の値への依存のみを許可する）についても同じことが言えます。

于 2012-10-17T15:27:43.750 に答える
6

私はそれが（経験から知っているように、依存型を完全にサポートしているが、まだ非常に便利な方法ではないCoqプルーフアシスタントで依存型を使用したことがある）依存型が非常に高度なプログラミング言語機能であるためだと思います実際には、複雑さが指数関数的に爆発する可能性があります。それらは今でもコンピュータ サイエンス研究のトピックです。

于 2012-10-18T07:21:09.667 に答える