简化 Haskell 类型签名

Question

我的问题是如何通过分析Haskell类型签名来处理它。为了具体说明，我正在看“fix”函数：

fix :: (a -> a) -> a

我写了一个小的虚构函数来执行类似于 Peano 的加法:

add = \rec a b -> if a == 0 then b else rec (a-1) (b+1)

当我检查类型时，我得到了我期望的fix add类型。

fix add :: Integer -> Integer -> Integer

看起来它的执行结果和我预期的一样：

> (fix add) 1 1
2

我该如何使用 fix 和 add 的类型签名来展示 fix add 具有上述签名？在处理类型签名时，有哪些“代数”的规则可以遵循？我应该如何“展示我的工作”？

- Chris

Answer 1

ghci告诉我们：

add :: Num a => (a -> a -> a) -> a -> a -> a

由于add的第二个参数需要一个Eq实例（您正在检查它是否等于0），因此存在一些类型类的噪声。

当我们将fix应用于add时，fix的签名变为：

fix :: ((a -> a -> a) -> (a -> a -> a)) -> (a -> a -> a)

请记住，《code>fix :: (a -> a) -> a中的a可以具有任何类型。在这种情况下，它们的类型为(a -> a -> a)

因此，fix add :: Num a => a -> a -> a，这恰好是添加两个a所需的正确类型。

您可以以非常代数的方式处理Haskell的类型签名，变量替换的效果就像您期望的那样。实际上，类型和代数之间存在直接的翻译。

- cdk

---

谢谢！我已经弄清楚了（fix中的a必须是(a -> a -> a)）。但是还缺少一步吗？在((a -> a -> a) -> (a -> a -> a)) -> (a -> a -> a)和a -> a -> a之间是否有一些中间步骤？ - Chris

是的，您正在将 fix 部分应用于 add。生成的部分应用函数的类型为 a -> a -> a。 - cdk

将 fix 应用于 add，会从 fix 的类型中移除 ((a -> a -> a) -> (a -> a -> a)) 参数。 - Gabriella Gonzalez

@GabrielGonzalez 谢谢，我想那就可以了。我现在知道它是如何工作的了。感谢大家。 - Chris