验证lambda表达式的类型

Question

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

我的方法给了我:

我试图在Haskell(在Hugs上)定义它,如下所示:

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

当我打电话给:键入comamnd它给了我:

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

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

Answer 1

请注意,f使用both 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)