問題タブ [gadt]

私はHaskellとHListがどのように実装されているかについての研究論文を読んでいて、説明されている手法がタイプチェッカーにとって決定可能であるかどうか疑問に思っていました。また、GADTでも同様のことができるので、GADTの型チェックは常に決定可能かと思いました。

説明を読んだり理解したりできるように、引用があればいいと思います。

ありがとう！

コード：

Const aに show 型の値を含めて、後で印刷できるようにします。したがって、C＃では次のように記述します。

Haskellでそれを行うにはどうすればよいですか?

一般化された代数データ型を利用するにはどうすればよいですか?

haskell wikibookに示されている例は短すぎて、GADT の実際の可能性についての洞察を得ることができません。

Haskell WikiでGADTについて読み始めましたが、それを理解するのはあまり快適ではありませんでした。Haskell初心者のためにGADTを説明する特定の本の章またはブログ投稿をお勧めしますか？

型の比較のために GADT を定義するとします。

次に、次の型シグネチャで関数eqtを宣言することは可能ですか:

... typeOf x == typeOf y --- の場合、 eqt xyがJust Witnessと評価され、それ以外の場合はNothingと評価されるようなものですか?

関数eqtを使用すると、通常のポリモーフィック データ構造を GADT に持ち上げることができます。

簡単な言語を考えると、

それを型付き表現に変換することは可能ですか:

次のようなさまざまなアプローチを試しました。

これは機能せず、次のエラー メッセージが表示されます。

制約内のあいまいな型変数 'a':
'Typeable a'
は、'e2t' の使用に起因します ...
推定修正: これらの型変数を修正する型シグネチャを追加します

しかし、もし私がこれを好きなら

コンパイルします。

GADTの使用を提案して質問に答えると、パフォーマンスに関するいくつかの質問がコメントに表示されました。質問には型クラスが含まれていましたPlotValue：

そして私の答えはGADTを使用することを提案しましたInput：

しかし、詳細は重要ではないと思います。

パフォーマンスの2つの側面について疑問に思っています。

時間：次のようなパターン一致によって発生する実行時コストはありますか

Maybe2つの値に一致する通常のコストを超えていますか？

スペース：タイプの値はどのくらいのストレージオーバーヘッドInputを運びますか？私の推測ではPlotValue、タイプのすべての値Input（それぞれ「ポインタ」？）に対して2つの辞書があります。つまり、a[Input]を使用するよりも、メモリ使用量の点ではるかに非効率的(Just Double, Just Double)です(# #Double, #Double #)。value通常のタプルまたは解凍されたタプルの結果。

ですから、GADTが私に与える表現力は大好きですが、パフォーマンスの側面についてはあまり考えたことがありません。誰かがこれについてもっと教えてもらえますか（そして私が気付いていないかもしれない他の隠れたコスト）？

(省略) のように定義された GADT があります。

コンパイラは、R の Show を導出できないと正しく不平を言います。この場合、(Either ab) は Show クラスですが、b が Show クラスである場合、これが true であることを知ることはできません。エラーメッセージは、

存在型 ​​b に対して "Show b => Show (D (Either ab))" のようなものを言うか、"(Show a, Show b) = 含意をアップグレードできるようにする必要があるようです。 > Show (Eith ab)」なので、双方向です。

どうもありがとう！

(タイトルや説明は自由に削除してください。)

私はこのようなGADTを持っています：

さまざまな入力プリミティブをラップしますが、最後のコンストラクターではFunctorインスタンスも使用できます。

このタイプのポイント、ところで、サポートすることです：

私ができるようにしたいのは、このタイプの明白なEqインスタンスを次のように定義することです。

問題は3番目のケースです。これは、xとyがその時点で必ずしも同じタイプであるとは限らないため、失敗します。という事は承知しています。私自身のコードでは、長い回避策を講じることができますが、Eqを直接定義する方法があるはずだと感じています。私の考えでは、解決策は「MまたはTに到達するまで、Fコンストラクターをドリルスルーし続け、それらが同じコンストラクター（つまり、両方ともMまたは両方のT）であり、同じタイプである場合は、同等性の比較を行う」のようなものですが、私はどうやってそれを書くことができるかわかりません。

Haskell で GADT の Typeable または Typeable1 インスタンスを定義するための良い例を教えてください。

または、誰かが次の GADT の Typeable を (手動で) 定義する方法を示すことができますか?

あるいは、そのアイデアを紹介した論文へのポインタも役立ちます。