- 功能应用程序是左结合:
a b c
解析作为(a b) c
- 函数定义对于lambda表达式语法糖:
f x y = ...
装置f = \x y -> ...
- lambda表达式使用多个参数自动咖喱:
\x y -> ...
装置\x -> (\y -> ...)
因此
f g x = g (g x) x
意味着
f = \g -> (\x -> (g (g x)) x)
现在,让我们试着得出的f
类型。让我们给它一个名字:
f :: ta
但究竟什么是ta
? f
被定义为的λ,所以它的类型涉及->
(它是一个函数):
\g -> (\x -> (g (g x)) x) :: tb -> tc
g :: tb
\x -> (g (g x)) x :: tc
即对于某些类型tb
和tc
,并且g
(参数)的类型是tb
,并且结果(函数体)的类型是tc
,\g -> ...
的类型是tb -> tc
。
而且因为整个事情是必然f
,我们有
ta = tb -> tc
我们不tc
做,虽然:
\x -> (g (g x)) x :: td -> te
x :: td
(g (g x)) x :: te
与
tc = td -> te
功能正文(其类型我们称为te
)由一个应用程序组成(必须是)变量x
的函数。由此可以得出:
g (g x) :: td -> te
因为
x :: td
(g (g x)) x :: te
再次向下钻取,我们有
g :: tf -> (td -> te)
g x :: tf
因为应用g
到g x
必须有类型td -> te
。最后,
g :: td -> tf
因为
x :: td
g x :: tf
现在我们有g
两个等式:
g :: tf -> (td -> te)
g :: td -> tf
因此
tf = td
td -> te = tf
tf -> te = tf
在这里,我们碰到一个问题:tf
定义在之中ms本身,给出类似于
tf = (((((... -> te) -> te) -> te) -> te) -> te) -> te
即无限大的类型。这是不允许的,这就是为什么f
没有有效的类型。
我无法理解所问的问题。你能否准确地向我们提出与工作表中出现的问题一样的问题?我可以说'g(g x)'将'g'应用于'x'的结果是'g'。如果你对使用括号的应用程序的语言更熟悉,那么这些语言就是'g(g(x))'。 –
@ReinHenrichs问题如下:“解释为什么下面定义的函数f没有类型: f g x = g(g x)x” 我有点好奇你怎么能解决这个问题?一旦我们评估g(g x),将g应用于g x的结果,我们将如何处理x(g(g x)x? – CowNorris
啊,我错过了最后的'x'并且感到困惑,因为'f g x = g(g x)'显然是一个类型。 –