日々の流転

λ. Constructing M-types from W-types

Containers: constructing strictly positive types の話。

先日、「W-typesによる帰納的データ型の表現」で書いたように、W-typesは整礎(wellfounded)な木のデータ型になっている。 そして、Wa:A. B(a) は関手 T(X) = Σa:A. B(a)→X の最小不動点になっている。 最小不動点があれば当然最大不動点も考えたくなるもので、それがM-types。 Ma:A. B(a) は T の最大不動点で、整礎とは限らない木のデータ型になっている。 ちなみに、名前はM-typesはW-typesの双対だから「W」を上下反転した「M」を使ったのだろうと思う*1。

で、M-typesはW-typesとは別に追加しなくてはいけないかと思ったら、実はMartin-Löf圏ではW-typesから構成することが出来るそうだ。 無限木を深さnで切ってそこをダミーの値に置き換えると有限の木になり、逆にnを大きくしていった時のそのような有限の木の極限が元の無限木と考えることが出来る。なので、元の無限木を直接扱う代わりに、そのような有限の木の族として扱う。有限の木はW-typesで表現出来るので、M-typesはW-typesで表現できると。

イデアル完備化との関係?

こういう話を聞いて連想するのは、Jiří Adámek の Final Coalgebras are Ideal Completions of Initial Algebras で……

後で書く。

Agdaによる実装

M-types.agda (作業中)

後で書く。