問題タブ [gadt]

キーと値のペアの関係の種類に特定の制約を加えた、Data.Map 用の特別なスマート コンストラクターを作成したいと考えています。これは私が表現しようとした制約です:

各フィールドには、関連付ける値のタイプが 1 つだけあります。Speed私の場合、フィールドを にマップするのは意味がありませんByteString。Speedフィールドは一意にマップする必要がありますFloat

しかし、次のタイプのエラーが発生します。

使用-XKindSignatures:

Kind の不一致が発生する理由は理解していますが、toPair一致Fieldしない and で使用するコンパイル時の型チェッカー エラーになるように、この制約をどのように表現できますかValue。

#haskell から a を使用するように提案されGADTましたが、まだ理解できていません。

これの目標は、書くことができるようになることです

Mapキー/値の不変条件が尊重される安全な s を作成できるようにします。

したがって、これは型チェックする必要があります

しかし、これはコンパイル時エラーであるはずです

編集：

私の特定の要件は不可能だと思い始めています。私の元の例を使用して

Fooとに制約を課すには、タイプ レベルで とをBar区別する何らかの方法が必要です。したがって、代わりに2つのGADTが必要ですFooIntFooFloatBar

との両方が同じタイプでタグ付けされてPairいる場合にのみ保持されるのインスタンスを作成できるようになりましたFooBar

そして、私は私が望むプロパティを持っています

xs = [FooInt, FooFloat]しかし、それには異種のリストが必要になるため、書く能力を失います。Mapさらに、シノニムを作成しようとすると、タイプのみまたはタイプのみのどちらかでtype FooBar = Map (Foo ?) (Bar ?)立ち往生しています。これは私が望んでいるものではありません。私が気付いていない強力な型クラスの魔法がない限り、それはかなり絶望的に見えます。MapIntFloat

次のGADTがあるとします：

私は今、次のように機能する関数が欲しいです:

そのような関数をどのように構築しますか?

タイプをバインドするさまざまな方法を試しましたが、成功しませんでした。より広範な型バインディングを可能にする、不足している拡張機能はありますか?

これはエラーメッセージです：

達成したいことの説明: DSL と、いくつかの異なる方法で DSL のコードを実行しようとする関数 run を設計したいと考えています (それぞれの方法に複数の異なる run 関数があります)。run 関数は、与えられたコードをできるだけ多く実行しようとし、実行できなかったコードと、実行できたコードの結果を報告します。

次のプログラムは、型チェックとコンパイルを行います。

ただし、 のケースを追加しようとするとeval (Branch m)、checking bombs out と入力します。タイプの何か

が期待されていますが、もちろん私が持っている方法は

書き方について誰か提案がありますeval (Branch m)か？

編集私

@sabauma のコメントに応えて、 の型シグネチャevalを変更する必要があると思いますが、どうすればよいかわかりません。

編集Ⅱ

何が起こるべきかの例を次に示します。

与えるべき、

これが @sabauma さんの提案です。

次のGADTASTがあるとします。

次に、ツリー内Lのタイプのすべての（軒）を置き換える関数を作成します。次のようになります。a

そのような関数を構築することは可能でしょうか？（多分クラスを使用しますか？）GADTに変更が加えられた場合、それは可能でしょうか？

私はすでにtypeof関数を持っています：typeof :: a -> Typeクラス内。

GHCにGADTが導入されたのはいつですか? (バージョン + 日付)

また、それらはまだ言語拡張と見なされていますか、それとも Haskell 標準の適切な一部になっていますか?

Haskellでは、XMLドキュメントの場合のように、再帰ツリーのデータ型を簡単に作成できます。

およびそれに関連するフォールド：

今の私の問題は、HTMLをモデル化するためにツリーデータ型にいくつかの追加の制限を追加する方法がわからないことです。HTMLでは、各要素ノードは正しいコンテキストでのみ表示でき、各要素はその子の異なるコンテキストに対応します。例えば：

• imgのようなボイド要素には空のコンテキストモデルがあり、子を持つことは許可されていません。
• タイトルなどのテキストコンテンツモデルを持つ要素は、子としてテキストノードのみを持つことができます（ネストされたタグは許可されません）
• div要素はPhrasingコンテキストに表示できないため、span要素の子孫になることはできません。

だから私の質問は：

1. Haskell98でこれらの制限をモデル化するにはどうすればよいですか？（Haskell98モデルは他のプログラミング言語にうまく翻訳されるはずなので、これを尋ねます）

   さまざまなコンテキストに対してさまざまなデータ型を作成する必要があるかもしれないと思いますが、これを原則的かつ明確な方法で行う方法がわかりません。迷子になることなくこれを行うにはどうすればよいですか？また、折り畳み関数はどのようになりますか？

2. GADTなどの最新のGHC機能の使用が許可された場合、モデルはどのようになりますか？

   GADTは、制限をタイプチェッカーにプッシュして、折り畳み機能を単純に保つのに役立つかもしれないという予感がありますが、私はそれらの経験があまりありません...

100％機能するソリューションは必要ありません。それは明らかにStackOverflowの説明の範囲を超えているからです。GADTなどをよりよく理解し、残りを自分でできるようになるのに十分なだけです。

次のコードがあるとします。

次に、次のインスタンス宣言が制約なしtで機能します。

そして私が期待することをします。

ただし、次のインスタンス宣言は機能しません。

GHC（私は7.6.1を使用しています）が次のように不平を言っているので：

Typeable tもちろん、コンテキストへの追加は機能します。ただし、次のインスタンスを追加することもできます。

GHCにこの後者のインスタンスを作成させる方法はありますか？もしそうなら、どのように？そうでない場合は、なぜですか？

制約の場合と同じように、GHCがコンストラクターTypeableのコンテキストから制約をプルできることを期待していました。私の問題は、GHCが明示的に書き込みを禁止しているという事実に要約されていると思います。また、標準インスタンスは辞書を見つけるために「内部を調べる」ことができません。WrapEqderiving instance Typeable (Wrapper t)(Typeable1 s, Typeable a) => Typeable (s a)s aTypeable a

コンストラクターに特定の制約のない GADT を、その制約を持つ GADT に変換できますか? 私がこれをしたいのは、矢印の深い埋め込みを取得し、(今のところ) が必要と思われる表現でいくつかの興味深いことをしたいからですTypeable。(理由は一つ)

次の関数を試すこともできますが、再帰ポイントfromの情報がないため、すぐに機能しなくなります。 Typeable

代わりに、型クラスで変換をキャプチャしようとします。しかし、それは破綻するだけでなく、実存的なTypeable b情報を失うことにもなります。b

他の提案はありますか？最終的には、型パラメーターに関する情報CategoryとArrow一緒に深い埋め込みを作成したいと考えています。Typeableこれは、アロー構文を使用して DSL で値を構築し、かなり標準的な Haskell コードを持つことができるようにするためです。多分私は Template Haskell に頼らなければなりませんか?

私が行っている小さな実験のためにいくつかのコードをテストしていますが、最初は修正方法がわからない障害にぶつかりました。

わかりました、これはいくつかのテスト コードです。ドライバー関数はこれよりもはるかに複雑になりますが、このテストでも、「制約内の型変数 'a0' があいまいです: (フィールド a0) は、'fieldName の使用に起因します」というエラーが発生します。 '.したがって、コンパイラは fieldName がフィールドに適用されていることを確認しますが、ここではより具体的な型が必要なようです.関数を多態性のままにしておくと、pgsqlDriver が具体的なクラスではなくなると思いますか?

しかし、これらの関数はポリモーフィックであるという考えになります。これが、ここで GADT を使用することを選択した理由です。そのため、これらのドライバー関数のパラメーターに型の制約を課すことができ、インスタンス化のたびにパラメーターを繰り返す必要がありません。計画では、定義されたデータベース ドライバーが任意の Field および Table インスタンスで機能する可能性があります。これは単純に実行できず、私の DatabaseDriver 型も型クラスにする必要がありますか?

次の（間違った）コードがあるとします。

GHC は次のエラーを表示します。

このエラーメッセージは完全に間違っていませんか? エラーは AApply とは関係ありません。