日々の流転

λ. 最小不動点と最大不動点

A Categorical Programming Lanuage の論文では

left object nat with pr is
  zero: 1 -> nat
  succ: nat -> nat
end object

に対応するright objectとして

right object conat with copr is
  pred: conat -> coprod(1,conat)
end object

を定義していた。ここでnatは NatF(X)=1+X の最小不動点に、 conatはNatFの最大不動点になってる。 対称性は、natの定義を以下のようにcoprodを用いたものに書き換えると 明らかでしょう。

left object nat with pr is
  α: coprod(1,nat) -> nat
end object

論文には(何故か)取りあげられていないのですが、 さらに同様にして、

left object list(X) with prl is
  nil:  1 -> list
  cons: prod(X,list) -> list
end object

に対応するright objectとして

right object colist(X) with coprl is
  α: colist -> coprod(1,prod(X,colist))
end object

が定義できるはずだ(しかし、natural transformation αの良い名前が思いつかなひ)。 listが有限のリストを、inflistが無限のリストを表わしているのに対して、 こいつは有限と無限の両方のリストを表わすはず。 listとinflistからの埋め込みはそれぞれ

• list2colist = coprl(prl(in1, in2.prod(I, case(nil, cons))))
• inflist2colist = coprl(in2.pair(head,tail))

となる。

λ. Haskellとの関係

ところで、Haskellのリストがlist,inflist,colistのどれに対応するかを考えると、Haskellのリストは有限のリストも無限のリストも共に表わすことが出来るので、明らかにcolistに対応するはず。

代数的データ型の意味はfunctorの最小不動点として与えられるとよく言われるが、Haskell等のlazyな言語ではそのlazynessのために最大不動点になっているように思える。