2022年1月12日 星期三

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

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

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

(.) 的型別是 $(y \to z) \to (x \to y) \to x \to z$,所以我們這樣列

第一個參數 (.): $(b_1 \to c_1) \to (a_1 \to b_1) \to a_1 \to c_1 \tag{1} $
中置的函數 . :   $(y  \to  z)  \to  (x  \to y)  \to x \to z$

第二個參數 (.): $(b_2 \to c_2) \to (a_2 \to b_2) \to a_2 \to c_2 \tag{2} $
中置的函數的第一個參數就是$(y \to z)$, 跟$(1)$式比較之後可得

$y=(b_1 \to c_1)\tag{3}$
$z=(a_1 \to b_1) \to a_1 \to c_1 \tag{3a}$
第二個參數是$(x \to y)$,跟$(2)$式比較之後可得

$x=(b_2 \to c_2) \tag{4a}$
$y=(a_2 \to b_2) \to a_2 \to c_2 \tag{4}$
$(3)$ 和 $(4)$ 式都是 $y$ 的型別,因此比較之後可得

$b_1 = (a_2 \to b_2) \tag{5}$
$c_1 = (a_2 \to c_2)\tag{6}$
接收了兩個參數後,中置函數的回傳型別是$x \to z$。這就是我們想知道的型別,但是要用 $a$ 和 $b$ 表示。由 $(3a)$ 和 $(4a)$ 可得 $x \to z$的型別就是
$$(b_2 \to c_2) \to (a_1 \to b_1) \to a_1 \to c_1$$
代入 $(5)$ 和 $(6)$ 可得
$$(b_2 \to c_2) \to (a_1 \to (a_2 \to b_2)) \to a_1 \to a_2 \to c_2$$
重新命名可以看得更清楚,讓 $a_1 = a, \  a_2 = d, \  b_2 = b, \  c_2=c $
因此$(b \to c) \to (a \to d \to b) \to a \to d \to c$就是(.).(.)的型別 。用數學式的寫法就是$g(f(x, y))$,就這麼簡單。η conversion 做的事就是把 $g, f, x, y$ 全去掉,只保留函數複合的記號,因為這函數的本質就只有函數複合。

沒有留言: