haskell - "succ(zero)"的类型与 GHC 中的 "one"的类型不同

Question

要求 GHC 打印“one”和“succ zero”(编码数字的 lambda 演算方式)的类型，我得到了两种不同的类型! 他们不应该是一样的吗？ 你能告诉我如何手动推导它的类型吗？

zero = \ f x -> x
one = \ f x -> f x
succ = \ n f x -> f (n (f x))

:t one -- (t1 -> t2) -> t1 -> t2

:t succ zero -- ((t1 -> t1) -> t2) -> (t1 -> t1) -> t2

Answer 1

正如评论中所说，正确的定义是

zero   f x = x
succ n f x = f (n f x)

"do one more f after n applications of f, starting with x."

因此

one f x = succ zero f x = f (zero f x) = f x
two f x = succ one  f x = f (one  f x) = f (f x)

派生的类型最初更通用，

zero     ::     t      -> t1 -> t1     -- most general
one      :: (t1 -> t ) -> t1 -> t      -- less general
succ one :: (t2 -> t2) -> t2 -> t2     -- most specific

但这没关系，它们之间都匹配(统一)，并且从 two = succ one 开始，类型稳定为最具体的 (b -> b) -> (b -> b).

你也可以定义

church :: Int -> (b -> b) -> b -> b           -- is derived so by GHCi
church n f x = foldr ($) x (replicate n f)
             = foldr (.) id (replicate n f) x
{- church n  = foldr (.) id . replicate n     -- (^ n) for functions -}

并且所有类型都完全相同，如

church 0 :: (b -> b) -> b -> b
church 1 :: (b -> b) -> b -> b
church 2 :: (b -> b) -> b -> b

真的没关系。

至于类型推导，归结为仅使用 modus ponens/application 规则，

       f   :: a -> b
         x :: a
       -------------
       f x ::      b

只需要注意一致地重命名每种类型，这样就不会在任何步骤引入类型变量捕获:

      succ n f x = f (n f x)
               x          ::      a
             f            :: t                              ,  t ~ ...
                      n   :: t -> a -> b
                   f      ::           b ->            c    ,  t ~ b -> c
      succ    n                       f           x :: c
      succ :: (t        -> a -> b) -> (b -> c) -> a -> c
           :: ((b -> c) -> a -> b) -> (b -> c) -> a -> c

(因为 succ 产生的最终结果类型与 f 产生的最终结果类型相同——即 c)，或者正如 GHCi 所说，

      succ :: ((t1 -> t) -> t2 -> t1) -> (t1 -> t) -> t2 -> t
           --   b     c     a     b       b     c     a     c