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

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

在 中键入 case 构造(无论是显式 case 语句还是隐式基于模式的函数定义)缺席 GADTs，个别的替代品:

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 表达式的类型 Bool ，将其与 isA 的类型统一起来获取 isA :: U -> Bool .

请注意，统一过程可以使类型特化。在这里，模式的类型 x :: a是通用的，但在统一过程结束时，它已专门用于 x :: U .这也可能发生在 body 上。例如:

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

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

一般来说，通过统一，所有主体的公共(public)、统一类型(以及整个 case 表达式的类型)将是“最一般”/“限制最少”的类型，其中主体的类型都是泛化。在某些情况下，这种类型可能是其中一个实体的类型，但一般来说，所有实体都可以比“最一般”的统一类型更通用，但没有任何实体可以更具限制性。

在 GADT 的存在下，情况会发生变化。当使用 GADT 进行类型检查 case 构造时，替代方案中的模式可以引入“类型细化”，即一组附加的类型变量绑定(bind)，用于对替代方案的主体进行类型检查。 (这就是首先使 GADT 有用的原因。)

因为不同替代品的 body 是在不同的细化下键入的，所以不可能进行天真的统一。例如，考虑微型类型的 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

如果我们天真地统一 body n :: Int , eval t == 0 :: Bool , 和 if eval b then eval t else eval e :: a ，程序不会进行类型检查(最明显的是，因为 Int 和 Bool 不统一!)。

一般来说，因为类型改进允许替代体的计算类型比最终类型更具体，所以没有明显的“最通用”/“限制最少”的类型可以统一所有体，就像没有 GADT 的 case 表达式。

相反，我们通常需要为整个 case 表达式提供一个“目标”类型(例如，对于 eval，类型签名中的返回类型 a)，然后确定是否在每个由构造函数引入的细化下(例如， IsZ 引入细化 a ~ Bool )，主体 eval t == 0 :: Bool具有相关的细化 a 作为其类型.

如果没有明确提供目标类型，那么我们能做的最好的事情——一般来说——是使用一个新的类型变量 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 试图做的是输入 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 .在这种细化下， body 的实际类型 True :: Bool匹配目标类型的“细化” Bool (“精炼”为 Bool )，并且确定替代品具有有效类型。

因此，直觉是，如果没有通配符替代，case 表达式的推断类型是任意类型变量 p ，这太笼统了，无法与类型提炼替代方案统一。但是，当您添加通配符大小写替代时 _ -> False ，它引入了更严格的体型 Bool进入统一过程，由模式 _ 推导出没有任何类型细化, 可以通过提供更严格的类型 Bool 来通知统一算法可以统一其他类型的精制替代品。

上面，我认为有一些两阶段方法，其中首先检查“非精炼”替代方案以确定目标类型，然后对照它检查精炼替代方案。

事实上，细化过程将新变量引入到统一过程中，即使它们被统一，也不会影响更大的类型上下文。因此，所有备选方案同时统一，但未精炼备选方案的统一会影响较大类型的上下文，而精炼备选方案的统一会影响一堆新变量，得出的最终结果与未精炼和完善的备选方案分别处理一样。