問題タブ [gadt]

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

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

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

OCaml (3.12) で型レベルの整数を作成し、それらの加算および減算操作をサポートすることについて、提案/アドバイスをくれる人はいますか?

たとえば、次のように表された数値があるとします。

次のような型で関数を定義する方法が必要です。

少し背景: 物理的な次元の演算用にいくつかの haskell コードを移植しようとしていますが、次元の型 (7 つの基本 SI 単位の指数を表す 7 つの型レベルの int の記録) の演算を定義する機能が必要です。動的バインディング (オブジェクトを使用する場合) を回避し、コンパイラがそのようなすべての式を静的に評価およびチェックできるようにするために、この方法で行う必要があります。

私の現在の理解では、操作を型コンストラクターとして実装する GADT を作成する必要がありますが、それでも私はその考えに苦労しており、ヒントがあれば大歓迎です。

パラメータ化されたデータ型を受け取り、同じ型を返す非常に単純な関数があります。

ノーマライズは、任意のサイズのリストを持つPolyRingを取得し、長さnのパディング/変更された係数ベクトルを持つ新しいPolyRingを返すという考え方です。ここで、nは渡されたPolyRingのタイプの一部です。

エラーが発生しました：

このエラーに関する他のすべてのSO投稿を確認しましたが、まだ何もありません。'len'へのすべての参照を削除しても（ただし、where句に保持して）エラーが発生するため、問題は次のようになります。

これは、他の場所でIntegerAsTypeを使用した方法と実質的に同じです。

あなたがそれをしている間、私はまた、私が現在使用しているパラメータ化された型システムの代替案についての提案をしています。特に、多くの異なる値に対してIntegerAsTypeを定義する必要があるため、これは面倒です。たとえば、異なる多項式環の2つの要素を追加できないようにするために、パラメーターではなく型を使用しています（パラメーター「a」は、同じ多項式を異なる基になる環に多項式環を追加できないようにします）。

ありがとう

これが私の問題です

次のタイプの例外処理に Control.Exception.catch を使用しています: (Hoogle から抜粋)

ハンドラー関数に渡すコンストラクターは次のとおりです

現在のハンドラー関数は次のとおりです。

これを使用して、いくつかのログを記録します。ログに記録する必要がある情報は、タイプ JobState のレコードになります

したがって、上記のタイプを強制されるハンドラーが必要であり、JobState が必要なので、JobException を書き直して JobState を内部に隠すことが答えになると考えました。それはGADTの仕事のようです！わかりません、これは新しい領域です。

私は正しいですか？これをGADTで解決できますか？誰かがそれを構築し始める方法の手がかりを提供できますか? 私が読んでいるチュートリアルは、私が得たものよりも複雑な問題を解決しようとしていると仮定しています。

私が間違っている場合、誰かが私を正しい方向に向けることができますか?

更新: 1から動的型について学び、その後すぐに Data.Dynamic を見つけました。暖かくなる？

ファントム型を楽しむ

最初の試み

この質問を簡潔にするのは難しいですが、最小限の例を提供するために、私がこのタイプを持っていると仮定します。

このタイプを使用すると、次の異種のリストを作成できます。

しかし、残念ながら、インスタンスを書き留めると、問題が発生しEqます。

ああ、だから私たちはCould not deduce (a1 ~ a)。まったく正しい。定義には何も書かれておらず、同じタイプxでなければなりません。y実際、要点は、それらが異なる可能性を許容することでした。

2回目の試行

Data.Typeableミックスに取り入れて、同じタイプの場合にのみ2つを比較してみましょう。

これはかなりいいです。xとyが同じタイプの場合、基になるEqインスタンスを使用します。それらが異なる場合は、を返しますFalse。ただし、このチェックは実行時まで遅延されるため、nonsense = Val2 True == Val2 "Hello"文句なしにタイプチェックできます。

質問

私はここで依存型をいちゃつくことに気づきましたが、Haskell型システムが実行時に返送nonsenseするようなものを許可しながら、上記のようなものを静的に拒否することは可能ですか？sensible = Val2 True == Val2 FalseFalse

この問題に取り組むほど、必要な操作を型レベルの関数として実装するために、 HListの手法のいくつかを採用する必要があるようです。しかし、私は実存主義とGADTを使用するのは比較的新しいので、これらだけで解決策が見つかるかどうか知りたいです。したがって、答えが「いいえ」の場合は、この問題がこれらの機能の限界に達する正確な場所についての議論と、適切な手法、HListなどへの微調整に感謝します。

私は論文「Scrapyourboiloperpolate」Revolutionsのプログラムに従おうとしました。残念ながら、セクションリフトスパインビューのプログラムが私のGHCでコンパイルされないことがわかりました。誰かが私が間違っているところを指摘できますか？

私はomegagbのdevlogでこのスニペットを見ました：

どういうdata ... where意味ですか？dataキーワードは新しいタイプを定義するために使用されると思いました。

Scala の型コンストラクターでの型推論について質問があります。私はScala 2.9.1を実行しています...

ツリーを定義したとします:

そして、私の Tree 定義に基づいて BinaryTree を定義しました:

整数の BinaryTree を次のように定義できるようになりました。

これの問題は、インスタンス化するたびに型パラメーターを指定する必要があることNodeです。

したがって、これを行う場合：

エラーが発生します：

の型を明示的に指定する必要がないように、型チェッカーを強制する方法はありますNodeか?

ありがとう！

私が正しく理解していれば、ステートメント

私の最初の質問では、この Pair 宣言は Tuple2 型コンストラクター (2 つの型パラメーターを必要とする) の単なる構文糖衣であるため、機能しません。これにより、型推論が失敗します。

独自の Pair クラスを宣言すると (ディディアードの回答で示唆されているように)、ツリーを正しく機能させることに成功します。

そしたらこれができる…

ディディアードがこの解決策について言及したことは知っていますが、これは私が望むように動作するようです。あなたの考えを教えてください！

私はJavaでGADTのようなものを持っている必要があります

だから私は簡単にクラスを宣言することができます

次に、たとえばセレクターのインスタンスを受け入れるアクションの実装で使用します。また、述語を受け入れるアクションの実装もありますが、引数の型はコレクションの戻り値の型と一致する必要があります。

主なアイデアは、あるタイプを別のタイプに依存させることです。それは普通の古いJava 6で可能ですか?

フォームのいくつかのステートメントを解析しています

私は State Monad を使用しており、私の状態は (String, Expr a) のペアである必要があります。GADT で PPair を定義する [PPair] として状態を実装しようとしました。

この行がコンパイラを通過すると、本当に間違ったことをしていると感じました。私はその考えを抑えて、コーディングを続けました。State から変数の値を抽出するコードを書き始めたとき、次の問題に気付きました。

私は得る：

これはかなり期待されています。この問題を回避するにはどうすればよいですか? 型をすべての候補型 a に分割することで解決できることはわかっていますが、もっときちんとした方法はありませんか?