問題タブ [gadt]

GADT を使用して、OCaml で単純なラムダ計算のような DSL をどのように定義しますか? 具体的には、型チェッカーを適切に定義して、型指定されていない AST から型付き AST に変換する方法がわかりません。また、コンテキストと環境の正しい型もわかりません。

OCaml の従来のアプローチを使用した単純なラムダ計算のような言語のコードを次に示します。

現在、これを GADT を使用するものに変換しようとしています。これが私のスタートです

これが問題です。まず、texp 型で TLam と TVar の正しい型を定義する方法がわかりません。通常、型には変数名を指定しますが、このコンテキストでそれを行う方法がわかりません。次に、関数の型チェックでコンテキストの正しい型がわかりません。以前はある種のリストを使用していましたが、今ではそのリストのタイプについて確信が持てます。第 3 に、コンテキストを除外した後、typecheck 関数自体は型チェックを行いません。メッセージで失敗します

これは完全に理にかなっています。これは、タイプチェックの正しいタイプがどうあるべきかわからないという問題です。

いずれにせよ、これらの機能をどのように修正しますか?

編集 1

コンテキストまたは環境の可能なタイプは次のとおりです

編集 2

環境の秘訣は、環境のタイプが式のタイプに組み込まれていることを確認することです。そうしないと、型を安全にするための十分な情報がありません。これが完成したインタープリターです。現時点では、型なし式から型付き式に移行するための有効な型チェッカーがありません。

次に、

次のコードがあり、これを型チェックに失敗させたい:

アイデアは、GADT の各エントリに関連するエラーがあり、それをPrismより大きな構造にモデル化するというものです。この GADT を「解釈」するときe、これらすべてのインスタンスを持つ具体的な型を提供しますPrism。ただし、個々のケースごとに、コンストラクターの関連付けられたコンテキストで宣言されていないインスタンスを使用できるようにしたくありません。

上記のコードはエラーになるはずです。なぜなら、でパターン マッチを行うと、Twoしか使用できないことを学習するはずIncrement eですが、 を使用しているからですGreet。これが機能する理由がわかります-Either String IntのインスタンスがあるためGreet、すべてがチェックアウトされます。

これを修正する最善の方法が何であるかはわかりません。からの含意を使用できるData.Constraintか、またはより高いランクの型でトリックが存在する可能性があります。

何か案は？

proc(Netwire と Vinyl を使用して) 構文で GADT をパターン マッチングしようとすると、次のようになります。

ghc-7.6.3 から (かなり奇妙な) コンパイラ エラーが発生します。

パターンにパターンを入れると、同様のエラーが発生しproc (...)ます。どうしてこれなの？それは不健全ですか、それとも実装されていないだけですか?

私はghc 7.8.2でGADTと明示的なforallで遊んでいます。次の簡単な例を見てみましょう。

ここで ghc は次のように失敗します:

T2がコメントアウトされている場合、型チェックは成功します。しかしT1、 とT2は一見同等です。これは ghc のバグですか、それとも GADT の制限ですか? 後者の場合、両者の違いは何ですか？

私は 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で次の線形代数ベクトルを書きました

を実装しようとすると、との定義が異なる (つまり、* と * -> *)Foldableという問題に遭遇します。ZeroSucc

この問題の明白な解決策はありますか?

Stringそれ自体でタグ付けされたを作成する簡単な方法が欲しいです。今、私は次のようなことができます：

そしてそれを次のように使用します

しかし、これは良くないので

• tagタグに関する保証は、GADT によってのみ提供されます。
• 値を作成するたびに、型シグネチャを提供する必要がありますが、値がより大きな式の一部である場合、これは扱いにくくなります。

Stringこれを改善する方法はありますSymbolか? Tag "blah"type を書き、ghc に推論 させたいと思いTagString "blah"ます。

GHC.TypeLits は、someSymbolVal多少関連しているように見える関数を提供しますが、 aSomeSymbolではなくを生成し、Symbol使用方法をかなり理解できます。

「一般化された抽象データ型」と「一般化された代数データ型」という用語は同じ意味で使用されているようですが、技術的には同じではないことは確かです。

おそらくHaskellのコンテキストで簡単な例を使用して、誰かが違いを説明できますか?

GADTを使用して、存在量化された型を表現できます。

GADTはより一般的であることがわかります- data-type-extensions、段落セクション 7.4.7

GADTよりも存在量化された型を使用する方が良いのはいつですか? Existentially quantified typesと比較して、 GADTを使用する際に欠点はありますか?

2 つの De Bruijn インデックス付き変数が同じであることをコンパイラに納得させるのに問題があります。Manuel Chakravarty のConverting a HOAS term GADT into a de Bruijn term GADT に基づいた De Bruijn インデックス コードを使用して、DSL を次のように深く埋め込んでいます。

この関数fuseは、兄弟の融合 (タプリングの最適化) を実装しようとします。Var同じ 2 つの s でパターン マッチする必要があります。インデックス自体を比較することはできますが、これらのインデックスの入力環境が同じであり、同じ型の値にマップされることをコンパイラに納得させる必要もあります。Letこれは、コンストラクターとパターン マッチングを追加することで解決できるのではないかと感じていますが、その方法は不明です。タイプ エラーの要約版を次に示します。

同じである 2 つの変数でパターン マッチを行うにはどうすればよいですか?