GADT的详尽检查失败了

Question

请考虑以下代码:

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

尽管有趣是一场详尽的比赛,但在使用-Wall进行编译时,GHC会抱怨丢失案例.但是,如果我添加另一个构造函数:

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

然后GHC正确地检测到乐趣是完全的.

我在我的工作中使用类似于此的代码,如果我错过了案例,我希望GHC提出警告,如果不这样做,就不会发出警告.为什么GHC会对第一个程序抱怨,如何在没有添加虚假构造函数或案例的情况下在没有警告的情况下编译第一个样本？

Answer 1

实际报告的问题是:

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

这是真的.您为Inr构造函数提供了一个案例,但不提供Inl构造函数.

什么你希望的是,因为没有办法提供类型的值Sig B,它使用Inl的构造函数(它需要类型的参数Foo B,但唯一的构造函数Foo的类型的Foo A),即GHC会发现,你不需要处理Inl构造函数.

麻烦的是,由于底部每种类型都有人居住.这里是类型的值Sig B使用的Inl构造函数; 甚至有非底价值.它们必须包含底部,但它们本身不是底部.因此,程序可能正在评估一个fun无法匹配的调用; 这就是ghc警告的内容.

所以要解决这个问题,你需要改成fun这样的东西:

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

但是现在当然如果你以后添加Baz :: Foo B这个功能是一个定时炸弹等待发生.ghc对此提出警告是很好的,但实现这一目标的唯一方法是将模式匹配foo与当前详尽的模式集进行模式匹配.不幸的是,你可以把有没有有效的模式!foo已知是类型Foo B,只有底部居住,你不能写底部的图案.

但是你可以将它传递给一个接受多态类型参数的函数Foo a.然后,该函数可以匹配所有当前存在的Foo构造函数,以便稍后添加一个构建函数时会收到警告.像这样的东西:

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

现在你已经正确处理了:+:in的所有构造函数fun,"不可能"的情况只是错误,如果它实际发生,如果你曾经添加Baz :: Foo B你得到一个关于非详尽模式的警告errorFoo,这至少指导你看在fun因为它在定义的连接where.

在缺点方面,当你添加不相关的构造函数Foo(比如更多类型Foo A)时,你将不得不添加更多的情况errorFoo,如果你有很多函数应用这种模式,那么这可能是不合适的(虽然简单和机械).

Answer 2

很抱歉告诉你这个,但你的第一个例子并不像你想象的那样详尽:

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

很烦人,是的,但他们是休息.⊥这就是为什么我们不能拥有美好的东西.:[