Почему неисчерпывающая защита приводит к провалу неопровержимого сопоставления с образцом? - PullRequest
Новая
       26

Почему неисчерпывающая защита приводит к провалу неопровержимого сопоставления с образцом?

11 голосов
/ 18 августа 2011

У меня есть эта функция в 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 не отказывает первый шаблон и соответствует второму.Я ожидал какую-то ошибку - возможно, «неисчерпывающую охрану».Так что же на самом деле происходит, и есть ли способ включить предупреждения компилятора на случай, если это случайно произойдет?

Ответы [ 3 ]

11 голосов
/ 18 августа 2011

Первый шаблон действительно является «неопровержимым шаблоном», однако это не означает, что он всегда будет выбирать соответствующую правую часть вашей функции. Он все еще находится под защитой, которая может потерпеть неудачу, как в вашем примере.

Чтобы обеспечить охват всех дел, обычно используется otherwise, чтобы иметь окончательного охранника, который всегда будет успешным. 

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

Обратите внимание, что в otherwise нет ничего волшебного. Он определен в прелюдии как otherwise = True. Однако идиоматично использовать otherwise в последнем случае.

В общем случае было бы невозможно предупредить компилятор о неисчерпывающих элементах защиты, поскольку это потребовало бы решения проблемы остановки, однако существуют такие инструменты, как Catch , которые пытаются выполнить работу лучше, чем компилятор при определении того, все ли случаи покрыты или нет в общем случае.

6 голосов
/ 18 августа 2011

Компилятор должен предупреждать вас, если вы пропустите второе предложение, т. Е. Если в вашем последнем совпадении есть набор охранников, где последнее не является тривиально истинным.

Как правило, проверка защиты на полноту, очевидноневозможно, так как это будет так же трудно, как решить проблему остановки.

Ответ на комментарий Мэтта:

Посмотрите на пример: 

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

Человек может видетьчто один из обоих охранников должен быть правдой.Но компилятор не знает, что либо 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 не является нижним, тогда p x является True для всех возможных x.Другими словами, он должен доказать, что либо p x является нижним (не останавливается), независимо от того, что x является или оценивается как True.

1 голос
/ 18 августа 2011

Охранники не являются неопровержимыми.Но очень распространенной (и хорошей) практикой является добавление одного последнего охранника, который ловит другие случаи, поэтому ваша функция становится такой: 

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