haskell - 为什么类型签名看起来像这样？ (将教堂编号转换为 Int)

Question

我正在学习 Haskell 并尝试编写一个将教会数字转换为 Int 的函数。仅当我不编写类型签名时，我的代码才有效。

type Church a = (a -> a) -> a -> a

zero :: Church a
zero s z = z

c2i :: Church a -> Int   -- This line fails
c2i x = x (+1) 0

我使用 :t c2i 获得了 c2i 的正确类型签名

c2i :: (Num a1, Num a) => ((a -> a) -> a1 -> t) -> t

但我想知道为什么会这样？

Answer 1

如果您在 c2i 签名中使用 a，则它必须与 any a 一起使用。换句话说，a 由函数的调用者 选择。具体来说，它必须与

c2i :: Church String -> Int
-- that is
c2i :: ((String -> String) -> String -> String) -> Int

由于代码在a = String时不起作用，多态类型无效。

如果您不添加类型，编译器能够推断出某种类型，从而使代码正常工作。一个更简单的类型可能是:

c2i :: Church Int -> Int

或者，在启用一些扩展之后，

c2i :: (forall a. Church a) -> Int

在后一种情况下，我们指定 a 由 c2i 选择，而不是由调用者选择。相反，调用者必须传递一个必须具有多态类型的参数:即，它必须为所有 a 传递一个 Church a，而不仅仅是一个 Church String 。

或者，甚至可以声明

type Church = forall a . (a->a)->a->a

并仅传递多态值。