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

【问题标题】：GADT confusion with custom data types?GADT 与自定义数据类型混淆？
【发布时间】：2016-11-06 22:40:04
【问题描述】：

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

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'在'Success'被传递给它时返回'SecondPair'的实例，如果'Fail'被传递给它，'False'。

但是，我收到了这个错误：

"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)"

我在这里做错了什么？

【问题讨论】：

您的问题似乎缺少一些代码。您的错误引用了ContextaPair'，但您没有提及。你能发布你的实际代码吗？
您仍然没有运行您发布的相同代码。您的代码中没有 [Char] 值。

标签： haskell gadt

【解决方案1】：

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，这就是它所抱怨的问题。

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

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)
     ...

我认为这些情况不太可能发生，我只是认为它们可能有助于您理解问题。

【讨论】：