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

Question

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

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

谢谢!

Answer 1

这似乎是某种运动/家庭作业所以我不会破坏一切,但首先给你一些提示:

• c -> a -> b实际上是这种类型c -> (a -> b)
• 所以你必须统一 c -> (a -> b)使用(a -> b) -> c,那就是:
  • c与a -> b(第一部分)
  • a -> b与c(第二部分)

现在可以做什么(试图摆脱c;))？

PS:我假设你想要的类型a,b..是相同的

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为解决国家统一问题.以下是您可能想知道的另一个问题:统一后,简化类型是(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))

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]

我们已经完成了vanilla Haskell可以做的事情,但是你可以让编译器通过使用Daniel Wagner的答案中描述的类型相等约束更一般地回答问题.下一节只描述了forall作用域类型不是通用解决方案的原因.

对全部

之前阅读本节你应该考虑是否有可能结合起来,为所有c,c -> a -> b和(a -> b) -> c.

对于有经验的haskeller,看起来你可以通过forall在ScopedTypeVariables扩展的显式范围中引入它们来保持类型变量不同.我不知道一个简单的方法在ghci中做到这一点,但有下列snipet 孔^†要求编译器统一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] -> ()