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

Question

我做了 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 中不是问题.

Answer 1

本质上，这是一个 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+GADT 难一些——我必须警告你。我只会补充一点，依赖消除起初对我来说很神秘。在我理解了 Coq 中模式匹配的一般形式之后，一切都开始变得很有意义了。