日々の流転

λ. Do you know that the S combinator is injective?

たまたま見たShin-Cheng Mu氏のページに「Do you know that the S combinator is injective?」と書いてあった。 「へー、そうなのか」と思い暗算で確認してみたが、どうせなのでagdaでも示してみる。

s (A,B,C::Set) :: (A->B->C) -> (A->B) -> (A->C)
s f g a =  f a (g a)

z (A,B,C::Set) :: ((A->B) -> (A->C)) -> (A->B->C)
z h a b = h (\(x::A) -> b) a

prop (A,B,C::Set) (!f::A->B->C) :: Id (z (s f)) f
prop = refId f

どうでも良いが、zの型は一種の functional completeness っぽい感じ?