这张图中的 f 有多种类型？

Question

https://youtu.be/brE_dyedGm0?t=1362

data T a where
  T1 :: Bool -> T Bool
  T2 :: T a

f x y = case x of
  T1 x -> True
  T2   -> y

Simon 说f可以输入为T a -> a -> a，但我认为返回值必须是 Bool，因为这是 case 表达式分支中的显式结果。这是关于 Haskell GADT 的。为什么会这样呢？

Answer 1

这就是 GADT 的全部要点。构造函数上的匹配可能会导致其他类型信息进入作用域。

让我们看看当 GHC 检查以下定义时会发生什么：

f :: T a -> a -> a
f x y = case x of
    T1 _ -> True
    T2   -> y

让我们先看一下这个T2案例，只是为了摆脱困境。y并且结果具有相同的类型，并且T2是多态的，因此您可以声明它的类型也是T a. 都好。

接下来是更棘手的情况。x请注意，我删除了内部名称的绑定case，因为阴影可能会令人困惑，未使用内部值，并且它不会更改说明中的任何内容。当您匹配 GADT 构造函数（例如T1显式设置类型变量的构造函数）时，它会在该分支内引入额外的约束，以添加该类型信息。在这种情况下，匹配T1会引入(a ~ Bool)约束。这种类型相等说明了a和Bool彼此匹配。因此，具有类型的文字True与类型签名中写入的Bool文字相匹配。未使用，因此该分支与 一致。ayT a -> a -> a

所以一切都匹配。T a -> a -> a是该定义的有效类型。但正如西蒙所说，这是模棱两可的。T a -> Bool -> Bool也是该定义的有效类型。两者都不比另一个更通用，因此该定义没有原则类型。因此，除非提供类型，否则定义将被拒绝，因为推理无法为其选择一个最正确的类型。