为什么我不能将 Int 类型与 a 类型匹配答案

【问题标题】：Why can't I match type Int with type a为什么我不能将 Int 类型与 a 类型匹配
【发布时间】：2022-01-26 03:00:29
【问题描述】：

Haskell Noob 在这里。

我在这里尝试做的一个过于简单的案例：

test :: Int -> a
test i = i -- Couldn't match expected type ‘a’ with actual type ‘Int’. ‘a’ is a rigid type variable bound by ...

我不太明白为什么这不起作用。我的意思是，Int 肯定包含在 a 类型的东西中。

我真正想要实现的是：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

data EnumType = Enum1 | Enum2 | Enum3

data MyType (a :: EnumType) where
  Type1 :: Int -> MyType 'Enum1
  Type2 :: String -> MyType 'Enum2
  Type3 :: Bool -> MyType 'Enum3

myFunc :: EnumType -> MyType 'Enum1 -> MyType any
myFunc Enum1 t = t -- Can't match type `any` with `Enum1`. any is a rigid type variable bound by ...
myFunc Enum2 _ = Type2 "hi"
myFunc Enum3 _ = Type3 True

这里发生了什么？有没有办法解决这个问题，或者它只是你不能做的事情？

【问题讨论】：

您的函数承诺对于 any a，它可以将 Int 转换为 a，因此如果您确定 a 是 @987654330 @，那么您的函数应该仍然能够将Int 转换为Char。
这与 Java 不同，例如，object 的返回类型承诺输出将是对象的子类。但是在哪里无法通过调用函数来决定该对象将是什么。
您可能会喜欢我对Why can a Num act like a Fractional? 的回答。简而言之：它是test 的调用者，而不是实现者，可以选择将a 专门化为什么单态值；他们可能会选择不是Int。

标签： haskell

【解决方案1】：

您要编写的 GADT 函数，标准技术是使用单例。问题是 EnumType 类型的值是website...

【讨论】：

【解决方案2】：

如前所述，您的签名表达了一种通用类型

myFunc :: ∀ a . EnumType -> MyType 'Enum1 -> MyType a

而你真正想要表达的是一个存在类型

myFunc :: EnumType -> MyType 'Enum1 -> (∃ a . MyType a)

Haskell 没有类似的功能，但它确实有一些方法可以实现基本相同的目标。

GADT 和 ExistentialTypes 扩展都允许表达存在，但您需要为它们定义单独的类型。

data MyDynType where
  MyDynWrap :: MyType a -> MyDynType

myFunc :: EnumType -> MyType 'Enum1 -> MyDynType
myFunc Enum1 t = MyDynWrap t
myFunc Enum2 _ = MyDynWrap $ Type2 "hi"
myFunc Enum3 _ = MyDynWrap $ Type3 True

也许您甚至不需要单独的类型，但可以简单地将 MyType 首先修改为“动态”。

data MyType = Type1 Int | Type2 String | Type3 Bool

myFunc :: EnumType -> MyType -> MyType
myFunc Enum1 (Type1 i) = Type1 i
myFunc Enum2 _ = Type2 "hi"
myFunc Enum3 _ = Type3 True

通过展开一层连续传递样式，然后通过 RankNTypes 扩展使用对偶全称量词，可以匿名地在现场模拟存在。

{-# LANGUAGE RankNTypes #-}

data MyType (a :: EnumType) where ... -- as original

myFunc :: EnumType -> MyType 'Enum1 -> (∀ a . MyType a -> r) -> r
myFunc Enum1 t q = q t
myFunc Enum2 _ q = q (Type2 "hi")
myFunc Enum3 _ q = q (Type3 True)

【讨论】：

【解决方案3】：

对于您要编写的 GADT 函数，标准技术是使用单例。问题是EnumType 类型的值是值级别的东西，但你想通知类型系统一些东西。所以你需要一种方法来连接 types of kind EnumType 与 values of type EnumType (本身有种Type)。这是不可能的，所以我们作弊：我们将类型 EnumType 的类型 x 与新类型 SEnumType x 的值连接起来，使得该值唯一地确定 x。下面是它的外观：

data SEnumType a where
    SEnum1 :: SEnumType Enum1
    SEnum2 :: SEnumType Enum2
    SEnum3 :: SEnumType Enum3

myFunc :: SEnumType a -> MyType Enum1 -> MyType a
myFunc SEnum1 t = t
myFunc SEnum2 _ = Type2 "hi"
myFunc SEnum3 _ = Type3 True

现在返回类型MyType a 中的a 不仅仅是凭空捏造的；它被限制为等于从SEnumType 传入的a，并且SEnumType 所在的模式匹配可以让您观察a 是Enum1、Enum2 还是Enum3。

【讨论】：

【解决方案4】：

有没有办法解决这个问题，或者它只是你不能做的事情？

恐怕这只是“你不能做的事情”。原因很简单。

当您编写类型签名时（以您的第一个更简单的示例为例）

test :: Int -> a

或者，写成更直接的扩展形式

test :: forall a. Int -> a

你的意思是，“对于所有a”，这个函数可以接受一个Int 并返回一个a 类型的值。这很重要，因为调用代码必须相信这种类型签名，因此能够执行类似的操作（这不是现实的代码，但想象一下将test 2 的结果提供给需要@ 的函数的情况987654326@ 或其他类型之一）：

test 2 :: Char
test 2 :: [Int]
test 2 :: (Double, [Char])

等等。显然，您的函数不能与这些示例中的任何一个一起使用 - 但如果您给它此类型签名，它必须能够与其中的任何一起使用。很简单，您的代码不适合该类型签名。（而且也不可能，除非你通过使用 test x = undefined 来“作弊”。）

这应该不是问题 - 编译器只是在保护您免于出错，因为我确信您意识到您的代码不能满足这种类型签名。以你的“真实”为例：

myFunc :: EnumType -> MyType Enum1 -> MyType any

虽然这会产生编译错误，但您在函数中的代码可能是正确的，问题在于类型签名。如果您将其替换为

myFunc :: EnumType -> MyType Enum1 -> MyType Enum1

然后它将编译（除非有任何进一步的错误，我没有检查过它），并且可能会做你想做的事。看起来您实际上并不希望能够调用myFunc 并让它产生例如MyType Int。（如果你有任何机会，我建议你问一个单独的问题，在这里详细说明你实际需要什么。）

【讨论】：