GADT của kiểm tra

Question

Xét đoạn mã sau:

data (:+:) f g a = Inl (f a) | Inr (g a) 

data A 
data B 

data Foo l where 
    Foo :: Foo A 

data Bar l where 
    Bar :: Bar B 

type Sig = Foo :+: Bar 

fun :: Sig B -> Int 
fun (Inr Bar) = 1 

Mặc dù vui là một trận đấu đầy đủ, khi biên dịch với Wall, GHC phàn nàn về một trường hợp mất tích. Tuy nhiên, nếu tôi thêm một constructor:

data (:+:) f g a = Inl (f a) | Inr (g a) 

data A 
data B 

data Foo l where 
    Foo :: Foo A 
    Baz :: Foo B 

data Bar l where 
    Bar :: Bar B 

type Sig = Foo :+: Bar 

fun :: Sig B -> Int 
fun (Inr Bar) = 1 
fun (Inl Baz) = 2 

Sau đó GHC phát hiện một cách chính xác rằng vui là tổng.

Tôi đang sử dụng mã tương tự như vậy trong tác phẩm của mình và muốn GHC tăng cảnh báo nếu tôi bị lỡ trường hợp và không tăng cảnh báo nếu tôi không làm như vậy. Tại sao GHC phàn nàn về chương trình đầu tiên, và làm thế nào tôi có thể lấy mẫu đầu tiên để biên dịch mà không có cảnh báo mà không cần thêm các nhà xây dựng hoặc trường hợp giả mạo?

Answer 1

Vấn đề thực sự được báo cáo là:

Warning: Pattern match(es) are non-exhaustive 
     In an equation for `fun': Patterns not matched: Inl _ 

Đó là sự thật. Bạn cung cấp trường hợp cho hàm tạo Inr, nhưng không phải là hàm tạo Inl.

Những gì bạn đang hy vọng là vì không có cách nào để cung cấp một giá trị kiểu Sig B có sử dụng các nhà xây dựng Inl (nó sẽ cần một đối số kiểu Foo B, nhưng các nhà xây dựng chỉ cho Foo là loại Foo A), mà Ghc sẽ nhận thấy rằng bạn không cần xử lý hàm tạo Inl.

Vấn đề là do dưới cùng mọi loại đều có người ở. Có là giá trị của loại Sig B sử dụng hàm tạo Inl; thậm chí còn có các giá trị không phải dưới cùng. Họ phải chứa dưới cùng, nhưng họ không phải là chính họ dưới cùng. Vì vậy, nó có thể cho chương trình để được đánh giá một cuộc gọi đến fun mà không phù hợp; đó là điều mà ghc đang cảnh báo.

Vì vậy, để khắc phục điều đó bạn cần thay đổi fun một cái gì đó như thế này:

fun :: Sig B -> Int 
fun (Inr Bar) = 1 
fun (Inl foo) = error "whoops" 

Nhưng bây giờ tất nhiên nếu bạn sau đó thêm Baz :: Foo B chức năng này là một quả bom thời gian chờ để xảy ra. Thật tuyệt khi ghc cảnh báo về rằng, nhưng cách duy nhất để thực hiện điều đó xảy ra là đối sánh mẫu foo với tập hợp các mẫu hiện tại đầy đủ. Rất tiếc, có là không có mẫu hợp lệ nào bạn có thể đặt ở đó! foo được biết là loại Foo B, chỉ có người ở dưới đáy và bạn không thể viết mẫu cho đáy.

Nhưng bạn có thể chuyển nó đến một hàm chấp nhận đối số của loại đa hình Foo a. Hàm đó sau đó có thể khớp với tất cả các nhà xây dựng hiện tại đang tồn tại Foo, do đó bạn sẽ nhận được cảnh báo nếu sau này bạn thêm một.Một cái gì đó như thế này:

fun :: Sig B -> Int 
fun (Inr Bar) = 1 
fun (Inl foo) = errorFoo foo 
    where 
     errorFoo :: Foo a -> b 
     errorFoo Foo = error "whoops" 

Bây giờ Bạn đã xử lý đúng tất cả các nhà thầu của :+: trong fun, những "bất khả thi" trường hợp chỉ đơn giản là lỗi ra nếu nó bao giờ thực sự xảy ra và nếu bạn đã bao giờ thêm Baz :: Foo B bạn nhận được một cảnh báo về một mẫu không đầy đủ trong errorFoo, ít nhất là hướng bạn đến xem fun vì nó được xác định trong một where được đính kèm.

Mặt khác, khi bạn thêm nhà xây dựng không liên quan đến Foo (nói thêm kiểu Foo A), bạn sẽ có thêm nhiều trường hợp để errorFoo, và đó có thể là unfun (mặc dù dễ dàng và cơ khí) nếu bạn đã có rất nhiều các hàm áp dụng mẫu này.

Answer 2

Tôi xin lỗi để cho bạn biết điều này, nhưng ví dụ đầu tiên của bạn không phải là khá đầy đủ như bạn nghĩ rằng đó là:

∀x. x ⊢ fun (Inl (undefined :: Foo B)) 
*** Exception: Test.hs:48:1-17: Non-exhaustive patterns in function fun 

Annoying, vâng, nhưng họ là phá vỡ. ⊥ là lý do tại sao chúng ta không thể có những điều tốt đẹp. : [