私はウィキブックスの実存的セクションを読んでいますが、そこには次のように書かれています。
まず、forall は「すべての人に」という意味です。型について考える 1 つの方法は、その型の値のセットです。たとえば、Bool はセット {True, False, ⊥} (一番下の ⊥ はすべての型のメンバーであることを思い出してください!)、Integer は次のセットです。整数 (および下)、String は可能なすべての文字列 (および下) のセットなどです。forall は、これらのセットの交差として機能します。たとえば、forall a. a は、{⊥} でなければならないすべてのタイプの共通部分です。つまり、唯一の値 (つまり、要素) が下にあるタイプ (つまり、セット) です。
forallこれらのセットの交点としてどのように機能しますか?
forall形式論理では、それは言説の宇宙からの任意の値になり得ることを意味します。Haskell ではどのように交差に変換されますか?
Haskell のforall-s は、制限された従属関数型と見なすことができます。これは、概念的に最も啓発的なアプローチであり、集合論的または論理的解釈にも最も適していると思います。
従属言語では、引数の値を関数型にバインドし、それらの値を戻り値の型に含めることができます。
-- Idris
id : (a : Type) -> (a -> a)
id _ x = x
-- Can also leave arguments implicit (to be inferred)
id : a -> a
id x = x
-- Generally, an Idris function type has the form "(x : A) -> F x"
-- where A is a type (or kind/sort, or any level really) and F is
-- a function of type "A -> Type"
-- Haskell
id :: forall (a : *). (a -> a)
id x = x
決定的な違いは、Haskell は を使用して型、持ち上げられたカインド、および型コンストラクターのみをバインドできるforallのに対し、従属言語は何でもバインドできることです。
文献では、従属関数は従属製品と呼ばれます。それらが関数であるのに、なぜそれらをそれと呼ぶのですか？従属関数のみを使用して、Haskell の代数積型を実装できることがわかりました。
一般に、どの関数も、キーに typeがあり、要素にa -> btype がある製品のルックアップ関数と見なすことができます。-sのペアとして解釈できます。この解釈は、すべての製品フィールドが同じタイプでなければならないため、非依存関数にとってはあまり興味深いものではありません。従属関数を使用すると、ペアは適切にポリモーフィックになります。abBool -> IntInt
Pair : Type -> Type -> Type
Pair a b = (index : Bool) -> (if index then a else b)
fst : Pair a b -> a
fst pair = pair True
snd : Pair a b -> b
snd pair = pair False
setFst : c -> Pair a b -> Pair c b
setFst c pair = \index -> if index then c else pair False
setSnd : c -> Pair a b -> Pair a c
setSnd c pair = \index -> if index then pair True else c
ここで、ペアの重要な機能をすべて回復しました。また、 を使用しPairて、任意のアリティの製品を構築できます。
forallでは、 -sの解釈とどのように結びついているのでしょうか。まあ、私たちは通常の製品を解釈して、それらに対するいくつかの直感を構築し、それをforall-s に変換しようとします。
では、まず通常積の代数を少し見てみましょう。代数型は、代数によって値の数を決定できるため、代数型と呼ばれます。詳細な説明へのリンク。値Aの|A|数があり、B値|B|の数Pair A Bがある場合|A| * |B|、可能な値の数があります。合計型では、住民の数を合計します。はフィールドをA -> B持つ積と見なすことができ、すべてタイプが であるため、 の住民の数は-sの数を掛け合わせたものになり、これは次のようになります。|A|BA -> B|A||B||B|^|A|. したがって、関数を表すために時々使用される「指数型」という名前です。関数が従属関係にある場合、指数公式が適合しなくなるため、「いくつかの異なる型の積」の解釈に戻ります。
この理解があればforall (a :: *). t、 type のインデックスと type*を持つフィールドを持つ積の型として解釈できます。Haskell に の特定の型を推測させ、関数を型引数に効果的に適用することで、フィールドを調べることができます。tataforall
この製品には、存在するインデックスの値と同じ数のフィールドがあることに注意してください。これは、Haskell 型の潜在的な数を考慮すると、ここではほとんど無限です。
forallこれらのセットの交点としてどのように機能しますか?
ここで、 Curry-Howard 通信について少し読み始めると役立つ場合があります。簡単に言うと、型を論理命題、言語式をその型の証明、値を正規形証明(これ以上単純化できない証明) と考えることができます。たとえば、は「命題の証明です"Hello world!" :: String」と読みます。"Hello world!"String
forall a. aだから今、命題として考えてください。直観的に、これを命題変数に対する 2 次量化されたステートメントと考えてaくださいa。それは基本的にすべての命題を主張しています。これは、xが の証明である場合forall a. a、任意の命題に対してPもxの証明であることを意味しPます。したがって、 の証明はforall a. a任意の命題を証明する証明であるため、 の証明は、forall a. a各命題をその証明の集合にマッピングし、それらの交点を取った場合に得られるものと同じでなければならないということになります。そして、これらすべての集合に共通する唯一の正規形証明 (すなわち「値」) は下です。
それを見る別の非公式な方法は、全称量化が無限接続詞 ( の∀x.P(x)ようなものP(c0) ∧ P(c1) ∧ ...) のようなものであるということです。モデル理論的な観点から見た結合は集合交点です。が真である評価環境のセットは、が真である環境と真A ∧ Bである環境の共通部分です。AB