“succ（零）”的类型与GHC中的“一”类型不同

Question

要求GHC打印“one”和“succ zero”的类型（lambda calculus编码数字的方式），我得到两种不同的类型！它们不应该是一样的吗？你能告诉我如何手动派生它的类型吗？

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)

“在f的n应用之后再做一次f，从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

Answer 2

首先，您希望zero与one的类型相同。在zero的等式中，你不要在f的rhs上使用->。所以编译器不知道要推断出什么类型。在one的等式中，您希望f x（其结果）与x（zero的结果）相同。但你也没有得到。提供签名最简单，但没有使用asTypeOf。

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

你能告诉我如何手动派生它的类型吗？

好吧，让我们使用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 /你会遇到可怕的单态限制。然后asTypeOf无法帮助你;你必须诉诸类型签名（更高级别）。