摆脱的限制型家庭GADTs当“非详尽的彭定康匹配”警告

考虑下面的程序：摆脱的限制型家庭GADTs当“非详尽的彭定康匹配”警告

{-# LANGUAGE DataKinds, GADTs #-} 
{-# LANGUAGE TypeFamilies #-} 

data Foo = A | B 
type family IsA (foo :: Foo) :: Bool 

type instance IsA A = True 
type instance IsA B = False 

data Bar (foo :: Foo) where 
    BarA :: (IsA foo ~ True) => Int -> Bar foo 
    BarB :: (IsA foo ~ False) => String -> Bar foo 

f :: Bar A -> Int 
f bar = case bar of 
    BarA x -> x

使用-fwarn-incomplete-patterns为定义的总功能f当我从GHC 7.4.2此警告以上：

Warning: Pattern match(es) are non-exhaustive 
     In a case alternative: Patterns not matched: BarB _

当然，这没有任何意义，甚至尝试添加匹配BarB：

Couldn't match type `'False' with `'True' 
Inaccessible code in 
    a pattern with constructor 
    BarB :: forall (foo :: Foo). IsA foo ~ 'False => String -> Bar foo, 
    in a case alternative 
In the pattern: BarB _ 
In a case alternative: BarB _ -> undefined 
In the expression: 
    case bar of { 
    BarA x -> x 
    BarB _ -> undefined }

有没有办法让GHC相信f是完全的？另外，这是GHC的一个bug，还是只是一个已知的限制;或者实际上有一个非常好的理由，为什么没有办法看到f中的模式匹配是完整的？

来源

2012-09-15 Cactus

这很烦人，是的。 GHC有一个假设，即类型家族（和类）在各地的算法中都是开放式的;然而，你正在编写一个由封闭类型参数化的类型族。这种紧张关系解释了你和GHC之间的误解。我认为对如何处理封闭式班级和家庭有一些想法，但这是一个棘手的领域。

与此同时，您可以避免类型家庭的开放性，以说服总体检查。

{-# LANGUAGE DataKinds, GADTs #-} 
{-# LANGUAGE TypeFamilies #-} 

data Foo = A | B 

data Bar (foo :: Foo) where 
    BarA :: Int -> Bar A -- or BarA :: foo ~ A => Int -> Bar foo 
    BarB :: String -> Bar B -- or BarB :: foo ~ B => String -> Bar foo 

f :: Bar A -> Int 
f bar = case bar of 
    BarA x -> x 
-- or f (BarA x) = x

来源

2012-09-15 18:04:40

不幸的是，我不能这么说，因为我的真实用例通过让'data Foo = A | B | C'和两个构造函数'BarA'和'BarBC'。 – Cactus

@Cactus'data BorC a where {IsB :: BorC B; IsC :: BorC C};数据Bar foo where BarBC :: BorC foo - > String - > Bar foo' –

您总是可以使用_模式匹配任何情况作为案例的最后一个条件。

因此_ -> undefined而不是BarB _ -> undefined。

这将在其论点中总结案例。

Neil Mitchell还有一个library，它检查非穷举模式以防止由于不匹配模式导致运行时失败。

来源

2012-09-15 16:14:01 Satvik

摆脱的限制型家庭GADTs当“非详尽的彭定康匹配”警告

回答

相关问题