問題タブ [gadt]

構成可能なロジックを使用して複雑なデータ構造を作成しようとしています。つまり、データ構造には、一般的な形式 (基本的には、型が変更される可能性のあるいくつかのフィールドを持つレコード) といくつかの一般的な関数があります。特定の構造には、汎用関数の特定の実装があります。

私が試した2つのアプローチがあります。1 つは、型システムを使用することです (型クラス、型ファミリ、関数依存などを使用)。もう 1 つは、独自の「vtable」を作成し、GADT を使用することです。どちらの方法も同様の方法で失敗します - ここで欠けている基本的なものがあるようです。または、おそらく、これを行うためのより良い Haskell 風の方法はありますか?

失敗した「入力された」コードは次のとおりです。

次のエラーが発生します。

そして、失敗した「vtable」コードは次のとおりです。

次のエラーが発生します。

全体が明示的に ScopedTypeVariables と "forall block" の下にあるのに、GHC が "block1" を選択する理由がわかりません。

編集 #1: これを指摘してくれた Chris Kuklewicz のおかげで、機能的な依存関係が追加されました。ただし、問題は残ります。

編集＃2：クリスが指摘したように、VTableソリューションでは、すべての「ブロック〜ブロック状態ポート」を取り除き、代わりに「ブロック状態ポート」をどこにでも書くことで問題が解決します。

編集＃3：OK、問題は、GHCがすべてのタイプを推測するために、すべての個別の関数に対して、パラメーターに十分なタイプ情報を必要とすることです。まったく使用されていないタイプであっても。したがって、上記の (たとえば) logicState の場合、パラメーターは状態のみを提供し、ポートと着信および発信の型が何であるかを知るには十分ではありません。logicState 関数にとって実際には問題にならないことは気にしないでください。GHC は知りたがっていますが、知ることができないため、コンパイルは失敗します。これが本当に核​​心的な理由なら、logicState 宣言をコンパイルするときに GHC が直接文句を言う方がよかったでしょう - そこに問題を検出するのに十分な情報があるようです。その場所で「ポートタイプが使用されていない/決定されていない」という問題を見ていたら、もっと明確だったでしょう。

編集＃4：（ブロック〜ブロック状態ポート）が機能しない理由はまだわかりません。意図しない目的で使用していると思いますか？うまくいくはずだったようです。CPP を使用して回避することは忌まわしいことであるという Chris の意見に同意します。しかし、「B trp e」(より多くのパラメーターを持つ私の実際のコード) を書くことも良い解決策ではありません。

ここで、誰かがFooツリーを作成し、Foo 値の引数が有効かどうかを確認したいとします。コンストラクターの引数に関する規則は次のとおりです。

• Bar2 Bar1 Foo
• Bar3 (Bar2|Bar3|Bar4)
• Bar4 Bar1 Bar1 (Bar1|Bar4)

私は値のコンストラクターを知っており、直接の引数のみをチェックしたいだけで、再帰的なものは何もありません。このような：

たとえば、Bar4 の場合も同様です。

これらの条件を最も簡潔に表現するにはどうすればよいでしょうか? すべての組み合わせをリストすることは、場合によっては少し多すぎます。私の知る限り、パターン マッチングの "OR" 構文は存在しません。

アップデート

私はダニエルのソリューションを採用し、これに到達しました：

これについて私が気に入っているのは、派生句を追加する以外はデータ型を変更する必要がなく、読み取り可能であることです。もちろん、欠点は、これらが動的チェックであることです。私の場合、アサートのようなチェックでプログラミング エラーを検出するだけなので、これで問題ありません。

タイプセーフな二項ヒープを実装しようとしています。このために、型エンコードされたインデックスによって要素型がパラメーター化される 2 つのデータ型があります。

Vec数値パラメーターが減少する値をエンコードします。最後の要素は常に によってパラメーター化されZeroます。RVec他の制限なしで増加する数値パラメーターで値をエンコードします (これが、任意の数値RNilを生成できる理由RVecです)。

これにより、（たとえば）型システムによってチェックされた、高さが増加/減少するツリーのリストを持つことができます。プロジェクトの大部分を実装した後、実装できなかった一見単純な関数が必要であることに気付きました。

指定されたリストの順序を単純に逆にする必要があります。何か案は？前もって感謝します。

GADTとDataKindsを組み合わせるのが本当に好きであることがわかりました。これにより、以前よりも型の安全性が向上します（ほとんどの用途で、Coq、Agdaなどとほぼ同じです）。悲しいことに、パターンマッチングは最も単純な例では失敗し、型クラス以外の関数を作成する方法は考えられませんでした。

これが私の悲しみを説明する例です：

2つの型クラス（1つは定理用、もう1つはユーティリティ操作用）と5つのインスタンスがあります-些細な定理用です。理想的には、Haskellはこの関数を見ることができます：

そして、各句を独自にタイプチェックし、呼び出しごとに、どのケースが可能で（したがって、一致させる価値があります）、どれが不可能であるかを決定します。したがって、trans Le_base Le_baseHaskellを呼び出すと、最初のケースのみが3つの変数を許可することに気付きます。同じで、最初の句でのみ一致を試みます。

私は次のGADTを持っています

クラスを使用して、固定長ベクトルをモデル化する

ベクトルに追加関数をプログラムしようとしました：

タイプチェッカーはそれが好きではありません：

型変数に関する GHC の問題を説明できる人はいますnmか? そして~、エラーメッセージの正確な意味は何ですか?

存在記号型の値を返す必要がある場合があります。これは、ファントムタイプ（たとえば、バランスの取れた木の深さを表す）で作業しているときに最も頻繁に発生します。AFAIKGHCには数量詞はありませんexists。存在記号のデータ型のみを許可します（直接またはGADTを使用）。

例を挙げると、次のような関数が必要です。

これまでのところ、答えとして追加する2つの可能な解決策があります。誰かがより良いまたは異なることを知っているかどうかを知りたいと思います。

Andy Gillは、 Haskellレベルで存在していた共有を DSL で復元する方法を示しています。彼のソリューションはdata-reify パッケージに実装されています。このアプローチを変更して、GADT で動作するようにすることはできますか? たとえば、次の GADT があるとします。

上記のASTを次のように変換して共有を回復したい

関数による

(の種類はわかりませんrecoverSharing。)

let コンストラクトを介して新しいバインディングを導入することは気にしませんが、Haskell レベルに存在していた共有を回復する場合にのみ注意してください。それが私がrecoverSharingリターンを持っている理由Mapです。

再利用可能なパッケージとしてできない場合は、少なくとも特定の GADT に対して行うことはできますか?

このコードには、繰り返されるフラグメントがあります。

したがって、関数を作成するのは魅力的です。

そして、どこでもそれを使用してください、例えば：

書く方法はありますinsert2か？素朴なアプローチはタイプチェックしません。

ForwardPossible と () の 2 つの異なるパラメーターでのみ使用される GADT があります。

OrForward t () と OrForward t ForwardPossible の両方をカバーするのに十分な Data.Data インスタンスを派生させたいと考えています。一般的な (Data t, Data forward) => OrForward t forward インスタンスは可能だとは思わないOrForward t forward インスタンスは、ghc にそれらのインスタンスを派生させる方法がある場合、解決策になる可能性があります。

私は定義しようとしました：

しかし、ghcは次のようなエラーを出します:

HaskellでCombinatoryLogicを実装しようとしていますが、その言語のパーサーに書き込みたいと思います。パーセクを介してパーサーを機能させるのに問題があります。基本的な問題は、パーサーによって返されるオブジェクトが適切に型指定されていることを確認する方法が必要なことです。誰かがこれを行う方法について何か創造的なアイデアを持っていますか？