8

たとえば、Num a => a。

それらは単に「制約付きタイプ」と呼ばれていると思いましたが、グーグルはその用語の多くの使用法を見つけなかったので、それらが他の名前で呼ばれるかどうか知りたいです。

4

5 に答える 5

7

この特定の種類の制約を持つ型は「修飾型」と呼ばれ、機能自体が「修飾されたポリモーフィズム」になることもあります。この用語は、もともとMarkJonesのESOP'92論文によって導入されたと思います。

修飾型は、Javaなどの言語のジェネリックスが基づいている「有界ポリモーフィズム」のより主流の概念と混同しないでください。有界ポリモーフィズムは本質的に、パラメトリックポリモーフィズムとサブタイピングの（かなり複雑な）組み合わせですが、修飾されたタイプはサブタイピングなしでうまくいきます。

于 2012-07-14T12:51:51.253 に答える
6

「修飾されたタイプ」。マークP.ジョーンズを参照してください。適格なタイプ：理論と実践。ケンブリッジ大学出版局、ケンブリッジ、1994年。

Googleで関連するマッチがたくさんあります。

于 2012-07-14T11:29:22.940 に答える
6

私は型理論の専門家ではありませんが、少し調べてみると、これが私が見つけたものです（これは役立つかもしれないし、役に立たないかもしれませんが、コメントに収めることはできません）。

Haskellの穏やかな紹介：クラスはそのNum a部分をタイプのコンテキストと呼びます：

タイプaがクラスEqのインスタンスでなければならないという制約は、Eqaと書かれています。したがって、式aは型式ではなく、型に対する制約を表し、コンテキストと呼ばれます。

ですから、「文脈のある型」とか、「制約型」と言ってもいいと思います。

もう1つの注目すべき場所は、Haskellの型クラスが最初に記述されている場所です（私は信じています）：アドホック多相性をアドホックでなくする方法[postscript]。

型クラスは、オブジェクト指向プログラミング、型の有界量化、および抽象データ型で発生する問題と密接に関連しているようです[CW85、MP85、Rey85]。いくつかの接続の概要を以下に示しますが、これらの関係を完全に理解するには、さらに作業が必要です。

この論文は1988年に書かれたので、これらの関係が完全に理解されているかどうかはわかりませんが、有界量化のウィキペディアのページにはHaskellが記載されていないため、まったく同じかどうかはわかりません。（もう一度、タイプ理論家ではなく、Haskellが好きな人だけです）

また、square :: Num a => a -> aそれが言うタイプについて：

これは、「クラスに属するすべてのものに対して、タイプsquareがあります（つまり、、、およびnegateがで定義されているようなもの）」と読み取られます。a -> aaaNum(+)(*)a

タイプは「クラスに属する」と言えます。

それが私が持っているすべてについてです。個人的には、「制約されたタイプ」または「クラスに制約されたタイプ」は問題なく機能すると思います。

于 2012-07-13T17:50:13.770 に答える
6

このNum a =>部分は実際には制約と呼ばれます。あなたはそれを「もしNum a真実なら...」と読むことができます。

通常、制約と数量詞は一緒に議論されます。制約付きタイプは、制約が数量詞forallまたはexists数量詞のすぐ内側にのみ表示される同等のタイプに変換できます。forall a. C => Tしたがって、「制約付きパラメトリック多態性」（ ）、「制約付き存在型」（exists a. C => T）、または「制約付き多態性」（両方の種類の数量詞）について聞くほど、「制約付き型」については耳にしません。

関連する用語は「有界ポリモーフィズム」です。有界ポリモーフィズムとは、通常、制約がサブタイプまたはスーパータイプの制約である制約付きポリモーフィズムを意味します。ただし、この区別は厳密には守られていません。JavaやScalaのようなサブタイピングのある言語では、「バウンド」と呼ばれるあらゆる種類の制約がよく聞こえます。

于 2012-07-13T20:26:53.683 に答える
1

これを有界ポリモーフィック型と呼ぶことができます（ウィキペディアを参照）。

于 2012-07-13T17:22:01.050 に答える