haskell - タイプ数量詞とは何ですか？

Question

多くの静的に型付けされた言語には、パラメトリック多態性があります。たとえば、C＃では次のように定義できます。

T Foo<T>(T x){ return x; }

通話サイトでは、次のことができます。

int y = Foo<int>(3);

これらのタイプは、次のように記述されることもあります。

Foo :: forall T. T -> T

「forallはタイプレベルでのラムダ抽象化のようなものです」と人々が言うのを聞いたことがあります。したがって、Fooは、型（たとえば、int）を取り、値（たとえば、型int-> intの関数）を生成する関数です。Foo(3)多くの言語は型パラメーターを推測するため、の代わりに書くことができますFoo<int>(3)。

fタイプが。のオブジェクトがあるとしますforall T. T -> T。このオブジェクトでできることは、最初に。Qを記述して型を渡すことf<Q>です。次に、タイプが。の値を取得しますQ -> Q。ただし、特定fのは無効です。たとえばこれf：

f<int> = (x => x+1)
f<T> = (x => x)

したがって、「呼び出す」f<int>とタイプが返さint -> intれ、一般に「呼び出す」f<Q>とタイプが返されるQ -> Qので、これは良いことです。ただし、これは、渡すタイプによって異なる動作をするためf、タイプの有効なものではないと一般的に理解されています。forallの考え方は、これは明示的に許可されていないということです。また、forallがタイプレベルのラムダである場合、何が存在しますか？（すなわち、存在記号）。これらの理由から、forallとexistsは実際には「型レベルのラムダ」ではないようです。しかし、それでは彼らは何ですか？この質問はかなり曖昧だと思いますが、誰かが私のためにこれを解決できますか？forall T. T -> T

---

考えられる説明は次のとおりです。

ロジックを見ると、数量詞とラムダは2つの異なるものです。定量化された式の例は次のとおりです。

forall n in Integers: P(n)

したがって、forallには2つの部分があります。1つは定量化するセット（整数など）、もう1つは述語（Pなど）です。Forallは、高階関数と見なすことができます。

forall n in Integers: P(n) == forall(Integers,P)

タイプ付き：

forall :: Set<T> -> (T -> bool) -> bool

存在は同じタイプです。Forallは無限接続詞のようなもので、S[n]は集合Sのn番目の要素です。

forall(S,P) = P(S[0]) ∧ P(S[1]) ∧ P(S[2]) ...

存在は無限の論理和のようなものです。

exists(S,P) = P(S[0]) ∨ P(S[1]) ∨ P(S[2]) ...

型を類推すると、∧の型類似は交差型∩を計算し、∨の型類似は共用体型∪を計算していると言えます。次に、forallを定義し、次のように型に存在します。

forall(S,P) = P(S[0]) ∩ P(S[1]) ∩ P(S[2]) ...
exists(S,P) = P(S[0]) ∪ P(S[1]) ∪ P(S[2]) ...

つまり、forallは無限の共通部分であり、存在するのは無限の和集合です。それらのタイプは次のようになります。

forall, exists :: Set<T> -> (T -> Type) -> Type

たとえば、多形恒等関数のタイプ。これTypesがすべての型のセットであり、->関数の型コンストラクターであり、=>ラムダ抽象化です。

forall(Types, t => (t -> t))

現在、型のものforall T:Type. T -> Tは値であり、型から値への関数ではありません。これは、タイプがすべてのタイプT-> Tの共通部分である値であり、Tはすべてのタイプにまたがっています。このような値を使用する場合、タイプに適用する必要はありません。代わりに、サブタイプの判断を使用します。

id :: forall T:Type. T -> T
id = (x => x)

id2 = id :: int -> int

idこれは、タイプがダウンキャストされますint -> int。int -> int無限の交差点にも表示されるため、これは有効です。

これはうまくいくと思います。これは、forallとは何か、ラムダとの違いを明確に説明していますが、このモデルは、ML、F＃、C＃などの言語で見たものと互換性がありませんid<int>。 intsで恒等関数を取得します。これはこのモデルでは意味がありません。idは値の関数であり、値の関数を返す型の関数ではありません。

---

型理論の知識を持っている人は、正確に何があり、何が存在するのかを説明できますか？そして、「すべてが型レベルでラムダである」というのはどの程度真実ですか？

Answer 1

個別に質問をさせてください。

• forall の「型レベルでのラムダ」の呼び出しは、2 つの理由から不正確です。まず、ラムダ自体ではなく、ラムダの型です。第二に、そのラムダは、型を抽象化しますが、用語レベルに存在します (型レベルのラムダも存在し、一般的な型と呼ばれるものを提供します)。

• 普遍的な数量化は、必ずしもすべてのインスタンス化に対して「同じ動作」を意味するわけではありません。これは、存在する場合と存在しない場合がある「パラメトリック性」と呼ばれる特定のプロパティです。単純な多相ラムダ計算はパラメトリックです。これは、ノンパラメトリックな動作を表現できないためです。しかし、typecase (別名 intensional type analysis) やチェック キャストなどの構造をその弱い形式として追加すると、パラメトリック性が失われます。パラメトリック性は優れた特性を意味します。たとえば、型のランタイム表現なしで言語を実装できます。そして、それは非常に強力な推論原理を誘発します。たとえば、Wadler の論文「Theorems for free!」を参照してください。しかし、それはトレードオフです。タイプのディスパッチが必要になる場合があります。

• 存在型は基本的に、型 (いわゆるwitness) とパッケージと呼ばれることもある用語のペアを表します。これらを表示する一般的な方法の 1 つは、抽象データ型の実装です。簡単な例を次に示します。

  pack ( Int , (λ x . x , λ x . x )) : ∃ T . ( Int → T ) × ( T → Int )

  これは、表現がIntであり、抽象型Tとの間で int を変換するために (ネストされたタプルとして) 2 つの操作のみを提供する単純な ADT です。これは、たとえばモジュールの型理論の基礎です。

• 要約すると、全称量化はクライアント側のデータ抽象化を提供しますが、存在型は二重に実装者側のデータ抽象化を提供します。

• 補足として、いわゆるラムダ キューブでは、forall と arrow は Π 型の統一概念に一般化されます (ここで、T1→T2 = Π(x:T1).T2 および ∀AT = Π(A:*))。 .T) も同様に存在し、タプルは Σ 型 (T1×T2 = Σ(x:T1).T2 および ∃AT = Σ(A:*).T) に一般化できます。ここで、型 * は「型の型」です。

Answer 2

すでに優れた2つの回答を補完するためのいくつかの発言。

forallまず、型レベルでラムダの概念が既に存在するため、 が型レベルでラムダであるとは言えず、それは とは異なりforallます。これは、タイプレベルの計算を備えたシステム F の拡張であるシステム F_omega に表示されます。これは、たとえば ML モジュール システムを説明するのに役立ちます ( F-ing modules、Andreas Rossberg、Claudio Russo、および Derek Dreyer による、2010 年)。

System F_omega (の構文) では、たとえば次のように記述できます。

type prod =
  lambda (a : *). lambda (b : *).
    forall (c : *). (a -> b -> c) -> c

これは、製品タイプの教会エンコーディングのタイプprodなど、「タイプ コンストラクター」の定義です。型レベルで計算がある場合、型チェックを確実に終了させたい場合は、それを制御する必要があります (それ以外の場合は、 type を定義できます。これは、「型レベルの型システム」またはkind system. would of kind . Only the types at kind can be inhabited by values, types at higher-kind are only applied at the type level.値の型にすることはできない型レベルの抽象化であり、あらゆる種類のフォームに存在する一方で、あるタイプでポリモーフィックな値を分類しますprod a b(a, b)(lambda t. t t) (lambda t. t t)prod* -> * -> **lambda (c : k) . ....k -> ...forall (c : k) . ....c : kそして必然的に地面の種類*です。

forall第二に、システム F と Martin-Löf 型理論の Pi 型の間には重要な違いがあります。System F では、ポリモーフィック値はすべての型で同じことを行います。最初の概算として、 type の値forall a . a -> aは (暗黙的に)t入力として型を取り、 type の値を返すと言えますt -> t。しかし、それはプロセスで何らかの計算が行われている可能性があることを示唆していますが、そうではありません。道徳的に、 type の値を type の値にインスタンス化してもforall a. a -> a、値は変化t -> tしません。それについて考えるには、3 つの (関連する) 方法があります。

• System F 数量化には型消去があります。型を忘れても、プログラムの動的セマンティックが何であるかを知ることができます。ML 型推論を使用してポリモーフィズムの抽象化とインスタンス化をプログラムに暗黙的に残す場合、「プログラム」を実行される動的オブジェクトと考えると、推論エンジンに「プログラムの穴を埋める」ことはできません。そして計算します。

• Aは「 for each typeforall a . fooのインスタンスを生成するもの」ではなく、「不明な型のジェネリック」である単一の型です。fooafooa

• 全称量化は無限連言として説明できますが、すべての連言が同じ構造を持ち、特にその証明がすべて同じであるという一様性条件があります。

対照的に、Martin-Löf 型理論の Pi 型は、何かを受け取って何かを返す関数型に似ています。これが、型に依存するだけでなく、用語(依存型)に依存するためにも簡単に使用できる理由の 1 つです。

これらの正式な理論の健全性について懸念している場合、これは非常に重要な意味を持ちます。System F は非予測的 (forall 量化された型は、それ自体を含むすべての型を量化する) であり、それが依然として健全である理由は、この普遍的な量化の均一性にあります。ノンパラメトリック構造を導入することは、プログラマーの観点からは合理的ですが (そして、一般的にノンパラメトリック言語でパラメトリック性について推論することはできます)、基礎となる静的推論システムの論理的一貫性を非常に迅速に破壊します。Martin-Löf の述語理論は、正しいことを証明し、正しい方法で拡張するのがはるかに簡単です。

システム F のこの均一性/汎用性の側面の高レベルの説明については、Fruchart と Longo の 97 記事Carnap's remarks on Impredicative Definitions and the Genericity Theorem を参照してください。非パラメトリック構造の存在下でのシステム F の失敗に関するより技術的な研究については、Robert Harper と John Mitchell によるParametricity and variants of Girard's J operator (1999) を参照してください。最後に、言語設計の観点から、グローバルなパラメトリック性を放棄してノンパラメトリック構造を導入するが、ローカルでパラメトリック性について議論できるようにする方法については、George Neis、Derek Dreyer、および Andreas Rossberg によるNon-Parametric Parametricityを参照してください。 2011年。

「計算による抽象化」と「均一な抽象化」の違いに関するこの議論は、変数バインダーの表現に関する大量の作業によって復活しました。バインディングの構築は抽象化のように感じられます (そして、HOAS スタイルのラムダ抽象化によってモデル化できます) が、結果のファミリーというよりむしろデータ スケルトンのようにする均一な構造を持っています。これは、LF コミュニティ、Twelf の「表象的矢印」、Licata&Harper の作品の「正の矢印」などでよく議論されています。

最近、関連する「無関係」の概念 (結果が引数に「依存しない」ラムダ抽象化) に取り組んでいる人が何人かいますが、これがパラメトリック ポリモーフィズムとどの程度密接に関連しているかはまだ完全には明らかではありません。1 つの例は、Tim Sheard との Nathan Mishra-Linger の作業です (例: Pure Type Systems における Erasure and Polymorphism )。

Answer 3

forall がラムダ ... の場合、何が存在するか

もちろん、タプルです！

Martin-Löf 型理論では、関数/普遍量化に対応する Π 型と、タプル/存在量化に対応する Σ 型があります。

それらの型は、あなたが提案したものと非常に似ています (ここではAgda表記を使用しています)。

Π : (A : Set) -> (A -> Set) -> Set
Σ : (A : Set) -> (A -> Set) -> Set

確かに、Π は無限積であり、Σ は無限和です。ただし、タイプが交差する場所を追加で定義しないとできないため、提案したように、それらは「交差」と「結合」ではないことに注意してください。(一方の型のどの値が他方の型のどの値に対応するか)

これら 2 つの型コンストラクターから、すべての通常関数、ポリモーフィック関数、従属関数、通常タプルと従属タプル、および存在論的および普遍的に量化されたステートメントを作成できます。

-- Normal function, corresponding to "Integer -> Integer" in Haskell
factorial : Π ℕ (λ _ → ℕ)

-- Polymorphic function corresponding to "forall a . a -> a"
id : Π Set (λ A -> Π A (λ _ → A))

-- A universally-quantified logical statement: all natural numbers n are equal to themselves
refl : Π ℕ (λ n → n ≡ n)


-- (Integer, Integer)
twoNats : Σ ℕ (λ _ → ℕ)

-- exists a. Show a => a
someShowable : Σ Set (λ A → Σ A (λ _ → Showable A))

-- There are prime numbers
aPrime : Σ ℕ IsPrime

ただし、これはパラメトリック性にまったく対応しておらず、AFAIK パラメトリック性と Martin-Löf 型理論は独立しています。

パラメトリック性については、通常、Philip Wadler の研究を参照します。