21

proc(Netwire と Vinyl を使用して) 構文で GADT をパターン マッチングしようとすると、次のようになります。

sceneRoot = proc inputs -> do
            let (Identity camera :& Identity children) = inputs 
            returnA -< (<*>) (map (rGet draw) children) . pure

ghc-7.6.3 から (かなり奇妙な) コンパイラ エラーが発生します。

  私の脳はちょうど爆発した
    存在または GADT データ コンストラクターのパターン バインドを処理できません。
    代わりに、ケース式または do 表記を使用して、コンストラクターをアンパックします。
    パターン: Identity cam :& Identity childs

パターンにパターンを入れると、同様のエラーが発生しproc (...)ます。どうしてこれなの？それは不健全ですか、それとも実装されていないだけですか?

4

1 に答える 1

12

GADT を検討する

data S a where
  S :: Show a => S a

そしてコードの実行

foo :: S a -> a -> String
foo s x = case s of
            S -> show x

ディクショナリベースの Haskell 実装では、値sがクラス ディクショナリを保持していて、実行できるようにそのディクショナリから関数をcase抽出することが期待されます。showshow x

実行すると

foo undefined (\x::Int -> 4::Int)

例外があります。ディクショナリにアクセスできないため、操作上、これは予想されます。より一般的には、 ( ではない場合)case (undefined :: T) of K -> ...の評価を強制するため、エラーが発生します。undefinedTnewtype

コードを考えてみましょう (これがコンパイルされるとしましょう)

bar :: S a -> a -> String
bar s x = let S = s in show x

との実行

bar undefined (\x::Int -> 4::Int)

これは何をすべきですか？と同じ例外を生成する必要があると主張する人もいるかもしれませんfoo。この場合、参照透過性は次のことを意味します。

let S = undefined :: S (Int->Int) in show (\x::Int -> 4::Int)

同じ例外で失敗します。これは、が式letを評価していることを意味しundefinedます。たとえば、非常に異なります。

let [] = undefined :: [Int] in 5

に評価され5ます。

実際、 a のパターンletは遅延型です: とは異なり、式の評価を強制しませんcase。これが理由です。

let (x,y) = undefined :: (Int,Char) in 5

に正常に評価され5ます。

でaが必要かどうかをlet S = e in e'評価させたいと思うかもしれませんが、それはかなり奇妙に感じます。また、評価するとき、 、、または両方を評価するかどうかが不明確になります。eshowe'let S = e1 ; S = e2 in show ...e1e2

GHC は現在、単純な規則でこれらすべてのケースを禁止することを選択しています: GADT を削除するときに怠惰なパターンはありません。

于 2014-05-08T11:25:55.857 に答える