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

【问题标题】：Unifying c -> a -> b and (a -> b) -> c统一 c -> a -> b 和 (a -> b) -> c
【发布时间】：2015-11-28 20:49:54
【问题描述】：

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

谁能解释一下我该如何解决？

谢谢！

【问题讨论】：

你可以问ghci：:t [undefined :: c -> a -> b, undefined :: (a -> b) -> c]
@Cirdec 非常好 - 尽管它不会给出完整的答案（它并没有真正得到 as 和 bs 的意思的 hint一样;)) - 无论如何：很棒的评论（甚至可能值得回答？）
@Cirdec 我认为你应该把它变成一个答案——它不仅回答了（好吧，结果确实如此）OP 的问题，而且还回答了所有问题。至于 Carsten 的评论 - 不会完全解决这个问题吗？
@joozek, @carsten 我添加了an answer，解释这些是不同的类型变量，添加foralls 不会解决问题。
@Carsten 我添加了一个答案，显示如何向 GHC 提示 as 和 bs 应该是相同的。

标签： haskell types

【解决方案1】：

这似乎是某种练习/家庭作业，所以我不会破坏所有内容，而是先给你一些提示：

c -> a -> b 的类型实际上是c -> (a -> b)
所以你必须统一 c -> (a -> b) 和(a -> b) -> c，即：
- c 和 a -> b（第一部分）
- a -> b 和 c（第二部分）

现在会是什么（尝试摆脱c ;)）现在是什么？

PS：我假设您希望这些类型 a、b、.. 相同

【讨论】：

【解决方案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作为统一问题的解决方案。这里还有一个你可能想知道的问题：统一后，(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

我在这个命令中唯一改变的是“查询”部分。结果告诉我们，统一后(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))

【讨论】：

使用一个元组来捕获统一结果的类型是非常聪明的。
let x :: ... x = undefined in x 包装器有什么原因吗？ ghci 7.8.3 很乐意接受查询:t undefined :: ((a -> b) -> c) ~ (c -> a -> b) => (a, b, c)
@Cirdec 这是一个很好的简化！我将在今天晚些时候将其包含在我的答案中。

【解决方案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]

我们已经完成了 vanilla Haskell 的功能，但您可以使用 type equality constraints as described in Daniel Wagner's answer 让编译器更一般地回答问题。下一节仅描述为什么forall 作用域类型不是通用解决方案。

全部

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

对于经验丰富的haskeller，您似乎可以通过将类型变量引入显式forall 范围并使用ScopedTypeVariables 扩展名来保持它们的不同。我不知道在 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，c 并不是一个函数。一些不是函数的示例类型包括 Int、Bool 和 IO a。

^† 在询问进入洞的类型是什么时，我使用(undefined :: _) 而不是_。如果您只使用_ ghc 不会键入检查所有表达式。编译器可能会让你相信一个漏洞是可以填补的，而实际上这是不可能的。在example2 的输出中还有以下极具误导性的行

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

【讨论】：