30

今日、既存のGADTコンストラクターで照合するときにレイジーパターンを使用しようとすると、コンパイラエラーが発生しました。

実存的またはGADTデータコンストラクターは、遅延（〜）パターン内では使用できません

なぜその制限なのですか？それが許可された場合、どのような「悪い」ことが起こる可能性がありますか？

4

2 に答える 2

28

検討

data EQ a b where
  Refl :: EQ a a

定義できれば

transport :: Eq a b -> a -> b
transport ~Refl a = a

それから私たちは持つことができました

transport undefined :: a -> b

したがって、取得します

transport undefined True = True :: Int -> Int

をヘッド正規化しようとしたときに発生するより適切な失敗ではなく、クラッシュしますundefined。

GADT データは型に関する証拠を表すため、偽の GADT データは型の安全性を脅かします。その証拠を検証するには、それらに厳密である必要があります。底の存在下で未評価の計算を信頼することはできません。

于 2013-01-26T15:39:42.207 に答える
13

「通常の」データでは、パターンマッチング中にコンストラクターのチェックをスキップできます。パターンのデータを使用しようとすると、データが存在しないことが判明し、例外がスローされる可能性があることを理解してください。

GADTを使用すると、存在するコンストラクターに応じて型シグネチャが変更される可能性があります。コンパイル時に型について知る必要があります; 値が必要になるまでコンストラクターをチェックしないのは良くありません。その場合、タイプの不一致エラーが発生する可能性があります。そして、それは潜在的に、あなたのプログラムがセグメンテーション違反（またはさらに悪いこと）でクラッシュすることを意味します。Haskellプログラムは決してセグメンテーション違反であってはなりません。

于 2013-01-26T15:27:19.427 に答える