为什么在枚举所有情况时通配符匹配不起作用？

Question

考虑这个代码：

{-# LANGUAGE GADTs #-}

data P t where
 PA :: P Int
 PB :: P Double
 PC :: P Char

isA PA = True
isA _ = False

它编译并运行良好。现在考虑这个代码：

{-# LANGUAGE GADTs #-}

data P t where
 PA :: P Int
 PB :: P Double
 PC :: P Char

isA PA = True
isA PB = False
isA PC = False

它无法编译：

Main.hs:8:10: error:
    • Couldn't match expected type ‘p’ with actual type ‘Bool’
        ‘p’ is untouchable
          inside the constraints: t ~ Int
          bound by a pattern with constructor: PA :: P Int,
                   in an equation for ‘isA’
          at Main.hs:8:5-6
      ‘p’ is a rigid type variable bound by
        the inferred type of isA :: P t -> p
        at Main.hs:(8,1)-(10,14)
      Possible fix: add a type signature for ‘isA’
    • In the expression: True
      In an equation for ‘isA’: isA PA = True
    • Relevant bindings include isA :: P t -> p (bound at Main.hs:8:1)
  |
8 | isA PA = True
  |          ^^^^

Main.hs:9:10: error:
    • Couldn't match expected type ‘p’ with actual type ‘Bool’
        ‘p’ is untouchable
          inside the constraints: t ~ Double
          bound by a pattern with constructor: PB :: P Double,
                   in an equation for ‘isA’
          at Main.hs:9:5-6
      ‘p’ is a rigid type variable bound by
        the inferred type of isA :: P t -> p
        at Main.hs:(8,1)-(10,14)
      Possible fix: add a type signature for ‘isA’
    • In the expression: False
      In an equation for ‘isA’: isA PB = False
    • Relevant bindings include isA :: P t -> p (bound at Main.hs:8:1)
  |
9 | isA PB = False
  |          ^^^^^

Main.hs:10:10: error:
    • Couldn't match expected type ‘p’ with actual type ‘Bool’
        ‘p’ is untouchable
          inside the constraints: t ~ Char
          bound by a pattern with constructor: PC :: P Char,
                   in an equation for ‘isA’
          at Main.hs:10:5-6
      ‘p’ is a rigid type variable bound by
        the inferred type of isA :: P t -> p
        at Main.hs:(8,1)-(10,14)
      Possible fix: add a type signature for ‘isA’
    • In the expression: False
      In an equation for ‘isA’: isA PC = False
    • Relevant bindings include isA :: P t -> p (bound at Main.hs:8:1)
   |
10 | isA PC = False
   |          ^^^^^

为什么？这里发生了什么？

编辑：添加类型签名isA :: P t -> Bool使其工作，所以我现在的问题变成：为什么类型推断在第二种情况下不起作用，因为它在第一种情况下起作用？

Answer 1

在没有 GADT 的情况下键入 case 构造（无论是显式case语句还是隐式基于模式的函数定义）时，各个替代方案：

pattern -> body

可以通过以下方式统一：键入所有模式并将其与被检查者的类型统一，然后键入所有主体并将其与表达式的类型统一case为一个整体。所以，在一个简单的例子中，例如：

data U = UA | UB | UC
isA1 u = case u of
  UA -> True
  UB -> False
  x  -> False

我们可以首先输入模式UA :: U, UB :: U, x :: a，使用类型相等来统一它们a ~ U以推断受审查者的类型u :: U，并且类似地将True :: Bool和 两者统一False :: Bool为整个 case 表达式的类型，将其与getBool的类型统一。isAisA :: U -> Bool

请注意，统一过程可以对类型进行专门化。在这里，图案的类型x :: a是通用的，但到统一过程结束时，它已经专门化为…… x :: U。这也可能发生在身体上。例如：

len mstr = case mstr of
  Nothing -> 0
  Just str -> length str

在这里，0 :: Num a => a是多态的，但因为length返回一个Int，所以在进程结束时，主体（以及整个 case 表达式）已统一为类型Int。

一般来说，通过统一，所有主体的共同的、统一的类型（以及整体案例表达的类型）将是“最一般的”/“最少限制的”类型，其中主体的类型都是概括的。在某些情况下，该类型可能是其中一个主体的类型，但一般来说，所有主体都可以比“最通用”统一类型更通用，但没有一个主体可以更具限制性。

GADT 的存在使事情发生了变化。当使用 GADT 对案例构造进行类型检查时，替代方案中的模式可以引入“类型细化”，即一组用于对替代方案主体进行类型检查的类型变量的附加绑定。（这就是 GADT 发挥作用的首要原因。）

因为不同的替代方案的主体是在不同的改进下进行类型化的，所以简单的统一是不可能的。例如，考虑微型类型 DSL 及其解释器：

data Term a where
  Lit :: Int -> Term Int
  IsZ :: Term Int -> Term Bool
  If :: Term Bool -> Term a -> Term a -> Term a

eval :: Term a -> a
eval t = case t of
  Lit n -> n
  IsZ t -> eval t == 0
  If b t e -> if eval b then eval t else eval e

如果我们天真地统一主体n :: Int、eval t == 0 :: Bool和if eval b then eval t else eval e :: a，程序将不会键入检查（最明显的是，因为Int和Bool不统一！）。

一般来说，由于类型细化允许替代方案主体的计算类型比最终类型更具体，因此不存在明显的“最通用”/“限制最少”类型来统一所有主体，就像没有 GADT 的 case 表达式。

相反，我们通常需要为整个 case 表达式提供一个“目标”类型（例如， for ，类型签名中的eval返回类型），然后在构造函数引入的每个细化下确定 if （例如，引入细化） ，身体具有与其类型相关的细化。aIsZa ~ Booleval t == 0 :: Boola

如果没有明确提供目标类型，那么一般来说，我们能做的最好的事情就是使用新的类型变量p作为目标，并尝试根据该类型检查每个精炼类型。

这意味着，给定以下没有类型签名的定义isA2：

data P t where
  PA :: P Int
  PB :: P Double
  PC :: P Char

isA2 = \p -> case p of
  PA -> True
  PB -> False
  PC -> False

GHC 试图做的是 type isA2 :: P t -> p。对于替代方案：

PA -> True

它键入PA :: P t给出细化t ~ Int，并在此细化下，它尝试键入True :: p。不幸的是，p没有Bool进行任何涉及不相关类型变量的细化a，并且我们得到一个错误。其他替代方案也会产生类似的错误。

事实上，我们还可以做一件事。如果存在不引入类型细化的替代方案，那么其主体的计算类型并不比最终类型更具体。因此，如果我们统一“未精炼”替代方案的主体类型，则生成的类型将为精炼替代方案提供合法的统一目标。

这意味着，例如：

isA3 = \p -> case p of
  PA -> True
  x  -> False

第二种选择：

x -> False

x :: P t通过匹配不引入类型细化的模式来键入。主体的未精炼类型是Bool，并且该类型是统一其他替代方案的适当目标。

具体来说，第一种选择：

PA -> True

与类型细化相匹配a ~ Int。在此细化下，主体的实际类型True :: Bool与目标类型的“细化”相匹配Bool（“细化”为Bool），并且确定替代方案具有有效类型。

因此，直觉是，如果没有通配符替代方案，则 case 表达式的推断类型是任意类型变量p，这太笼统而无法与类型精炼替代方案统一。但是，当您添加通配符大小写替代项时，它会在统一过程中_ -> False引入更具限制性的主体类型，该主体类型是在没有通过模式进行任何类型细化的情况下推导出来的，可以通过提供更具限制性的类型来通知统一算法，而其他类型则为类型细化替代，可以统一。Bool_Bool

在上面，我听起来像是有一些两阶段的方法，首先检查“非精炼”替代方案以确定目标类型，然后对照它检查精炼替代方案。

事实上，所发生的情况是，细化过程将新的变量引入到统一过程中，即使它们是统一的，也不会影响更大的类型上下文。因此，所有替代方案立即统一，但未精炼替代方案的统一会影响更大的类型上下文，而精炼替代方案的统一会影响一堆新变量，从而给出相同的最终结果，就好像未精炼和精炼替代方案分别处理一样。