"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 与 one 的类型相同。在 zero 的等式中，您没有在 -> 的右侧使用 f。所以编译器不知道要推断什么类型。在 one 的等式中，您希望 f x（其结果）与 x（zero 的结果）具有相同类型。但你也没有得到。签名是最简单的方法，但如果签名失败，请使用 asTypeOf.

在 succ 的等式中，您希望其结果与 f x 的类型相同，与 x.

的类型相同

Can you also show me how to derive its type manually?

好的，让我们使用 asTypeOf 来实现上述目标。然后你可以使用 :t 来查找类型 ...

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

（根据@LambdaFairy，我使用了 succ 的正确定义。）

请注意，在无类型的 lambda 演算中，教会数字被框起来了——这就是维基百科所显示的内容。当你接触到更多关于它们的奇异函数（比如加法或前置函数）时，你会发现 Haskell 是一个类型化的 lambda 演算，而 GHC 将 barf/you 会遇到可怕的单态性限制。那asTypeOf帮不了你；你必须求助于（更高级别的）类型签名。

Answer 2

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

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

"succ(zero)" 的类型不同于 GHC 中 "one" 的类型

Type of "succ(zero)" differs from type of "one" in GHC

haskell

types

type-inference

lambda-calculus