問題タブ [system-f]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
types - Hindley Milner 型推論で使用できない System F の型の例
「ヒンドリー・ミルナーとは」の下に、次のように記載されています。
Hindley-Milner はSystem Fの制限であり、より多くの型を許可しますが、プログラマによる注釈が必要です。
私の質問は、Hindley Milner (型推論) では利用できない、System F で利用可能な型の例は何ですか?
(システム F 型の推論が決定不能であることが証明されているという仮定)
haskell - Haskell は、システム F にチューリング完全性をどのように追加しましたか?
私はさまざまな型システムとラムダ計算について調べてきましたが、ラムダ キューブ内の型指定されたラムダ計算はすべて、同等のチューリングではなく、強く正規化されていることがわかりました。これには、単純に型付けされたラムダ計算とポリモーフィズムである System F が含まれます。
これにより、次の質問に至りましたが、これに対する包括的な答えを見つけることができませんでした。
- (例えば) Haskell の形式主義は、それが表向きに基づいている微積分とどのように違うのですか?
- Haskell のどの言語機能が System F 形式に当てはまらない?
- チューリングの完全な計算を可能にするために必要な最小限の変更は何ですか?
これを理解するのを手伝ってくれた人に感謝します。
haskell - Haskell は高ランクのポリモーフィズムを型付けしたくない
このプログラムがタイプ可能でない理由がわかりません:
-XRankNTypes私はGHC でオプションを使用します。
次のエラーがあります。
誰か助けてくれませんか？
agda - Set₀ でのシステム F のパラメトリック多形性のモデル化
システム F では、ポリモーフィック型の種類は*(とにかくシステム F ではそれが唯一の種類であるため...)、たとえば次の閉じた型の場合:
Agda で System F を表現し*たいと考えていSetます。のようなもの
ただし、Agda にはポリモーフィック型がないため、Agda では上記の型は (大きい!) Π 型である必要があります。
これは Set₀ にないことを意味します:
これを回避する方法はありますか、それとも System F はこの意味で Agda に組み込むことはできませんか?
haskell - インスタンス宣言の「不正なポリモーフィックまたは修飾型」(System-F スタイル ツリー)
Haskell で System-F スタイルのデータ構造を実装して実験しています。
型へA <B>の用語の適用を意味するために使用します(型には大文字も使用します)。AB
Tree <T>は type の値を持つ二分木の型だとしましょうT。として機能できるタイプを見つけたいと考えていますTree <T>。次の 3 つのコンストラクターがあります。
したがって、Girard のおかげで、次のように使用できると思います。
そこから
Haskell でこれらのことを行うために必要なディレクティブを見つけました。欠落しているとは思いません。したがって、Haskell では次のようになります。
これまでのところ、これはすべてコンパイルされ、機能しているようです。Show自分のT tタイプのインスタンスを作成しようとすると、問題が発生します。さらにディレクティブを追加しました:
およびツリーを印刷する関数
適切なヘルパーdisplayEmpty :: StringとdisplayFork :: String -> String -> String. これもコンパイルして動作します（かわいらしさまで）。T tのインスタンスとしてインスタンス化しようとするとShow
コンパイルしようとすると、次のエラーが発生します。
andの必要性TypeSynonymInstancesとFlexibleInstances、それらが存在する実用的な理由は理解していますが、なぜ私の型T t がまだのインスタンスとして宣言できないのか理解できませんShow。これを行う方法はありT tますか?また、これが現在私のコードで問題になっていることを意味するのはどのプロパティですか?
haskell - ポリモーフィック セルフ アプリケーション
私がよく理解していない System F 多形性の例があります。
タイプを削除すると、\f.\af (fa) が残り、意味がありません。
これで私を助けてもらえますか？ありがとうございました！
lambda - これらのポリモーフィック型の違いはどれですか?
システム F では、次の 3 つのタイプの違いは何ですか。
ここにテキストで再現：
2番目のものは最初のものよりも一般的ですか?
haskell - 単純型付きラムダ計算をカバーするために、型なしラムダ計算の実装を拡張するには何が必要ですか?
Matt Mightは、Scheme の 7 行でラムダ計算インタープリターを実装することについて語っています。
これは単に型付けされたラムダ計算ではありません。Haskellの中核には、System Fに非常によく似た中間言語があります。一部の人 ( Simon Peyton Jonesを含む)は、これを単純型付きラムダ計算の実装と呼んでいます。
私の質問は、単純型付きラムダ計算をカバーするために型なしラムダ計算の実装を拡張するには何が必要ですか?