問題タブ [gadt]

私が DSL を書いていて、ファントム型のサポートと正しく型付けされていない式の両方をサポートしたいとしましょう。私の値のタイプは

ファントム消去バージョンで作業できます

これで、この方法でファントム タイプの両方を削除したり、再構築したりValunkすることで、 の値を操作できます。caseVNumVBool

Typeableしかし、これは機械を再実装しているように感じます。Typeable残念ながら、GHC ではfor を導出できません。Val

この制限を回避する方法はありますか? ぜひ書きたい

しかし今、私はこのような機械に頼らなければなりません

私のすべてのタイプに。

ひどいタイトルでごめんなさい。である型をラップするApplicativeためのインスタンスを作成しようとしています。MonadMonoid

これは機能しません。GCHi は次のように訴えます。

上に書いたことは意味をなさないかもしれないことを理解しています。コンテキストは次のとおりです。論文A pattern for most compositional functions でcompos説明されているように、抽象化を使用しようとしています。このツリーを取得します ( の GADT バージョンを使用して、大幅に簡略化しました):compos

ツリーをたどり、エラーのリストまたは文字列のセットを返す関数をたくさん書きますが、下に行くときに状態 (バインド環境など) も必要とします。たとえば、次のようになります。

composFoldM構造を利用するcomposことで、これらはすべて抽象化できるはずだと思います(Monad m, Monoid o) => m o。そのため、論文の 575/576 ページにある の GADTApplicativeバージョンで使用します。この構造のインスタンスを作成する必要があると思います。どうすればいいですか？それとも、完全に間違った道を進んでいますか?composApplicative

(コメントを使用すると、コピーと貼り付けが簡単になります)

「正しいこと」を行うこの種のクラスを書くことは可能ですか? つまり、正しいインスタンスが選択されるようにプログラムを変更するにはどうすればよいでしょうか。

ランタイム ソリューションを 1 つ知っていると思いますが、それはあまり良くありません。

書き換えルールを見てきましたが、それは良い解決策ですか?

まず、私のコードの最小限の例を次に示します。

異なる種類の URL が混在しないように、GADT を使用しています。このmyExportURL機能は、すべての種類の URL で同じです。このようなものを使用する方法はありますか：

GADT のすべてのサブタイプ (正しい用語は?) ごとに繰り返す代わりに?

コードまたは私が解決しようとしている問題に関するその他のコメントも大歓迎です。

私はこのタイプとこれらの機能を持っています:

コードは型チェックを行いません:

しかし、なぜそうしないのか理解できません。Tag aにはコンテキストがあり(Show a, Eq a, Ord a, Storable a, Binary a)、getVaこのコンテキストを保持する必要があります。私のやり方が間違っているのでしょうか、それとも GADTs 拡張機能の制限ですか?

これは機能します：

編集：例を最小限の例に変更しました

編集: わかりました、なぜこのタイプチェックをしないのですか?

Haskell で組み込み言語の安全な表現を作成するには、多くの拡張機能を使用する必要がありました。関数の相互依存関係を導入したある時点で、型推論は停止し、型変数の正しい置換を見つけ出しました。以下の例を参照してください。

興味深いことに、TypeFamily を使用したときはConnect問題ありませんでした。

2 つのケースの型解決の違いは何ですか?

次のコードがあります

コンパイルまたは解釈すると-Wall、次の警告が表示されます。

通常、これは予想されることです。通常、パターンが考えられるすべてのケースをカバーすると推論できたとしても、コードを実行せずにコンパイラーがそれを知る方法はありません。ただし、提供されたパターンの網羅性は、コンパイル時に実行される型チェッカーによって適用されます。GHC によって提案されたパターンを追加すると、コンパイル時にエラーが発生します。

私の質問はこれです: GHC の警告は GHC の拡張機能とうまく機能しませんか? 彼らはお互いを認識しているはずですか？この機能 (拡張機能を考慮した警告) は将来のリリースで予定されていますか? または、この機能の実装に技術的な制限はありますか?

解決策は単純なようです。コンパイラは、おそらく一致しないパターンを関数に追加し、提案されたパターンが適切に型付けされているかどうかを型チェッカーに再度問い合わせることができます。そうである場合は、実際にパターンの欠落としてユーザーに報告できます。

一次言語の有限モデルを、定数 c、単項関数記号 f、および述語 P で表現したいとします。キャリアを listmとして、定数を の要素としてm、関数を順序付きのリストとして表現できます。の要素のペアm(ヘルパー関数 を介して適用できます)、およびそれを満たすapの要素のリストとしての述語:m

その後、特定のモデルとモデルの操作を構築できます。詳細は私の質問では重要ではなく、型だけです (ただし、型の制約がどこから来たのかを確認できるように、定義を含めました)。

ここで、これらすべてのモデルに名前を付けたいと思います。

最後に、このコードを記述して、各名前をその名前のモデルにマッピングします。

これを機能させるために、型を定義するという意味で、ファントム型、GADT、および型ファミリを使用するなど、model_of のこの定義を正確に使用できるようにするという意味で、いくつかのアプローチを試みましたが、方法は見つかりませんでした。それをするために。(しかし、繰り返しになりますが、私は Haskell の比較的初心者です。) 実行できますか? どうすればいいですか？

GADT ウォークスルーを読んでいて、演習の 1 つに行き詰まってしまいました。指定されたデータ構造は次のとおりです。

演習はsafeTail関数を実装することです。tailPrelude の関数と同様に動作するようにしたいと思います。

^{(私は実際には を定義しませんでしたが==、私が何を意味するかは明らかだと思います)}

これはできますか？タイプがどうなるかは完全にはわかりません...多分safeTail :: MarkedList a Safe -> MarkedList a NotSafe？