统一 c -> a -> b 和 (a -> b) -> c

Question

当Haskell类型合成器统一类型c -> a -> b和(a -> b) -> c时，推断出的类型是什么？

有人可以解释一下我如何解决它吗？

谢谢！

- yonutix

---

你可以在ghci中输入以下命令：:t [undefined :: c -> a -> b, undefined :: (a -> b) -> c] - Cirdec

@Cirdec 很好 - 尽管它不会给出完整的答案（它实际上没有真正理解这些 a 和 b 应该是相同的 提示 ;)) - 无论如何: 很棒的评论（甚至可能值得一个回答？） - Random Dev

@Cirdec 我认为你应该把这个变成一个答案——它不仅回答了 OP 的问题，还回答了整个类别的问题（至少是结果）。至于 Carsten 的评论——使用 forall 无法解决这个问题吗？ - joozek

@joozek，@carsten 我添加了一个答案，解释了这些是不同的类型变量，并且添加forall也无法解决问题。 - Cirdec

@Carsten，我已经添加了一个答案，展示了如何给GHC提示那些a和b是相同的。 - Daniel Wagner

@DanielWagner 不错 :D - Random Dev

Answer 1

这似乎是一些练习/作业，所以我不会泄露所有内容，而是先给你一些提示：

• 类型 c -> a -> b 实际上是 c -> (a -> b)
• 因此，您必须将 c -> (a -> b) 与 (a -> b) -> c 进行合一，也就是：
  • c 与 a -> b（第一部分）
  • a -> b 与 c（第二部分）

现在，那么那个（试着摆脱c ;) ）是什么呢？

PS：我假设您希望那些类型 a，b 等相同。

- Random Dev

Answer 2

在其他答案中，我们已经看到了如何手动执行合一操作，以及在我们不需要连接要合一的两个类型中的类型变量时，如何向ghci提出一些有限的合一问题。在本答案中，我将展示如何使用现有的工具来回答您所提出的问题，就我理解的意思而言。

诀窍是使用类型相等约束来要求GHC统一两种类型，然后将结果公开为元组类型。类型相等约束启动合一器；当合一完成时，我们元组类型中的类型变量将根据在合一期间学到的知识进行简化。

因此，例如，您的问题如下：

> :set -XTypeFamilies
> :{
| :t undefined -- a dummy implementation we don't actually care about
| :: ((a -> b) -> c) ~ (c -> a -> b) -- the unification problem
| => (a, b, c) -- how we ask our query (what are the values of a, b, and c after unification?)
| :}
<snip -- a copy of the above text>
  :: (a, b, a -> b)

从这里我们可以得知，对于任意类型的a和b，我们都可以选择a ~ a、b ~ b和c ~ a -> b作为解决unification问题的方案。以下是另一个你可能会想到的问题：在统一之后，(a -> b) -> c的简化类型是什么？你可以运行前面的查询，并手动替换a、b和c，或者你可以询问ghci：

> :t undefined :: ((a -> b) -> c) ~ (c -> a -> b) => (a -> b) -> c
undefined :: ((a -> b) -> c) ~ (c -> a -> b) => (a -> b) -> c
  :: (a -> b) -> a -> b

这个命令中我改变的唯一部分是“query”的部分。结果告诉我们，在统一后，(a -> b) -> c 变成了 (a -> b) -> a -> b。请注意，结果类型中的 a 和 b 并不能保证与查询中的 a 和 b 完全相同，尽管在 GHC 中可能总是这样。

另一个值得一提的快捷技巧是，您可以使用 Proxy 将任意种类的类型变量转换为 * 类型，以便在元组中使用；例如：

> :t undefined :: f a ~ (b -> c) => (a, b, c, f)

<interactive>:1:42:
    Expecting one more argument to ‘f’
    The fourth argument of a tuple should have kind ‘*’,
      but ‘f’ has kind ‘* -> *’
    In an expression type signature: f a ~ (b -> c) => (a, b, c, f)
    In the expression: undefined :: f a ~ (b -> c) => (a, b, c, f)
> :m + Data.Proxy
> :t undefined :: f a ~ (b -> c) => (a, b, c, Proxy f)
undefined :: f a ~ (b -> c) => (a, b, c, Proxy f)
  :: (c, b, c, Proxy ((->) b))

- Daniel Wagner

---

使用元组来捕获统一结果的类型是非常聪明的。 - Cirdec

let x :: ... x = undefined in x 包装器有什么意义吗？ghci 7.8.3 可以接受查询 :t undefined :: ((a -> b) -> c) ~ (c -> a -> b) => (a, b, c)。 - Cirdec

@Cirdec 这是一个不错的简化！我稍后会在我的答案中包含它。 - Daniel Wagner

Answer 3

你可以询问ghci

:t [undefined :: c -> a -> b, undefined :: (a -> b) -> c]

它需要统一类型以确定列表元素的类型。我们可以通过这种方式统一任意数量的类型；甚至是0，试试吧！

在 c->a->b 中左侧的类型变量与 a->b->c 中右侧的类型变量不同。 GHC会重命名类型变量以保持它们的不同，但会尝试保留原始名称。它通过在类型变量名称的末尾添加数字来实现此目的。此查询的答案包括一些类型变量 a ， a1 ， b ， b1 ， c 和 c1 。如果您不希望类型变量不同，则可以忽略添加的数字读取答案。

如果确实希望类型变量不同，则可能有点棘手，因为您不知道ghc正在做什么，因为您不知道哪个类型变量被重命名为什么。在实际编码中，当尝试理解类型错误时，这可能是一个问题。在两种情况下都有一个简单的解决方案：使用具有独特名称的类型变量自己重命名类型变量，以便ghc不需要重命名它们。

:t [undefined :: c1 -> a1 -> b1, undefined :: (a2 -> b2) -> c2]

我们已经完成了纯Haskell所能完成的工作，但是您可以通过使用类型相等约束，如Daniel Wagner的答案中所述，让编译器更普遍地回答问题。下一节仅描述了为什么forall范围的类型不是通用解决方案。

forall

在阅读本节之前，您应该考虑是否可以统一c -> a -> b和(a -> b) -> c，对于所有c。

对于有经验的Haskeller来说，似乎可以通过引入ScopedTypeVariables扩展中的显式forall作用域来避免类型变量不同。我不知道在ghci中如何轻松实现这一点，但以下带有hole^†的代码片段要求编译器统一a -> b和a -> b。

{-# LANGUAGE ScopedTypeVariables #-}

example1 :: forall a b. ()
example1 = (undefined :: _) [undefined :: a -> b, undefined :: a -> b]

输出似乎告诉我们，该列表是一个 a -> b 的列表。

Found hole `_' with type: [a -> b] -> ()

如果我们尝试将其用于示例问题，它将无法正常工作。

example2 :: forall a b c. ()
example2 = (undefined :: _) [undefined :: c -> a -> b, undefined :: (a -> b) -> c]

编译器礼貌地告诉我们原因^†。

Couldn't match type `c' with `a -> b'

并不是所有类型 c 都是函数。一些不是函数的例子包括 Int, Bool, 和 IO a。

---

^† 当询问一个空洞应该填入的类型时，我使用(undefined :: _)而不是_。如果仅使用_，ghc就不能对整个表达式进行类型检查。编译器可能会让你认为可以填补一个空洞，但实际上是不可能的。在example2的输出中还有以下极具误导性的行：

Found hole `_' with type: [c -> a -> b] -> ()

- Cirdec