计算类型哈斯克尔

Question

如何计算 （.） 的类型(.)在哈斯克尔？我知道应该是

(.)(.) :: (a -> b -> c) -> a -> (a1 -> b) -> a1 -> c

但是没有计算机如何计算呢？

Answer 1

(.)    :: (b        -> c                     ) -> ((a -> b)        -> (a -> c))
   (.) :: ((e -> f) -> ((d -> e) -> (d -> f)))
(.)(.) ::                                         ((a -> (e -> f)) -> (a -> ((d -> e) -> (d -> f))))
(.)(.) :: (a -> (e -> f)) -> (a -> ((d -> e) -> (d -> f)))
(.)(.) :: (a -> e -> f) -> a -> ((d -> e) -> (d -> f))
(.)(.) :: (a -> e -> f) -> a -> (d -> e) -> (d -> f)
(.)(.) :: (a -> e -> f) -> a -> (d -> e) -> d -> f

Answer 2

通过（手动）模式匹配和重写类型变量

(.)具有类型 (b -> c) -> ((a -> b) -> a -> c ），因此第一个参数应具有类型 b -> c 。现在，如果我们再次使用它，我们必须用 b' -> c' 替换b，用 (a' -> b') -> a' -> c') 替换c（第二个(.)应该有类型 (b' -> c') -> ((a' -> b') -> a' -> c') ），我们得到

(a -> b' -> c') -> a -> (a' -> b') -> a' -> c'

（重命名后）与上述相同。

请注意，我在这里使用了a -> b -> c = a -> (b -> c)

使用 GHCi

是的，我知道 - 你想要手工 - 但GHCi是一个非常有价值的工具，你真的应该用它来确认你的体力劳动。

这里来自终端：

$ ghci
GHCi, version 7.10.1: http://www.haskell.org/ghc/  :? for help
Prelude> :t (.)(.)
(.)(.) :: (a -> b -> c) -> a -> (a1 -> b) -> a1 -> c
Prelude> 

如您所见，类型是(a -> b -> c) -> a -> (a1 -> b) -> a1 -> c

顺便说一句：:t 是 :type 的缩写，您可以从 GHCi 会话中查看所有带有:help的命令。

Answer 3

由于我对接受的答案中缺少的解释不是特别满意，所以我也给出了我的POV：

-- this is the original type signature
(.) :: (b -> c) -> (a -> b) -> a -> c
-- now because of haskell polymorphism,
-- even 'b' and 'c' and so on could be functions
--
-- (.)(.) means we shove the second function composition
-- into the first as an argument.
-- Let's give the second function a distinct type signature, so we
-- don't mix up the types:
(.) :: (e -> f) -> (d -> e) -> d -> f
-- Since the first argument of the initial (.) is of type (b -> c)
-- we could say the following if we apply the second (.) to it:
(b -> c) == (e -> f) -> (d -> e) -> d -> f
-- further, because of how currying works, as in
(e -> f) -> (d -> e) -> d -> f == (e -> f) -> ((d -> e) -> d -> f)
-- we can conclude
b == (e -> f)
c == (d -> e) -> d -> f
-- since we passed one argument in, the function arity changes,
-- so we'd actually only have (a -> b) -> a -> c left, but that
-- doesn't represent the types we have now, so we have to substitute
-- for b and c, so
(a -> b) -> a -> c
-- becomes
(.)(.) :: (a -> (e -> f)) -> a -> (d -> e) -> d -> f
-- and again because of currying we can also write
(.)(.) :: (a -> e -> f) -> a -> (d -> e) -> d -> f