61

これらの違いは正確には何ですか？私は実存型がどのように機能するかを理解していると思います。それらは、ダウンキャストする方法なしにOOに基本クラスを持っているようなものです。ユニバーサルタイプはどのように異なりますか？

4

2 に答える 2

105

ここでの「ユニバーサル」および「存在」という用語は、述語論理の同様の名前の数量詞に由来します。

全称記号は通常∀と書かれます。これは「すべての人のために」と読むことができ、大まかに言って、「...」の代わりに「∀x。...」に似た論理ステートメントを意味します。数量化されているもののセットから選択できるすべての可能な「x」に当てはまります。

存在記号は通常∃と書かれ、「存在する」と読むことができます。つまり、「∃x。...」に似た論理ステートメントでは、「...」の代わりにあるものはすべて、特定されていないものに当てはまります。 「x」は、定量化されているもののセットから取得されます。

Haskellでは、定量化されるものは型であり（少なくとも特定の言語拡張を無視します）、論理ステートメントも型であり、「真」ではなく「実装可能」と考えます。

したがって、のような全称記号型forall a. a -> aは、可能な任意の型「a」に対して、型が。である関数を実装できることを意味しますa -> a。そして確かに私達はすることができます：

id :: forall a. a -> a
id x = x

a全称記号であるため、私たちはそれについて何も知らず、したがって、いかなる方法でも議論を調べることはできません。したがってid、そのタイプ（1）で可能な唯一の関数です。

Haskellでは、全称記号が「デフォルト」です。シグニチャ内の型変数はすべて、暗黙的に全称記号で表されます。そのため、id通常、の型は単に。として記述されますa -> a。これはパラメトリックポリモーフィズムとも呼ばれ、Haskellでは「ポリモーフィズム」と呼ばれることが多く、他のいくつかの言語（C＃など）では「ジェネリック」と呼ばれます。

のような存在記号型は、特定の型「a」に対して、型が。である関数を実装できることをexists a. a -> a意味します。どの関数でも実行できるので、次のいずれかを選択します。a -> a

func :: exists a. a -> a
func True = False
func False = True

...これはもちろんブール値の「not」関数です。ただし、タイプ「a」についてわかっているのはそれが存在することだけなので、そのままでは使用できないという問題があります。どのタイプであるかに関する情報はすべて破棄されています。つまりfunc、どの値にも適用できません。

これはあまり役に立ちません。

では、何ができるでしょfuncうか？ええと、それはその入力と出力が同じタイプの関数であることを知っているので、たとえばそれ自体で構成することができます。基本的に、実存的なタイプを持つものでできることは、そのタイプの存在しない部分に基づいてできることだけです。同様に、あるタイプの何かが与えられると、exists a. [a]その長さを見つけたり、それ自体に連結したり、いくつかの要素を削除したり、その他のリストに対して実行できることは何でもできます。

その最後のビットは、全称記号に戻り、Haskell （2）が存在型を直接持っていない理由（私existsの上記は完全に架空のものです、悲しいかな）：存在記号を持つものは存在記号を持つ操作でのみ使用できるため全称記号型の場合、型は次のように記述できます。exists a. aつまりforall r. (forall a. a -> r) -> r、すべての結果型に対して、すべての型に対して型の引数を取り、型の値を返すr関数が与えられると、型の結果を取得できます。aarr

これらがほぼ同等である理由が明確でない場合は、タイプ全体が全称記号ではなくa、それ自体が全称記号であるという引数を取り、a選択した特定のタイプで使用できることに注意してください。

余談ですが、Haskellには通常の意味でのサブタイピングの概念はありませんが、数量詞は、ユニバーサルから具象、実存へと階層化されたサブタイピングの形式を表すものとして扱うことができます。あるタイプのものはforall a. a他のタイプに変換できるため、すべてのサブタイプと見なすことができます。一方、任意のタイプをタイプに変換して、exists a. aすべての親タイプにすることができます。もちろん、前者は不可能であり（forall a. aエラー以外に型の値はありません）、後者は役に立たない（型では何もできませんexists a. a）が、少なくとも紙の上では類推は機能します。：]

存在型と全称記号の引数の同等性は、関数入力の分散が反転するのと同じ理由で機能することに注意してください。

したがって、基本的な考え方は、全称記号型はどの型でも同じように機能するものを記述し、存在型は特定の未知の型で機能するものを表すということです。

1：ええと、完全ではありません。たとえば、などのエラーを引き起こす関数を無視する場合に限ります。notId x = undefinedこれには、など、決して終了しない関数も含まれloopForever x = loopForever xます。

2：まあ、GHC。拡張機能がなければ、Haskellには暗黙の全称記号しかなく、実存型について話す実際の方法はまったくありません。

于 2013-01-13T02:10:52.080 に答える
6

Bartosz Milewskiは、彼の本の中で、Haskellが存在記号を必要としない理由についていくつかの良い洞察を提供しています。

疑似Haskellで：

(exists x. p x x) -> c ≅ forall x. p x x -> c

これは、実存型をとる関数がポリモーフィック関数と同等であることを示しています。このような関数は、実存型でエンコードされる可能性のある型のいずれかを処理するように準備する必要があるため、これは完全に理にかなっています。合計型を受け入れる関数は、合計に存在するすべての型に1つずつ、ハンドラーのタプルを使用して、caseステートメントとして実装する必要があることを示すのと同じ原則です。ここで、sum型はcoendに置き換えられ、ハンドラーのファミリーはend、つまりポリモーフィック関数になります。

したがって、Haskellの存在記号型の例は次のとおりです。

data Sum = forall a. Constructor a    (i.e. forall a. (Constructor_a:: a -> Sum) ≅ Constructor:: (exists a. a) -> Sum)

これは合計と考えることができます data Sum = int | char | bool | ...。対照的に、Haskellの全称記号タイプの例は次のとおりです。

data Product = Constructor (forall a. a)

これは製品と考えることができますdata Product = int char bool ...。

于 2019-10-03T22:09:42.023 に答える