7

次のプログラムがあるとします。

{-# LANGUAGE DataKinds, GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Foo = A | B
type family IsA (foo :: Foo) :: Bool

type instance IsA A = True
type instance IsA B = False

data Bar (foo :: Foo) where
    BarA :: (IsA foo ~ True) => Int -> Bar foo
    BarB :: (IsA foo ~ False) => String -> Bar foo

f :: Bar A -> Int
f bar = case bar of
    BarA x -> x

上記で定義され-fwarn-incomplete-patternsた関数全体に使用すると、GHC7.4.2からこの警告が表示されます。f

Warning: Pattern match(es) are non-exhaustive
         In a case alternative: Patterns not matched: BarB _

もちろん、BarB：に一致するものを追加しようとしても意味がありません。

Couldn't match type `'False' with `'True'
Inaccessible code in
  a pattern with constructor
    BarB :: forall (foo :: Foo). IsA foo ~ 'False => String -> Bar foo,
  in a case alternative
In the pattern: BarB _
In a case alternative: BarB _ -> undefined
In the expression:
  case bar of {
    BarA x -> x
    BarB _ -> undefined }

f合計であるGHCを説得する方法はありますか？また、これはGHCのバグですか、それとも既知の制限ですか。fまたは、パターンの一致が完全であることを確認する方法がないという非常に正当な理由が実際にありますか？

4

2 に答える 2

9

はい、それは迷惑です。GHCは、型族（およびクラス）がそのアルゴリズムに深く焼き付けられていることを前提としています。ただし、閉じた種類によってパラメーター化された型族を作成しています。この緊張はあなたとGHCの間の誤解を説明します。クローズドタイプのクラスやファミリーの扱い方については考えられていたと思いますが、難しいところです。

その間、型族の開放性を避けて、全体チェッカーを説得することができます。

{-# LANGUAGE DataKinds, GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Foo = A | B

data Bar (foo :: Foo) where
    BarA :: Int    -> Bar A -- or BarA :: foo ~ A => Int    -> Bar foo
    BarB :: String -> Bar B -- or BarB :: foo ~ B => String -> Bar foo

f :: Bar A -> Int
f bar = case bar of
    BarA x -> x
-- or f (BarA x) = x
于 2012-09-15T18:04:40.347 に答える
1

_ケースの最後の条件として、いつでも何にでもパターンマッチするために使用できます。

したがって_ -> undefined、の代わりにBarB _ -> undefined。

これにより、引数のケースが合計になります。

一致しないパターンによる実行時の失敗を防ぐために、非網羅的なパターンをチェックするNeilMitchellによるライブラリもあります。

于 2012-09-15T16:14:01.490 に答える