Processing math: 100%

2022年1月12日 星期三

如何做 Haskell 的 η conversion,以 (.).(.)為例

 Haskell的函數直接支援 η(eta) conversion,也就是說函數的撰寫可以變成完全無參數。事實上還是會接收參數,只是經過 η conversion 之後可以不寫。於是就有像 (.).(.) 這種完全不知道在幹什麼的函數。這不是乳房的象形文字,是一個合法的函數,而且還很有用。當然最好別這樣寫,這樣寫沒人看得懂。(.).(.) 函數可以經由 η conversion 轉回來變成有參數,Haskell當中有一種機械化的代數運算方式計算出 (.).(.) 的型別,有了型別就知道它在幹什麼了。

方法就是列出所有函數的型別,然後做型別的代數運算,看傳回的型別是什麼。重點是傳回的型別。(.).(.) 是中置式寫法,第一個參數是函數 (.),這是函數複合。第二個也是 (.),也就是說這是函數複合-複合-函數複合。用講的很像咒語。不過列出型別就更清楚了。

(.) 的型別是 (yz)(xy)xz,所以我們這樣列

第一個參數 (.): (b1c1)(a1b1)a1c1
中置的函數 . :   (yz)(xy)xz

第二個參數 (.): (b2c2)(a2b2)a2c2
中置的函數的第一個參數就是(yz), 跟(1)式比較之後可得

y=(b1c1)
z=(a1b1)a1c1
第二個參數是(xy),跟(2)式比較之後可得

x=(b2c2)
y=(a2b2)a2c2
(3)(4) 式都是 y 的型別,因此比較之後可得

b1=(a2b2)
c1=(a2c2)
接收了兩個參數後,中置函數的回傳型別是xz。這就是我們想知道的型別,但是要用 ab 表示。由 (3a)(4a) 可得 xz的型別就是
(b2c2)(a1b1)a1c1
代入 (5)(6) 可得
(b2c2)(a1(a2b2))a1a2c2
重新命名可以看得更清楚,讓 a1=a, a2=d, b2=b, c2=c
因此(bc)(adb)adc就是(.).(.)的型別 。用數學式的寫法就是g(f(x,y)),就這麼簡單。η conversion 做的事就是把 g,f,x,y 全去掉,只保留函數複合的記號,因為這函數的本質就只有函數複合。

沒有留言: