11

私はHaskellにこの関数を持っています：

test :: (Eq a) => a -> a -> Maybe a
test a b
  | a == b = Just a
test _ _ = Nothing

これは、さまざまな入力で関数を試したときに得たものです。

ghci>test 3 4
Nothing
ghci>test 3 3
Just 3

Real World Haskellによると、最初のパターンは反駁できません。しかしtest 3 4、最初のパターンは失敗せず、2番目のパターンと一致するようです。私はある種のエラーを予期していました-多分「非網羅的な警備員」。では、ここで実際に何が起こっているのでしょうか。これが誤って発生した場合に備えて、コンパイラの警告を有効にする方法はありますか？

4

3 に答える 3

12

最初のパターンは確かに「反駁できないパターン」ですが、これは、関数の対応する右側を常に選択するという意味ではありません。それでも、あなたの例のように失敗する可能性のあるガードの対象となります。

すべてのケースを確実にカバーするためにotherwise、常に成功するファイナルガードを使用するのが一般的です。

test :: (Eq a) => a -> a -> Maybe a
test a b
  | a == b    = Just a
  | otherwise = Nothing

について魔法は何もないことに注意してくださいotherwise。プレリュードでは、として定義されていotherwise = Trueます。otherwiseただし、最終的なケースに使用するのは慣用的です。

停止性問題の解決を伴うため、一般的なケースではコンパイラーに非強制的なガードについて警告させることは不可能ですが、すべてのケースがカバーされているかどうかを判断する際にコンパイラーよりも優れた仕事をしようとするCatchのようなツールが存在します。一般的なケースではありません。

于 2011-08-18T14:52:36.180 に答える
6

2番目の句を省略した場合、つまり最後の一致に一連のガードがあり、最後の句が自明ではない場合、コンパイラは警告を表示する必要があります。

一般に、停止問題を解くのと同じくらい難しいので、ガードの完全性をテストすることは明らかに不可能です。

マットのコメントへの回答：

例を見てください：

foo a b 
   | a <= b = True
   | a >  b = False

人間は、両方の警備員の1人が真実でなければならないことを理解できます。しかし、コンパイラはそれを認識していませa <= bんa > b。

次に、別の例を探します。

fermat a b c n 
    | a^n + b^n /= c^n = ....
    | n < 0 = undefined
    | n < 3 = ....

ガードのセットが完全であることを証明するために、コンパイラはフェルマーの最終定理を証明する必要がありました。コンパイラでそれを行うことは不可能です。警備員の数と複雑さは制限されていないことを忘れないでください。コンパイラは、数学の問題、Haskell自体に記載されている問題の一般的なソルバーである必要があります。

より正式には、最も簡単なケースでは：

 f x | p x = y

コンパイラは、がp xボトムでない場合、すべての可能なxに対してであることを証明する必要があります。言い換えると、が何であるか、またはに評価されるかに関係なく、どちらかが最下位（停止しない）であることを証明する必要があります。 p xTruep xxTrue

于 2011-08-18T15:10:55.433 に答える
1

警備員は反駁できません。ただし、他のケースをキャッチする最後のガードを1つ追加することは非常に一般的な（そして良い）方法であるため、関数は次のようになります。

test :: (Eq a) => a -> a -> Maybe a
test a b
  | a == b = Just a
  | True = Nothing
于 2011-08-18T14:52:32.047 に答える