- 功能應用程序是左結合:
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)'顯然是一個類型。 –