为什么类型签名看起来像这样？（将教堂编号转换为 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 是由函数的 caller 选择的。具体来说，它必须与

一起使用

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

并仅传递多态值。

Why does the type signature look like this? (Converting Church number to Int)