为什么 eqT 返回 Maybe (a :~: b) 比返回 Bool 效果更好？

Question

我做了一个 eqT 的变体，它允许我像处理任何其他 Bool 一样处理结果，从而写出类似 eqT' @a @T1 || eqT' @a @T2 的东西。然而，虽然这在某些情况下效果很好，但我发现我无法用它替换所有 eqT 的使用。例如，我想用它来编写 readMaybe 的变体，当它应该是 return 和 String 时，它只是 Just。虽然使用 eqT 允许我将类型保持为 String -> Maybe a，但使用 eqT' 需要类型为 String -> Maybe String。这是为什么？我知道我可以通过其他方式做到这一点，但我想知道为什么这不起作用。我想这与 GADT 的 case 表达式中的特殊处理有关（a :~: b 是 GADT），但这种特殊处理是什么？

这是我正在谈论的一些示例代码：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Typeable
import Text.Read

eqT' :: forall a b. (Typeable a, Typeable b) => Bool
eqT' = case eqT @a @b of
    Just Refl -> True
    _ -> False

readMaybeWithBadType1 :: forall a. (Typeable a, Read a) => String -> Maybe String
readMaybeWithBadType1 = if eqT' @a @String
    then Just
    else readMaybe

readMaybeWithBadType2 :: forall a. (Typeable a, Read a) => String -> Maybe String
readMaybeWithBadType2 = case eqT' @a @String of
    True -> Just
    False -> readMaybe

readMaybeWithGoodType :: forall a. (Typeable a, Read a) => String -> Maybe a
readMaybeWithGoodType = case eqT @a @String of
    Just Refl -> Just
    _ -> readMaybe

main :: IO ()
main = return ()

将 readMaybeWithBadType 的类型更改为 return Maybe a 导致 ghc 抱怨：

u.hs:16:14: error:
    • Couldn't match type ‘a’ with ‘String’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          readMaybeWithBadType1 :: forall a.
                                   (Typeable a, Read a) =>
                                   String -> Maybe a
        at u.hs:14:5-80
      Expected type: String -> Maybe a
        Actual type: a -> Maybe a
    • In the expression: Just
      In the expression: if eqT' @a @String then Just else readMaybe
      In an equation for ‘readMaybeWithBadType1’:
          readMaybeWithBadType1 = if eqT' @a @String then Just else readMaybe
    • Relevant bindings include
        readMaybeWithBadType1 :: String -> Maybe a (bound at u.hs:15:5)
   |
16 |         then Just
   |              ^^^^

u.hs:21:17: error:
    • Couldn't match type ‘a’ with ‘String’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          readMaybeWithBadType2 :: forall a.
                                   (Typeable a, Read a) =>
                                   String -> Maybe a
        at u.hs:19:5-80
      Expected type: String -> Maybe a
        Actual type: a -> Maybe a
    • In the expression: Just
      In a case alternative: True -> Just
      In the expression:
        case eqT' @a @String of
          True -> Just
          False -> readMaybe
    • Relevant bindings include
        readMaybeWithBadType2 :: String -> Maybe a (bound at u.hs:20:5)
   |
21 |         True -> Just
   |                 ^^^^

我有点明白为什么它在抱怨，但我不明白为什么它在 readMaybeWithGoodType 中不是问题。

Answer 1

您发现了 the documentation 所描述的

To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

在 Maybe a 上的大多数 case 匹配中，在 Just 分支中我们有一个额外的值，如果类型 a 我们可以使用。同样，在 readMaybeWithGoodType 的 Just 分支中，还有一个附加值。 Refl 在术语级别不是很有趣，但在类型级别很有趣。在这里它向 GHC 传达了一个我们通过检查知道的事实——当且仅当 a 是 String.

时这个分支是可达的

你是对的，其他 GADT 构造函数也可以将类型信息（通常是对其参数的类型 class 约束）引入范围。

Answer 2

本质上，这是一个 GADT 与非 GADT 消除的案例。

当我们想要使用值 x :: T 时，其中 T 是某种代数数据类型，我们求助于模式匹配（也称为“消除”）

case x of
  K1 ... -> e1
  K2 ... -> e2
  ...

其中 Ki 涵盖了所有可能的构造函数。

有时，我们不使用 case 而使用其他形式的模式匹配（例如定义方程式），但这无关紧要。另外，if then else完全等同于case of True -> .. ; False -> ...，所以不用讨论了。

现在，关键是我们要消除的类型 T 可能是 GADT，也可能不是。

如果不是一个GADT，那么所有的分支e1,e2,...都会进行类型检查，并且要求它们的类型相同。这是在不利用任何其他类型信息的情况下完成的。

如果我们写 case eqT' @a @b of ... 或 if eqT' @a @b then ...，我们将消除类型 Bool，它不是 GADT。类型检查器没有得到关于a,b的信息，检查两个分支是否具有相同的类型（可能会失败）。

相反，如果 T 是 GADT，类型检查器会利用更多类型信息。特别是，如果我们有 case x :: a :~: b of Refl -> e，类型检查器会学习 a~b，并在类型检查 e.

时利用它

如果我们有多个分支，比如

case x :: Maybe (a :~: b) of
   Just Refl -> e1
   Nothing   -> e2

然后 a~b 仅用于 e1，正如直觉所暗示的那样。

如果你想要自定义 eqT'，我建议你试试这个：

data Eq a b where
   Equal   :: Eq a a
   Unknown :: Eq a b

eqT' :: forall a b. (Typeable a, Typeable b) => Eq a b
eqT' = case eqT @a @b of
   Just Refl -> Equal
   Nothing   -> Unknown

readMaybe3 :: forall a. (Typeable a, Read a) => String -> Maybe String
readMaybe3 = case eqT' @a @String of
    Equal -> Just
    Unknown -> readMaybe

诀窍是消除 GADT，它提供有关手头类型变量的正确信息，就像在本例中一样。

如果您想更深入，可以查看具有完全依赖类型的语言（Coq、Idris、Agda 等），我们在其中发现依赖与非依赖消除的相似行为。这些语言比 Haskell+GADTs 要难一些——我必须警告你。我只会补充说，依赖消除起初对我来说很神秘。在我理解了 Coq 中模式匹配的一般形式之后，一切都开始变得有意义了。

Answer 3

感谢 bergey 和 chi，我想我理解了导致 GHC return 那个错误的一系列步骤。它们都是很好的答案，但我认为我的大部分误解是不理解 Haskell 进行类型检查的具体步骤以及它与 GADT 模式匹配的关系，在这种情况下。我将根据我的理解写一个描述此问题的答案。

因此，首先，使 GADT 成为 GADT 的其中一件事是您可以定义一个求和类型，其中每个选项可以是不同的类型，该类型比数据声明头部给出的类型更具体.这使得以下成为可能：

data a :~: b where
  Refl :: a :~: a

所以这里我们只有一个构造函数，Refl，它是一个 a :~: b，但更具体地说，这个特定的构造函数（尽管是唯一一个）产生 a :~: a。如果我们将其与 Maybe 组合以获得类型 Maybe (a :~: b)，那么我们有 2 个可能的值：Just Refl :: Maybe (a :~: a) 和 Nothing :: Maybe (a :~: b)。这就是类型通过模式匹配携带类型相等信息的方式。

现在，要使 GADT 与模式匹配一起工作，必须做一些很酷的事情。那就是与每个模式匹配的表达式可能比整个模式匹配表达式（例如 case 表达式）更专业。使用 GADT 构造函数中包含的添加的类型细化来进一步专门化匹配表达式所需的类型是 Haskell 在模式匹配中对 GADT 所做的特殊处理。所以当我们这样做时：

readMaybeWithGoodType :: forall a. (Typeable a, Read a) => String -> Maybe a
readMaybeWithGoodType = case eqT @a @String of
    Just Refl -> Just
    _ -> readMaybe

eqT是Maybe (a :~: b)，eqT @a @String，匹配的_是(Typeable a, Read a) => Maybe (a :~: String)，但是Just Refl是Maybe (String :~: String)。

Haskell 将要求整个 case 表达式是 (Typeable a, Read a) => String -> Maybe a 的类型超集。 _ 匹配只是 readMaybe 是类型 Read a => String -> Maybe a，它是一个超集。但是，Just 是 a -> Maybe a 类型，它不是超集，因为 case 表达式应该包括 String -> Maybe Int 但 Just 不能 return 因为它需要 String ~ Int。这就是匹配 Bool 时发生的情况。 GHC 告诉它无法匹配 Maybe String Just 将 return 与它所需要的更通用的 Read a => Maybe a。

这是包含此类型相等信息的构造函数上的模式匹配很重要的地方。通过匹配 Just Refl :: Maybe (String :~: String)，Haskell 不需要匹配表达式是 (Typeable a, Read a) => String -> Maybe a 的类型超集，它只需要它是 String -> Maybe String 的超集（a原始所需类型的子集类型），它是 a -> Maybe a.

为什么 eqT 返回 Maybe (a :~: b) 比返回 Bool 效果更好？

Why does eqT returning Maybe (a :~: b) work better than it returning Bool?

haskell

ghc

gadt