(flip id) -- その２

(flip id) の解釈の仕方がよく分からないので、とりあえず自分なりに考えてみました。

flipとidの定義が、こんな感じだとします。

　　flip :: (a -> b -> c) -> b -> a -> c
　　flip f = \b -> \a -> f a b

　　id :: a -> a
　　id = \a -> a

(flip id)を簡約すると、次のようになると考えられます。

　　flip id = (\f -> \b -> \a -> f a b) id
　　flip id = \b -> \a -> id a b
　　flip id = \b -> \a -> (id a) b
　　flip id = \b -> \a -> a b            -- (1)

次に、(flip id)の型を考えます。flipの第１引数を省略すると、(2)式のようになります。

　　flip :: (a -> b -> c) -> b -> a -> c
　　flip id :: b -> a -> c               -- (2)

ここで、(1)式の末尾の項(a b) は、(2)式の末尾の項cに対応しますから、その型はcになります。ここから、型変数aの型を(4)式のように推論することができます。さらに、(4)式を(2)式にあてはめると、(5)式を得ることができます。

　　(a b) :: c                           -- (3)
　　a :: b -> c                          -- (4)
　　flip id :: b -> (b -> c) -> c        -- (5)

ちょっと考えると、flipの第１引数の型は(a -> b -> c)と宣言されていますから、id :: a -> a を第１引数にしてよいのか、というころが気になります。しかし、この結果はGHCiの結果とマッチします(マッチするように考えましたから)。ということで、むりやり納得することにしました。もう少し詳しく、型推論の動作を知りたいところです。