如何手动推断 '(.) 的类型。 (.) 。 (.)'?

Question

在 Edward Kmett 的演讲 Lenses, Folds, and Traversals 中，在幻灯片 "The Power is in the Dot" 中，他显示 (.) . (.) . (.) 的类型是

(a -> b) -> (c -> d -> e -> a) -> c -> d -> e -> b

我可以通过在 GHCI 中显示它的类型来查看它。但我也想知道为什么。我想了解的另一件事是为什么参数从 (.) 到 (.) . (.) 和 (.) . (.) . (.):

的定期更改存在模式

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

P.S。我试图通过扩展 (.) . (.) 的函数定义来解决 (.) . (.) 自己的问题。应用 (.) 的定义后，我得到：

\x y z t -> x ((y z) t)

所以我推断出类型：

x :: a -> b
y :: c -> d -> a
z :: c
t :: d

然而我在 (.) . (.) . (.) 迷路了。而且我不知道这是否是进行手动类型推断的正确方法。

Answer 1

有函数，

instance Functor ((->) r) where
   -- fmap :: (a -> b) ->   f   a  ->   f   b
   --         (a -> b) -> (r -> a) -> (r -> b)
   fmap          p           q         x = p (q x)   -- fmap = (.)

所以你实际拥有的是 fmap . fmap . fmap:

fmap               :: (a -> b) -> f       a   -> f       b
fmap . fmap        :: (a -> b) -> f (g    a)  -> f (g    b)
fmap . fmap . fmap :: (a -> b) -> f (g (h a)) -> f (g (h b))

也就是

 (a -> b) -> (c -> (d -> (e -> a))) -> (c -> (d -> (e -> b)))   ~
 (a -> b) -> (c ->  d ->  e -> a)   -> (c ->  d ->  e -> b)

为什么是fmap . fmap :: (a -> b) -> f (g a) -> f (g b)？因为，

(fmap . fmap) foo = fmap (fmap foo)
{-
fmap            :: (a  ->  b) -> f a     -> f b
foo             ::  a  ->  b
fmap foo        ::               f a     -> f b
fmap foo        :: g a -> g b
fmap (fmap foo) ::               f (g a) -> f (g b)
-}

机械类型派生就是类型变量的替换和一致重命名。查看更多here or here.

Answer 2

(.) . (.) . (.)分两步归约：先归约没有括号的点：

((.) . (.) . (.)) f = (.) ((.) ((.) f))
                    = (.) ((.) (f .))
                    = (.) ((f .) .)
                    = ((f .) .) .)

秒减少剩余的表达式

((f .) .) .) g = ((f .) .) . g
               = \x -> ((f .) .) (g x)
               = \x -> (f .) . g x
               = \x y -> (f .) (g x y)
               = \x y -> f . g x y
               = \x y z -> f (g x y z)

所以首先你用 n - 1 点在括号中组成 n 点。然后将此构造应用于函数 f :: a -> b 和 g 并得到 (...((f .) .) ... .) g，其中每个点对应于 g 接收的一个参数——这就是为什么有一个模式：每个点在括号处理 g 的一个参数，你需要另一个点来将这个点与之前的所有点组合起来。在所有归约之后，表达式变为

\x1 x2 ... xn -> f (g x1 x2 ... xn)

其类型一目了然

一件好事是，如果我们有后缀运算符，我们就可以编写（代码在 Agda 中）

open import Function renaming (_∘′_ to _∘_) using ()

_% = _∘_

postulate
  a b c d e : Set
  f : a -> b
  g : c -> d -> e -> a

fg : c -> d -> e -> b
fg = f % % ∘ g

而不是 ((f .) .) . g。

如何手动推断 '(.) 的类型。 (.) 。 (.)'?

How to manually infer the type of '(.) . (.) . (.)'?

haskell

types

type-inference

function-composition

combinators