haskell 为什么Int类型不能与a类型匹配

yk9xbfzb 于 2022-11-14 发布在其他

关注(0)|答案(4)|浏览(197)

我是 haskell ·努布。
我在这里要做的是一个过于简单的例子：

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

这是怎么回事？有没有办法解决这个问题，或者只是一些你不能做的事情？

haskell

来源：https://stackoverflow.com/questions/70490514/why-cant-i-match-type-int-with-type-a

4条答案

按热度按时间

ki0zmccv1#

对于你想写的GADT函数，标准的技术是使用单例。问题是EnumType类型的值是值级别的东西，但是你想通知类型系统一些东西。所以你需要一种方法来连接 kindEnumType的 types 和 typeEnumType的 values（它本身有kind Type）。这是不可能的，所以我们作弊：我们将x1m5 n1,类型的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，模式匹配将使您能够观察a是Enum1、Enum2还是Enum3。

赞(0）回复(0）举报 2022-11-14

wgmfuz8q2#

有没有办法解决这个问题，或者只是一些你不能做的事情？
恐怕这只是“你做不到的事”，原因很简单。
当你编写一个类型签名时，比如（举第一个更简单的例子）

test :: Int -> a

或者，把它写得更字面，更扩展的形式

test :: forall a. Int -> a

你是说，从字面上看，“对于所有a“，这个函数可以接受一个Int，并返回一个a类型的值。（这不是实际的代码，但是想象一下，您将test 2的结果提供给一个需要Char或其他类型的函数）：

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。（如果您希望这样做，我建议您提出一个单独的问题，详细说明您在这里实际需要什么。）

赞(0）回复(0）举报 2022-11-14

hrirmatl3#

如前所述，您的签名表示一个通用类型

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

1.也许您甚至不需要一个单独的类型，而只需将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

1.通过展开一层延续传递风格，然后通过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)

赞(0）回复(0）举报 2022-11-14

3qpi33ja4#

你想写的GADT函数，标准的技术是使用单例。问题是类型EnumType的值是...

赞(0）回复(0）举报 2022-11-14