日々の流転

λ. Church-Rosser Theorem in Agda2

Haskell Hackathon in 2008 September に参加。やるネタは幾つか考えていたのだけど、結局、昔Agda1で書いたチャーチロッサーの定理の証明をAgda2で書き直すということをやっていた。

(詳しくは後で)

λ. Mの型付け

Mコンビネータ*1 λx. x x は多相型を適当に使うと型付け出来る。 例えばHaskell(GHC)ならば以下の通り。

m :: (forall a. a->a) -> (forall a. a->a)
m x = (x :: (forall a. a->a) -> (forall a. a->a)) x

これが出来るのは 型 forall a. a->a に属する真っ当な要素は id だけだから。

では、同様にすると、Yコンビネータ*2 λf. (λx. f (x x)) (λx. f (x x)) も型付け出来るだろうか?