首页 文章

GADT与自定义数据类型的混淆？

提问于
浏览 次
2

我有以下自定义数据类型：

data FirstPair' a b = FirstPair a b deriving (Show, Ord, Eq)
type FirstPair a = FirstPair' a a 

data SecondPair' a b = SecondPair a b deriving (Show, Ord, Eq)
type SecondPair a = SecondPair' a a

我正在尝试为我的函数创建一个GADT结构：

data Generator a where
  Success :: FirstPair a -> Generator (SecondPair a)
  Fail :: FirstPair a -> Generator Bool

myFunction :: Generator a -> a
myFunction (Success fp) = SecondPair "21" "24"
myFunction (Fail fp) = False

'Generator'类型的作用是使我能够强制'myFunction'返回'SecondPair'的实例，如果'Success'传递给它，并且'False'如果'Fail'传递给它 .

但是，我收到此错误：

"Could not deduce: a1 ~ [Char] from the context: a ~ SecondPair' a1 a1 bound by a pattern with constructor: Success :: forall a. FirstPair a -> Generator (SecondPair a)"

我在这做错了什么？

haskell gadt

1 回答

  • 4
    myFunction :: Generator a -> a
myFunction (Success fp) = SecondPair "21" "24"
myFunction (Fail fp) = False

    问题出在这里 . 类型签名是简写

    myFunction :: forall a. Generator a -> a

    也就是说，无论我选择什么类型的 a ，如果我给 myFunction 一个 Generator a ，它会给我一个 a . 所以，如果我给它一个 Generator Int ，它应该给我一个 Int .

    所以我可以构建

    successval :: Generator (SecondPair Int)
successval = Success (FirstPair 42 42 :: FirstPair Int)

    然后将其传递给 myFunction ，并根据我应该得到的类型签名

    myFunction successVal :: SecondPair Int

    但是，定义了 myFunction 的方式，无论我传递的是什么类型，它总是会返回 SecondPair String ，并且's the problem it'抱怨 .

    如果你想要这种多态性，你需要以某种方式使用你给出的参数 . 例如 .

    myFunction (Success (FirstPair x y)) = SecondPair x y

    会做的伎俩，因为出局的 x 和 y 与 x 和 y 进入的类型相同（和 FirstPair 和 SecondPair 匹配GADT所说的那样） .

    如果你需要返回 SecondPair String 无论如何，那么 myFunction 的类型签名是错误的，需要像

    myFunction :: Generator a -> SecondPair String

    （在 Fail 的情况下，这种情况不正常 - 我还有更多的话要说，如果这是你真正想要去的路线，但它比我想写的一个在黑暗中拍摄更多一些猜测）

    或者GADT需要说结果将是 SecondPair String .

    data Generator a where
     Success :: FirstPair a -> Generator (SecondPair String)
     ...

    我不认为这些是非常可能的场景，我只是认为它们可能有助于您理解问题 .

    回复于

相关问题