为什么类型签名看起来像这样？(将教会号码转换为Int)

Question

我正在学习Haskell并尝试编写一个将Church编号转换为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

我有正确的c2i使用类型签名:t c2i

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

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

Answer 1

如果您a在c2i签名中使用,则必须使用任何 签名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由调用者选择,而不是由调用者选择.调用者必须传递一个必须具有多态类型的参数:即,它必须传递一个Church afor all a,而不仅仅是a Church String.

或者,甚至可以宣布

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

并且仅传递多态值.