問題タブ [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 - System F の標準的な実装は何ですか?
System Fは、プロトタイプをプログラミングするときに型について単純に推論する優れた方法です。自分で実装する以外に、既存の実装を使用したいと考えています。
実装を探しているとき、何もないように見えます-そして、私にはその理由がわかりません.
私の質問は次のとおりです。System F の正規の実装とは何ですか?
lambda-calculus - System Fのzip機能
リストタイプを定義しましょう
たとえばどこで
zipタイプの関数を定義しようとしています
それは直感的にそうする
短いリストに合わせて長いリストを切り捨てることに注意してください。
ここで遭遇する主な問題は、一度に 2 つのリストを「反復」できないことです。システム F でそのような機能をどのように実装できますか? それは可能ですか？
agda - System F アグダの教会数字
タイプチェッカーおよびエバリュエーターとして Agda を使用して、システム F でいくつかの定義をテストしたいと思います。
教会の自然数を紹介する私の最初の試みは、次のように書くことでした
これは、通常のタイプ エイリアスと同じように使用されます。
ただし、 の定義はNum型 (種類?) チェックを行いません。それを機能させ、システム F 記法にできるだけ近づけるための最も適切な方法は何ですか?