1

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

data Term a where
    Lit :: Int ->  Term Int
    Pair :: Term a -> Term b -> Term (a,b)
    ...

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

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

2 に答える 2

7

GADT は Hugs には実装されていません。

代わりに、GADT を使用してコードを実行しようとしている場合は、GHC のポートを mips に使用する必要があります。よりエキゾチックなアーキテクチャではバイトコードをロードできないため、すべてのプラットフォームで ghci を使用できるわけではないことに注意してください。

于 2012-06-22T14:50:19.390 に答える
4

質問 2 (Haskell 98 で GADT ユース ケースをエンコードする方法) については、Sulzmann と Wang によるこの 2006 年の論文: Haskell 98 での GADTless プログラミング を参照してください。

あなたが参照している OCaml の作業のように、これは等価型を介して GADT を因数分解することによって機能します。等値型を定義するにはさまざまな方法があります。それらは OCaml のようなライプニッツ等価の形式を使用します。これにより、 kind での型演算子の任意の適用による置換が可能になります* -> *。

特定の型チェッカーが GADT の等価性についてどのように推論するかによって、これは GADT のすべての例をカバーするのに十分な表現力を持たない可能性があります。たとえば、 and をa*b = c*d意味a = cしb = dます。この形式の分解は、型コンストラクターを kind でのみ適用する場合には発生しません* -> *。2010年後半、オレグは、型ファミリーを使用して、ライプニッツの等式を介して「型デコンストラクター」を適用し、この定義の分解プロパティを取得する方法について説明しましたが、もちろん、これは Haskell 98 の範囲外です。

これは、型システムの設計者が心に留めておくべきことです: あなたの言語は、特殊な等式ソルバーができることを表現できるという意味で、ライプニッツの等式に対して完全ですか?

十分に表現力のある等値型のエンコーディングを見つけたとしても、非常に実用的な利便性の問題が発生します。GADT を使用すると、等値監視のすべての使用が型注釈から推測されます。この明示的なエンコーディングを使用すると、さらに多くの作業を行う必要があります。

最後に (しゃれは意図していません)、GADT の多くのユースケースはタグレス最終埋め込み(Oleg による) によって同等に表現でき、IIRC は Haskell 98 で実行できることがよくあります。dons が指す Martin Van Steenbergen によるブログ投稿その返信のコメントはこの精神にありますが、オレグはこの手法を大幅に改善しました。

于 2012-06-24T10:25:05.823 に答える