haskell - 为什么 eqT 返回 Maybe (a :~: b) work better than it returning Bool?

我制作了 eqT 的一个变体，它允许我像处理任何其他 Bool 一样处理结果来编写类似 eqT' @a @T1 || eqT' @a @T2 的东西。然而，虽然这在某些情况下效果很好，但我发现我无法用它替换 eqT 的每次使用。例如，我想用它来编写 readMaybe 的变体，当它应该返回 Just 时，它只会是 String 。虽然使用 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 的类型以返回 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 中不是问题。

最佳答案

本质上，这是 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 ...，我们将消除不是 GADT 的 Bool 类型。类型检查器没有得到关于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+GADT 更难——我必须警告你。我只想补充一点，一开始对我来说依赖消除是神秘的。在我了解了 Coq 中模式匹配的一般形式后，一切都开始变得有意义了。

关于haskell - 为什么 eqT 返回 Maybe (a :~: b) work better than it returning Bool?，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/52996623/