Dlaczego niewyczerpujące osłony powodują niepowodzenie dopasowania wzorca?

Question

mam tej funkcji w Haskell:

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

To co mam, kiedy próbowałem funkcji z różnych wejść:

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

Według Real World Haskell, pierwszy wzór jest niepodważalne. Ale wygląda na to, że test 3 4 nie zawodzi pierwszego wzorca i dopasowuje go do drugiego. Spodziewałem się pewnego rodzaju błędu - być może "niewyczerpujących strażników". Co więc tak naprawdę się tutaj dzieje i czy istnieje sposób, aby włączyć ostrzeżenia kompilatora, na wypadek gdyby tak się stało?

Answer 1

Pierwszy wzór jest rzeczywiście „niepodważalny wzór”, ale to nie znaczy, że zawsze wybierze odpowiednią prawą stronę swojej funkcji. Wciąż podlega strażnikowi, który może zawieść, tak jak w twoim przykładzie.

Aby upewnić się, że wszystkie przypadki są objęte ochroną, często używa się otherwise, aby uzyskać ostateczną osłonę, która zawsze się powiedzie.

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

Zauważ, że nie ma nic magicznego otherwise. Jest zdefiniowany w Preludium jako otherwise = True. Jednak w ostatecznym przypadku jest to idiomatyczne, aby użyć otherwise.

Posiadanie kompilatora ostrzegającego przed nieszczęśliwymi strażnikami byłoby niemożliwe w ogólnym przypadku, ponieważ wymagałoby to rozwiązania problemu zatrzymania, jednak istnieją narzędzia takie jak Catch, które próbują wykonać lepszą pracę niż kompilator przy określaniu, czy wszystkie przypadki są uwzględnione lub nie we wspólnym przypadku.

Answer 2

Osłony nie są niezbite. Ale jest bardzo często (i dobrze) praktyka, aby dodać ostatnią osłonę że złapać inne przypadki, więc funkcja staje:

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

Answer 3

Kompilator powinien ostrzegać, jeśli pominąć drugą klauzulę, tj. Jeśli twój ostatni mecz ma zestaw osłon, w których ostatni nie jest trywialnie prawdziwy.

Ogólnie rzecz biorąc, sprawdzenie osłon pod kątem kompletności jest oczywiście niemożliwe, ponieważ byłoby to równie trudne, jak rozwiązanie problemu zatrzymania.

Odpowiedź na komentarz Matta:

Spójrz na przykład:

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

Człowiek widzi, że jeden z obu strażników musi być prawdą. Ale kompilator nie wie, że albo a <= b lub a > b.

Spójrzmy teraz na inny przykład:

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

Aby udowodnić, że zbiór strażników jest kompletna, kompilator musiał udowodnić Wielkie Twierdzenie Fermata. Nie da się tego zrobić w kompilatorze. Pamiętaj, że liczba i złożoność strażników nie jest ograniczona. Kompilator musiałby być ogólnym rozwiązaniem problemów matematycznych, problemów, które są określone w samym Haskell.

Bardziej formalnie, w najprostszym przypadku:

f x | p x = y 

kompilator musi udowodnić, że jeśli p x nie jest dno, następnie p x jest True dla wszystkich możliwych x. Innymi słowy, musi udowodnić, że albo p x jest na dole (nie zatrzymuje się) bez względu na to, co x jest lub ocenia na True.