問題タブ [gadt]
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.
ocaml - OCaml で GADT を使用した単純なラムダ計算 DSL
GADT を使用して、OCaml で単純なラムダ計算のような DSL をどのように定義しますか? 具体的には、型チェッカーを適切に定義して、型指定されていない AST から型付き AST に変換する方法がわかりません。また、コンテキストと環境の正しい型もわかりません。
OCaml の従来のアプローチを使用した単純なラムダ計算のような言語のコードを次に示します。
現在、これを GADT を使用するものに変換しようとしています。これが私のスタートです
これが問題です。まず、texp 型で TLam と TVar の正しい型を定義する方法がわかりません。通常、型には変数名を指定しますが、このコンテキストでそれを行う方法がわかりません。次に、関数の型チェックでコンテキストの正しい型がわかりません。以前はある種のリストを使用していましたが、今ではそのリストのタイプについて確信が持てます。第 3 に、コンテキストを除外した後、typecheck 関数自体は型チェックを行いません。メッセージで失敗します
これは完全に理にかなっています。これは、タイプチェックの正しいタイプがどうあるべきかわからないという問題です。
いずれにせよ、これらの機能をどのように修正しますか?
編集 1
コンテキストまたは環境の可能なタイプは次のとおりです
編集 2
環境の秘訣は、環境のタイプが式のタイプに組み込まれていることを確認することです。そうしないと、型を安全にするための十分な情報がありません。これが完成したインタープリターです。現時点では、型なし式から型付き式に移行するための有効な型チェッカーがありません。
次に、
haskell - 制限された制約を GADT で使用するにはどうすればよいですか?
次のコードがあり、これを型チェックに失敗させたい:
アイデアは、GADT の各エントリに関連するエラーがあり、それをPrismより大きな構造にモデル化するというものです。この GADT を「解釈」するときe、これらすべてのインスタンスを持つ具体的な型を提供しますPrism。ただし、個々のケースごとに、コンストラクターの関連付けられたコンテキストで宣言されていないインスタンスを使用できるようにしたくありません。
上記のコードはエラーになるはずです。なぜなら、でパターン マッチを行うと、Twoしか使用できないことを学習するはずIncrement eですが、 を使用しているからですGreet。これが機能する理由がわかります-Either String IntのインスタンスがあるためGreet、すべてがチェックアウトされます。
これを修正する最善の方法が何であるかはわかりません。からの含意を使用できるData.Constraintか、またはより高いランクの型でトリックが存在する可能性があります。
何か案は？
haskell - 奇妙な ghc エラー メッセージ、「私の脳はちょうど爆発しました」?
proc(Netwire と Vinyl を使用して) 構文で GADT をパターン マッチングしようとすると、次のようになります。
ghc-7.6.3 から (かなり奇妙な) コンパイラ エラーが発生します。
パターンにパターンを入れると、同様のエラーが発生しproc (...)ます。どうしてこれなの？それは不健全ですか、それとも実装されていないだけですか?
haskell - ghc 7.8.2 での GADT と明示的な forall
私はghc 7.8.2でGADTと明示的なforallで遊んでいます。次の簡単な例を見てみましょう。
ここで ghc は次のように失敗します:
T2がコメントアウトされている場合、型チェックは成功します。しかしT1、 とT2は一見同等です。これは ghc のバグですか、それとも GADT の制限ですか? 後者の場合、両者の違いは何ですか？
haskell - 暗黙の引数と型ファミリー
私は Data.Singletons ライブラリを使用して、依存型付けされたプログラムを実験してきました。これは、論文「シングルトンを使用した依存型付けプログラミング」で長さの注釈が付けられたベクトルの開発に続き、次の問題に遭遇しました。
次のコードは、 function の定義を除いて、indexIGHC 7.6.3 で型チェックを行い、それがなくても期待どおりに動作します。
を含めた後indexI、GHC は 2 つのエラーを生成します。
と、
いずれの誤りの根源も、項withSing indexが 型FlipList a b n -> BiPreMap a b a0を持ち、 を推論できなければa0 ~ m、GHC が を証明できないことにあるようBiPreMap a b m ~ BiPreMap a b a0です。型ファミリの型推論には、ADTS を使用するときに得られる便利さ (単射性、生成性など) のほとんどが欠けていることはわかっていますが、この場合の問題が正確に何であるか、およびそれを回避する方法についての私の理解は非常に限られています。 . それを解決する可能性のある指定できる制約はありますか?
haskell - GADT を使用した型クラスの実装
Haskellで次の線形代数ベクトルを書きました
を実装しようとすると、との定義が異なる (つまり、* と * -> *)Foldableという問題に遭遇します。ZeroSucc
この問題の明白な解決策はありますか?