当Haskell类型合成器统一类型c -> a -> b
和(a -> b) -> c
时,推断出的类型是什么?
有人可以解释一下我如何解决它吗?
谢谢!
这似乎是一些练习/作业,所以我不会泄露所有内容,而是先给你一些提示:
c -> a -> b
实际上是 c -> (a -> b)
c -> (a -> b)
与 (a -> b) -> c
进行合一,也就是:
c
与 a -> b
(第一部分)a -> b
与 c
(第二部分)现在,那么那个(试着摆脱c
;) )是什么呢?
PS:我假设您希望那些类型 a
,b
等相同。
ghci
提出一些有限的合一问题。在本答案中,我将展示如何使用现有的工具来回答您所提出的问题,就我理解的意思而言。> :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
(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你可以询问ghci
:t [undefined :: c -> a -> b, undefined :: (a -> b) -> c]
:t [undefined :: c1 -> a1 -> b1, undefined :: (a2 -> b2) -> c2]
forall
范围的类型不是通用解决方案。
c -> a -> b
和(a -> b) -> c
,对于所有c
。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] -> ()
:t [undefined :: c -> a -> b, undefined :: (a -> b) -> c]
- Cirdeca
和b
应该是相同的 提示 ;)) - 无论如何: 很棒的评论(甚至可能值得一个回答?) - Random Devforall
也无法解决问题。 - Cirdeca
和b
是相同的。 - Daniel Wagner