問題タブ [gadt]

[0, ..., n-1]mod-nカウンターを、間隔を2つの部分に分割したものとして表現しようとしています。

これを使用すると、2つの重要な操作を定義するのは簡単です（簡潔にするためにいくつかの証明は省略されています）。

+1問題は、それ-1が逆であることを証明しようとするときに発生します。subst導入されたこれらのエリミネーターが必要な状況に遭遇し続けます。

しかし、これは（ある程度）論点先取であることが判明しました：それはタイプチェッカーによって受け入れられません、なぜならsubst B x=x' y : B x'そしてy : B x...

---- 更新 2 ----

最後に、彼は私にそう言ったExists...</p>

皆さん、ありがとうございました。

- - アップデート - -

わかりました、私たちはそれを呼びますForsome

ex3: forsome x0::[False,True]. forsome x1::[0,1,2]. (x0 || (0 < x1))

（「forallとは何か」を追加したと言った人）：

どうすればいいですか？ありがとう

- - オリジナル - -

式ex3があるとします

ex3: forall x0::[False,True]. forall x1::[0,1,2]. (x0 || (0 < x1)).

False最初は、 ex3は だと思います。なぜならx0 = False、x1 = 0式が (False || (0 < 0))しかし、ex3 はTrue、

"satisfiable ex3 is true because there is at least one combination from sets x0 and x1 which returns true. So as long as there is 1 valid solution in Forall, it is true."

それが正しいと仮定してください…</p>

同じレベルの組み合わせのグループを確認する必要があると思いますが、その方法がわかりません。「同じグループか」を判断するのは難しそうです。

これが私のコードです：

ファイル: Formula.hs

ファイル: Solver.hs

任意の提案をいただければ幸いです。

私は以下を持っています

そして、私は完了するために次のタイプされていないバージョンを検討するように求められます：

コンストラクターのために何を書くべきかわかりません。私は次のことを試しました：

また、vどのタイプでもかまいませんのでint、bool以下（上記）と呼んでv後でタイプを宣言するだけでいいのでしょうか？

どんな助けでも大歓迎です:)

編集：投稿全体を変更して、もう少し情報と明確さを追加しました（演習の私の理解に基づいています）。

基本的に、参照として与えられたGADTのコンストラクターを理解するのに助けが必要data Expr = Condition v...etcです。

私はHaskellの科目について、次のことを与えられた大学からの継続演習を行っています。

そして、それが本当に何をするのかわかりません。で定義されている用語の評価者のようExprです。誰かが私にそれを説明してもらえますか？私の演習では、それを次のように実行したGADTに変換します。

今、彼らは私に以下を静的に実装し、それをタイプセーフにするように求めています：

そこで、より高度な Haskell/GHC の機能と概念のいくつかを理解できるようにするために、動的に型指定されたデータの実用的な GADT ベースの実装を取り上げ、それを拡張してパラメトリック型をカバーすることにしました。(この例が長くなって申し訳ありません。)

ただし、これのコンパイルは最後の行で失敗します (私の行番号は例と一致しません):

私がこれを読んだ方法では、コンパイラは でそれを理解できず、Inductive :: Equal a b -> Equal (f a) (f b)底以外の値と等しくなければなりませんa。bだから私は試しましたがInductive :: Equal a a -> Equal (f a) (f a)、それも失敗し、の定義でmatchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a b):

matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a b)生成するの型を変更してmatchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a a)も機能しません (命題として読んでください)。どちらもしませんmatchTypes :: TypeRep a -> TypeRep a -> Maybe (Equal a a)(別の些細な命題です。私が理解しているように、これにはTypeRep a fromDynamic' to know theDynamic`のユーザーが必要です)。in thecontained in the

だから、私は困惑しています。ここで前進する方法についての指針はありますか？

私は把握しようとしGADTsています、そして私はGHCのマニュアルのGADTの例を見てきました。私が知る限り、同じことをMultiParamTypeClasses：で行うことは可能です。

evalGHCの例とまったく同じコンストラクターと、（インスタンス定義全体に広がる）のまったく同じコードがあることに注意してくださいGADTs。

それで、すべてのファズはGADTs何ですか？できないGADTsことでできることはありMultiParamTypeClassesますか？MultiParamTypeClassesそれとも、代わりに私ができることを行うためのより簡潔な方法を提供するだけですか？

ここでGADT の紹介を読んでいて、プログラマーが正しいタイプの構文ツリーのみを作成するように制限するというアイデアが素晴らしいことに気づき、このアイデアを単純なラムダ計算インタープリターに組み込みましたが、後で文字列を解析してこれは、入力に応じて、1 つの解析関数がさまざまなタイプの構文ツリーを返す必要があるためです。次に例を示します。

GADT を使用する前は、これを使用していました。

ここでは GADT が大きな利点ですLambda (Application ..) ..。

しかし、GADT では、文字列を解析して解析ツリーを作成することができませんでした。以下は、Lambda、Ident、および Application 式のパーサーです。

問題は次のとおりです。

各パーサーが異なる型を返すため、これは明らかに機能しません。

では、GADT を使用して文字列を解析し、構文ツリーを作成する方法はありますか?

GHCi でサポートされていないプラットフォーム (つまり、mipsel 上の GNU/Linux) で GADT を対話的に使用する Haskell プログラムを作成したいと考えています。問題は、GHC で GADT を定義するために使用できる構文です。たとえば、次のようになります。

ハグでは機能していないようです。

1. Hugs で GADT を実際に定義することはできませんか? Haskell クラスの私の TA は、Hugs では可能だと言いましたが、確信が持てないようでした。
2. そうでない場合、GADT を ocaml でエンコードできるように、Hugs でサポートされている他の構文またはセマンティクスを使用して GADT をエンコードできますか?