Tại sao các nhân viên bảo vệ không đầy đủ gây ra sự phù hợp với mô hình không thể chối cãi để thất bại?

Question

tôi có chức năng này trong Haskell:

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

Đây là những gì tôi nhận được khi tôi đã thử các chức năng với các đầu vào khác nhau:

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

Theo Real World Haskell, mô hình đầu tiên là không thể chối cãi. Nhưng có vẻ như test 3 4 không làm hỏng mẫu đầu tiên và khớp với mẫu thứ hai. Tôi mong đợi một số loại lỗi - có thể là 'những người bảo vệ không đầy đủ'. Vì vậy, những gì đang thực sự xảy ra ở đây, và có cách nào để kích hoạt cảnh báo trình biên dịch trong trường hợp điều này vô tình xảy ra?

Answer 1

Các mô hình đầu tiên thực sự là một "mô hình không thể chối cãi", tuy nhiên điều này không có nghĩa là nó sẽ luôn luôn chọn mặt bên phải tương ứng của hàm của bạn. Nó vẫn còn tùy thuộc vào bảo vệ có thể thất bại như trong ví dụ của bạn.

Để đảm bảo tất cả các trường hợp đều được đề cập, việc sử dụng otherwise để bảo vệ cuối cùng sẽ luôn thành công.

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

Lưu ý rằng không có gì kỳ diệu về otherwise. Nó được định nghĩa trong Prelude là otherwise = True. Tuy nhiên, nó là thành ngữ để sử dụng otherwise cho trường hợp cuối cùng. Khi có một trình biên dịch cảnh báo về các bảo vệ không phải là exaustive sẽ là không thể trong trường hợp chung, vì nó sẽ liên quan đến việc giải quyết vấn đề tạm dừng, tuy nhiên có các công cụ như Catch mà cố gắng thực hiện công việc tốt hơn so với trình biên dịch. trường hợp được bảo hiểm hay không trong trường hợp phổ biến.

Answer 2

Các vệ sĩ không thể chối cãi. Nhưng là thực tế rất phổ biến (và tốt) để thêm một bảo vệ cuối cùng mà bắt các trường hợp khác, vì vậy chức năng của bạn trở thành:

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

Answer 3

Trình biên dịch sẽ cảnh báo bạn nếu bạn bỏ qua mệnh đề thứ hai, tức là nếu trận đấu cuối cùng của bạn có một bộ đội bảo vệ, nơi trận đấu cuối cùng không phải là sự thật.

Nói chung, các nhân viên kiểm tra tính đầy đủ rõ ràng là không thể, vì nó sẽ khó giải quyết vấn đề dừng.

trả lời cho nhận xét của Matt:

Nhìn vào ví dụ:

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

Một con người có thể thấy rằng một trong hai vệ sĩ phải đúng. Nhưng trình biên dịch không biết rằng a <= b hoặc a > b.

Bây giờ hãy tìm một ví dụ khác:

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

Để chứng minh rằng tập hợp các vệ sĩ được hoàn tất, trình biên dịch phải chứng minh FLT. Nó không thể làm điều đó trong một trình biên dịch. Hãy nhớ rằng số lượng và độ phức tạp của các vệ sĩ không bị giới hạn. Trình biên dịch sẽ phải là một người giải quyết chung cho các vấn đề toán học, các vấn đề được nêu trong chính Haskell.

Nhiều chính thức, trong trường hợp đơn giản nhất:

f x | p x = y 

trình biên dịch phải chứng minh rằng nếu p x không phải là đáy, sau đó p x là True cho tất cả các thể x. Nói cách khác, nó phải chứng minh rằng p x là dưới cùng (không dừng lại) bất kể số x là hoặc đánh giá là True.