2

質問に対する私の考えは次のとおりです。誰でも確認、否定、または詳しく説明できますか?

は書いた

Scala は共変 List[A]を に割り当てられた GLB ⊤ と統合しません。割り当ての方向が重要な「二重統合」をサブタイプ化すること List[Int]で bcz は承知しています。したがって、またはからの代入を受け入れることができないNoneタイプOption[⊥](すなわちOption[Nothing])が必要Nilです。そのため、値制限の問題は方向性のない統一に由来し、グローバルな二重統一は、上記にリンクされた最近の研究まで決定できないと考えられていました。List[Nothing]Option[Int]List[Int]

上記のコメントのコンテキストを表示することをお勧めします。

ML の値の制限により、特にカリー化された関数 (関数型プログラミングで重要) を部分的に適用する場合など、パラメトリック ポリモーフィズムを許可しない場合 (以前はまれであると考えられていましたが、より一般的である可能性があります) )、代替の型付けソリューションは、関数型プログラミングと命令型プログラミングの間の階層化を作成し、モジュラー抽象型のカプセル化を破るためです。Haskell には、類似の二重単形化制限があります。OCaml では制限が緩和されている場合があります。これらの詳細のいくつかについて詳しく説明しました。

編集:上記の引用で表現された私の最初の直感(サブタイプによって値の制限が取り除かれる可能性がある)は間違っています。回答 IMO は問題をよく説明しており、アレクセイ、アンドレアス、または私のものを含むセットのどれを選択するのが最良の回答であるかを判断できません。IMO それらはすべて価値があります。

4

3 に答える 3

3

前に説明したように、値の制限 (または同様のもの) の必要性は、パラメトリック ポリモーフィズムと可変参照 (またはその他の特定の効果) を組み合わせるときに発生します。これは、言語に型推論があるかどうか、または言語がサブタイプを許可するかどうかとは完全に無関係です。次のような標準的な反例

let r : ∀A.Ref(List(A)) = ref [] in
r := ["boo"];
head(!r) + 1

型注釈を省略する機能や、量化された型に境界を追加する機能の影響を受けません。

したがって、F<: への参照を追加するときは、健全性を失わないように値の制限を課す必要があります。同様に、MLsub は値の制限を取り除くことができません。ポリモーフィック型を持つ値の定義を記述する方法さえないため、Scala はすでにその構文を通じて値の制限を適用しています。

于 2018-02-03T16:15:17.140 に答える
1

編集:この回答は以前は正しくありませ んでした。アンドレアスとアレクセイの回答の下にあるコメントから新しい理解を得るために、以下の説明を完全に書き直しました。

archive.is でのこのページの編集履歴とアーカイブの履歴は、私の以前の誤解と議論の記録を提供します。新しい回答を削除して書き込むのではなく、編集することを選択したもう 1 つの理由は、この回答に対するコメントを保持することです。IMO、この回答はまだ必要です。アレクセイはスレッドのタイトルに正しくかつ最も簡潔に回答していますが、アンドレアスの詳細は私が理解を得るのに最も役立ちましたが、素人の読者は別のより全体的なものを必要とするかもしれないと思います.ジェネレーティブ エッセンス) の説明を使用して、問題をある程度深く理解することができます。また、他の回答は全体論的な説明がどれほど複雑であるかをあいまいにしていると思います。素朴な読者にそれを味わうオプションを与えてほしい.


値の制限は、参照される1 タイプのパラメーター化されたオブジェクト2の突然変異がある場合に発生します。次のMLton コード例は、値の制限がないと発生する型の安全性を示しています。

val r: 'a option ref = ref NONE
val r1: string option ref = r
val r2: int option ref = r
val () = r1 := SOME "foo"
val v: int = valOf (!r2)

によって参照されるオブジェクトに含まれる値 ( に似ています)はNONE、多相型 を持つため、型パラメーターの具体的な型を持つ参照に割り当てることができます。上記の例に示すように、どちらによって参照されている同じオブジェクトが両方に割り当てられており、参照を介して値を書き込む (つまり変更する) ことができ、参照を介して値として読み取ることができるため、型の安全性が損なわれる可能性があります。上記の例では、値の制限によりコンパイラ エラーが発生します。nullr'ara'rstring option refint option refstringr1intr2

型付けの複雑さは、参照 (およびそれが指すオブジェクト) の型パラメーター (別名型変数) の (再) 定量化 (つまり、バインディングまたは決定) を防止するために発生します。以前に別のタイプで定量化された参照。

このような (間違いなく当惑し、複雑な) ケースは、たとえば、連続する関数アプリケーション (別名呼び出し)がそのような参照の同じインスタンスを再利用する場合に発生します。IOW、関数が適用されるたびに参照の型パラメーター (オブジェクトに関連する) が (再) 定量化されるが、参照の同じインスタンス (および参照が指すオブジェクト) が後続のアプリケーションごとに再利用されるケース関数の (および定量化)。

接線的に言えば、これらの発生は、明示的な全称量指定子 ∀ の欠如(暗黙的なランク 1 のプレネックスの語彙範囲の量化は、またはコルーチンなどの構成によって字句評価順序から取り除かれるためlet) と、間違いなくより大きな不規則性 ( Scala と比較して) ML の値制限で安全でないケースが発生する可能性がある場合:

アンドレアスは書いた

残念ながら、ML は通常、その構文で量指定子を明示的にせず、型付け規則でのみ明示します。

参照されたオブジェクトを再利用することは、たとえばlet、数学表記法に類似した式の場合に望ましく、置換のインスタンス化を作成して評価する必要があるのは、句内で 2 回以上語彙的に置換される可能性がある場合でも1回だけです。したがって、たとえば、関数適用が句内で (字句的にもそうでなくても) として評価される場合、置換の型パラメーターはアプリケーションごとに再定量化されます (置換のインスタンス化は字句的にのみであるため)。inin関数アプリケーション内で)、すべてのアプリケーションが問題のある型パラメーターを 1 回だけ定量化することを強制されない場合 (つまり、問題のある型パラメーターが多態的であることを禁止する)、型の安全性が失われる可能性があります。

値の制限は、型システムを単純化するために、すべての安全でないケースを防止すると同時に、一部の (以前はまれであると考えられていた) 安全なケースも防止するための ML の妥協案です。値の制限は、より良い妥協案と見なされます。なぜなら、安全なケースを制限しない、または多くの安全なケースを制限しない、より複雑な型付けアプローチの初期の (時代遅れの? ) 経験が、命令型プログラミングと純粋な関数型 (別名アプリケーション型) プログラミングとの間の分岐を引き起こし、一部がリークしたためです。 ML functor モジュールでの抽象型のカプセル化の。私はいくつかの情報源を引用し、ここで詳しく説明しました. 接線ではありますが、私は初期の反論が分岐は、概念的に部分的なアプリケーションが既に評価された状態でクロージャーを形成しないため、名前による呼び出し (たとえば、必要に応じてメモ化された場合の Haskell 風の遅延評価) には値の制限がまったく必要ないという事実に反しています。また、名前による呼び出しは、モジュラー合成推論に必要であり、純粋性と組み合わせると、モジュラー (圏等式推論) 効果の制御と合成が必要になります。名前による呼び出しに対するモノモーフィゼーション制限の引数は、実際には約です型注釈を強制しますが、最適なメモ化 (別名共有) が必要なときに明示的であることは、モジュール性と読みやすさのために注釈が必要であることを考えると、間違いなく負担が少なくなります。値による呼び出しは細かい歯の櫛レベルの制御であるため、その低レベルの制御が必要な場合は、おそらく値の制限を受け入れる必要があります。応用設定. ただし、この 2 つを同じプログラミング言語でスムーズかつエレガントな方法で階層化/分離できるかどうかはわかりません。代数的効果は、ML などの CBV 言語で実装でき、値の制限を回避できます。IOW、値の制限がコードに影響している場合、おそらくそれが原因ですあなたのプログラミング言語とライブラリには、効果を処理するための適切なメタモデルがありません

Scala は、そのようなすべての参照に対して構文上の制限を行います。これは、ML の値の制限と同じか、さらに多くのケース (制限されていなければ安全であろう)を制限する妥協案ですが、ML の値制限よりも規則的です。値の制限に関するエラー メッセージについて頭を悩ませています。Scala では、そのような参照を作成することは決して許可されていません。したがって、Scala では、型パラメーターが量化されたときに参照の新しいインスタンスが作成される場合しか表現できません。注意OCamlは値の制限を緩和する場合があります。

Scala と ML の両方が、参照が不変であると宣言することを可能にしないことに注意してください1val。変更できない参照の制限は必要ないことに注意してください。

複雑な型付けのケースを発生させるために参照型1letの可変性が必要な理由は、非パラメータ化オブジェクト (つまり、notNoneまたはNil4 but代わりに、たとえば aOption[String]またはList[Int]) の場合、参照には含まれません。ポリモーフィック型 (それが指すオブジェクトに関連する) であるため、再数量化の問題は決して発生しません。したがって、問題のあるケースは、ポリモーフィック オブジェクトを使用したインスタンス化が原因であり、その後、再数量化されたコンテキストで新しく数量化されたオブジェクトを割り当てる (つまり、参照型を変更する) と、その後の (によって指されるオブジェクト) 参照からの逆参照 (読み取り) が続きます。再定量化されたコンテキスト。前述のように、再数量化された型パラメーターが競合すると、型付けの複雑さが生じ、安全でないケースを防止/制限する必要があります。

ふぅ!リンクされた例を確認せずにそれを理解した場合、私は感銘を受けました.


1 IMO が「参照されるオブジェクトの可変性」と「参照型の可変性」の代わりに「可変参照」というフレーズを使用すると、より混乱する可能性があります。ポインターによって参照されます—参照が指しているポインターの可変性を参照していません。一部のプログラミング言語は、プリミティブ型の場合に、参照またはそれらが指すオブジェクトを変更する選択を許可していない場合、明示的に区別さえしません。

2 ここで、ファーストクラスの関数を許可するプログラミング言語では、オブジェクトは関数でさえあります。

3 オブジェクトが実際に持っている型ではない、静的に (つまり、コンパイル時に) 決定された型に関する推定を使用して、参照されるオブジェクトにアクセス (読み取りまたは書き込み) することによる、実行時のセグメンテーション違反を防ぐため。

4 どちらがNONEであり、[]それぞれ ML にあります。

于 2018-02-03T06:50:22.647 に答える