問題タブ [parametric-polymorphism]

プログラミング言語における型とポリモーフィズムに関する論文を読んで、Scala を使用して型メンバーの同様の全称量化を表現できるのではないかと思いました。紙の例：

これは一般的な同一性関数の型であり、紙の言語Funでの次の例は正しかった:

Scalaで同様のことを表現する方法はありますか?

これは type constructor と同じではありません。これは、がジェネリック関数の型であるtype GenericId[A] = A => A場合の型操作であるためです。∀A.A ↦ A

企業も人もいます。ユーザーは、ビジネスについて「いいね！」したり、コメントを投稿したりできますが、同じことは個人には起こりません。ユーザーがビジネスについて何かを投稿したり、いいねtarget!

ここで、あるプロパティを満たす(またはより多くの型の魅力を持つ)T | P[T]型パラメーターを意味する表記法を考案しています。コードのどこかで、次のような宣言が必要です。TP[T]T :|: P[T]

これらのオブジェクトは実際には証拠であり、Haskell 型クラスのようなものです。したがって、これはチェックを入力します：

しかし、これではありません：

Scala に関する私の知識が許す限り、この特定の状況を満足のいく方法でモデル化することはできません。ビジネスは次のようなものではないため、これはサブタイピングではないと主張します。

実際のところ、それは非常に望ましいことBusinessですPost. この関係は、実際には と の両方の外にPostありBusinessます。その上、上記のコードは2回Businessから継承しているため、そもそもコンパイルすらしないと思います。TargetingRelation洞察は大歓迎です。

related :クラス型パラメーターにバインドされたコンテキストを使用する

C++ と Java は、パラメトリック ポリモーフィズムの処理方法に類似点があります。どちらも、型パラメーターを通常の関数またはメソッドに推論しますが、プログラマーはコンストラクターを呼び出すときに型パラメーターを明示的に指定する必要があります (ただし、これは Java 7 で変更されました)。

この動作の背後にある技術的な理由は何ですか?

編集：これはScalaにも当てはまると誤って考えました。Java の例を次に示します。

これらはどちらも有効ですが、最初のものは ではなく「生の型」を作成しFoo<Integer>、未チェックの代入を実行します。

私はどのように機能するかを理解しようとしてNextMethod()います。S3 クラス システムについて私が見つけた最も詳細な説明は、Chambers & Hastie (edts.) のStatistical Models in S (1993 年、Chapman & Hall) にありますが、NextMethod呼び出しに関する部分は少しあいまいです。以下は、私が理解しようとしている関連する段落です (pp. 268-269)。

への呼び出しの結果として呼び出されるメソッドに目を向けると NextMethod()、これらのメソッドは、前のメソッドから特別な呼び出しで呼び出されたかのように動作します。継承されたメソッドの呼び出しの引数は、現在のメソッドの呼び出し (したがって、ジェネリックの呼び出し) と同じ数、順序、および実引数名になります。ただし、引数の式は、現在のメソッドの対応する仮引数の名前です。たとえば、式print(ratings)がメソッドを呼び出したとしますprint.ordered()。このメソッドが を呼び出すとき 、これはフォームのへNextMethod()の呼び出しと同等です。ここで、は のフレーム内にあり ます。複数の引数が仮引数に一致する場合"print.factor()print.factor(x)xxprint.ordered()..."、これらの引数は、継承されたメソッドの呼び出しで表されます y 特別な名前 " ..1"、" ..2" など。エバリュエーターはこれらの名前を認識し、適切に処理します (例については、476 ページを参照してください)。

このやや微妙な定義は、S における関数呼び出しのセマンティクスがメソッドの使用にできるだけきれいに引き継がれるようにするために存在します (Becker、Chambers、および Wilks のThe New S Language、354 ページを比較してください)。特に：

• NextMethod()引数は、呼び出された時点での現在の値とともに、現在のメソッドから継承されたメソッドに渡されます。
• 遅延評価は引き続き有効です。未評価の引数は未評価のままです。
• 欠落している引数は、継承されたメソッドで欠落したままです。
• " " 仮引数を介して渡された...引数は、正しい引数名で到着します。
• 呼び出しの実際の引数に対応しないフレーム内のオブジェクトは、継承されたメソッドに渡されません。」

引数に関する限り、継承プロセスは基本的に透過的です。

ややこしいと思ったのは次の2点です。

1. 「現在の方法」と「以前の方法」とは何ですか？
2. 「継承されたメソッドの呼び出しの引数」、「引数の式」、および「現在のメソッドの対応する仮引数の名前」の違いは何ですか?

一般的に言えば、誰かが上記の段落で与えられた説明をより明確な方法で言い換えることができれば、私はそれを感謝します.

私は Agda プロジェクトに数週間取り組んできましたが、レベルのポリモーフィズムを可能な限り無視しています。残念なことに (またはおそらく幸いなことに)、私はそれを理解し始める必要があるところまで来ているようです。

これまで、レベル変数は、 の 2 番目の引数Rel(または の 3 番目の引数REL) として必要な場合にのみ使用してきました。Setそれ以外の場合は、直接使用するだけで省略しました。現在、レベルを明示的に数量化し、いくつかのタイプのフォームを既存のコードにa渡そうとするクライアント コードがいくつかあります。Set a以下の例でquibbleは、 はクライアント コードを表し、_[_]×[_]_と≈-Listは、 を使用するだけの既存のコードの典型ですSet。

≈-Listここで、追加の level パラメータを使用しての帰納的定義を拡張してa、 type の型引数を取ることができますSet aが、入力と出力の関係のユニバースがどのように変化するかについては不明です。そして、問題はより複雑な定義にまで波及します。たとえば、_[_]×[_]_どのように進めたらよいかわからない場合などです。

与えられた例の署名を一般化してquibbleコンパイルするにはどうすればよいですか? 私が従うことができる一般的なルールはありますか? 私はこれを読みました。

違いは何ですか

と

使用法が次のように見える場合

?

どちらか一方を使用する必要があるのはいつですか。また、その理由は何ですか? 2 番目の例は理解できますが、最初の例の目的はよくわかりません。