型付ラムダ計算 - 白のカピバラの逆極限 S.144-3

(f, g) (a, b) = (f a, g b)

となるべきだと書いた。ようするに、圏論の積ですよね。
それを拡張して
http://d.hatena.ne.jp/nuc/20060424/p4
で、データ型を定義するときに、何を食ったときには何、のようなことになっていても問題はない。

3 f = f.f.f

とか。楽しそうではないか。

で、今日問題点に気がついて、それは型が付けられるならば計算が止まるというのが成り立たなくなるところにある気がした。
しかし、haskell でも、どうせ型が拡張されていて整理治していないんだからいいじゃないのと。

それと型がつけられるかということがどうも正則性公理と関わっている気がして、この公理ってないほうが楽しくないかな。