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

Question

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

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

{-# 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 aghc 抱怨的结果：

{-# 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 ()

我有点明白为什么它会抱怨，但我不明白为什么它在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

thena~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 中模式匹配的一般形式后，一切都开始变得有意义了。

Answer 2

感谢 bergey 和 chi，我想我理解了导致 GHC 将错误返回给我的一系列步骤。它们都是很好的答案，但我认为我的大部分误解是不理解 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。但是，Justis type a -> Maybe a，它不是超集，因为 case 表达式应该包含类似String -> Maybe Int但Just不能返回的内容，因为它需要 for String ~ Int。这就是与 匹配时发生的情况Bool。GHC 表示，它无法将返回的内容与所要求的Maybe String Just更一般的内容相匹配。Read a => Maybe a

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