Just $ A sandbox

プログラミングと計算機科学とかわいさ

ListのT代数の非自明な射は何か?

ListのT代数の非自明な射は何か?という感じの話.

List Monad, T-Algebra

以下のようなmonoid free functorとforgetful functorの随伴がある:
free functorは集合を自由モノイド(wordの集合, 演算は結合)に飛ばし, forgetful functorはモノイドを底集合に飛ばす.

$ F \dashv G : \mathbf{Mon}(FX,Y) \cong \mathbf{Set}(X, GY); h \mapsto h |_X $

ここから標準的に得られるモナドはList Monadに一致する:

$ TC = GFC = | C^* | \cong [C] $
$ \text{unit}_C : C \hookrightarrow TC $
$ \text{join}_C = G \epsilon F C = \text{concat} : T^2 C \to TC$

ListのT代数とは$(C,h : TC \to C)$であって以下の条件を満たすもののこと:

1. $ h \circ \text{join}_C = h \circ T h $
2. $ h \circ \text{unit}_C = 1_C $

あるいは, 元を明示して書くと,

1. `forall xs : [ [a] ]. h (concat xs) = h (fmap h xs)`
2. `forall x : a. h [x] = x`

ともかける.
例としては, `head, last : [a] -> a`や`sum, product : [Int] -> Int`などがそう.

$(C,h), (C', h')$がともにListのT代数のとき, この間のT代数の射$f : (C,h) \to (C',h')$とは, 射$f : C \to C'$であって以下を満たすもののこと:

1. $ f \circ h = h' \circ T f $

T代数の射の手頃で非自明な例は作るのが難しい, というのも型aが一般的だと例えばheadとlastの間には射はないので, 上に挙げた例の間に射をのばそうとしても上手くいかない.
idでない例としては, 例えば`length : ([a], h) --> (Int, h)`などがあるが, これは型が違うとはいえdomとcodに現れている射が同じものなのでほぼidと変わらない.

ListのT代数で非自明な射というのはどういうものがあるだろう?
もしくは他のモナドのT代数の場合だとどうだろう?という疑問.