验证 lambda 表达式的类型答案

【问题标题】：Verify the type of a lambda expression验证 lambda 表达式的类型
【发布时间】：2014-03-19 03:27:50
【问题描述】：

我需要验证 lambda 表达式的类型：

我的方法给了我：

我试图在 Haskell (on Hugs) 中这样定义它：

h= \f x -> f (f x)

当我调用 :type comamnd 时，它给了我：

(a -> a) -> a -> a

在 Haskell 中是否正确定义了 mi 函数？还是我的方法给出了错误的结果？

【问题讨论】：

标签： haskell lambda-calculus

【解决方案1】：

请注意，f 被调用时同时使用 x 和 f x 作为其参数——这立即意味着 x 的类型和 f x 的类型必须相同[1]。继续这个论点，我们看到由于x 是f 的输入，f x 是f 的输出，所以f 的输入和输出必须相同[2]。

最后，我们检查 lambda 项

\f x -> f (f x)

它有两个输入，f（一个函数）和x，它返回f 的返回类型是[3]。将所有这些信息放在一起，我们有

(a -> b) -> c -> d

where:

  b ~ c        by [1]
  a ~ b        by [2]
  d ~ b        by [3]

因此 Haskell 推断的类型是正确的

h :: (a -> a) -> a -> a
h f x = f (f x)

【讨论】：

还需要注意的是，由于类型的 -> 符号的关联性，这与 (a -> a) -> (a -> a) 相同 - 这可能是 OP 混淆的一部分。

【解决方案2】：

(a -> b) -> (c -> d) 类型等同于 haskells 类型系统中的(a -> b) -> c -> d。您还需要考虑，如果 x 的类型为 a，f x 的类型为 b，那么 f 的类型为 a -> b。所以让y = f x。那么f y === f (f x)的类型是什么？

【讨论】：

【解决方案3】：

你的 Haskell 命令没问题。

您的类型推断不正确。 x 参数的类型应该与f 的输入类型统一，因为你调用f x，那么f 的输入类型应该与f 的输出类型统一，因为你调用@ 987654326@ 上的结果(f x)。

【讨论】：