crush 演算子について

Hutton2 本 ¹ の第 14 章の補遺で Calculate Polytypically! ² という論文が紹介されていて，これを読んだので雑に解説を書きます．（まあまあ知られてる論文だと思うんですが，他に日本語で言及してる人があんまりいないので．）

例たち

論文中で一貫して登場し続ける例たちがあるので，最初にまとめて載せておきます．データ構造は以下の 4 つ．

data Maybe a = None | One a
data List a = Nil | Cons a (List a)
data BinTree a = Tip a | Join (BinTree a) (BinTree a)
data RoseTree a = Fork a (List (RoseTree a))

データ構造を扱う関数は，ノードが Int のデータ構造に対してその総和を計算する sum*** 族と，ノードが相等性を判定できる型のデータ構造に対して，ある元が含まれているかどうかを判定する elem*** 族の 2 つ．

-- 各種 sum
sumMaybe :: Maybe Int -> Int
sumMaybe None = 0
sumMaybe (One n) = n

sumList :: List Int -> Int
sumList Nil = 0
sumList (Cons n l) = n + sumList l

sumBinTree :: BinTree Int -> Int
sumBinTree (Tip n) = n
sumBinTree (Join lt rt) = sumBinTree lt + sumBinTree rt

sumRoseTree :: RoseTree Int -> Int
sumRoseTree (Fork n l) = n + sumListRoseTree l
  where
  sumListRoseTree Nil = 0
  sumListRoseTree (Cons (Fork n l1) l2) = n + sumListRoseTree l1 + sumListRoseTree l2

-- 各種 elem
elemMaybe :: Eq a => a -> Maybe a -> Bool
elemMaybe e None = False
elemMaybe e (One x) = e == x

elemList :: Eq a => a -> List a -> Bool
elemList e Nil = False
elemList e (Cons x l) = e == x || elemList e l

elemBinTree :: Eq a => a -> BinTree a -> Bool
elemBinTree e (Tip x) = e == x
elemBinTree e (Join lt rt) = elemBinTree e lt || elemBinTree e rt

elemRoseTree :: Eq a => a -> RoseTree a -> Bool
elemRoseTree e (Fork x l) = e == x || elemListRoseTree e l
  where
  elemListRoseTree e Nil = False
  elemListRoseTree e (Cons (Fork x l1) l2) = e == x || elemListRoseTree e l1 || elemListRoseTree e l2

全部似たようなことしかしてないのに型が異なるから別々に定義しなくちゃいけなくて，冗長でめんどいですね．これを全部まとめたいというのが元論文の目的です．

前提知識: catamorphism

元論文を読むための前提知識として，有限の再帰的データ構造は自己関手の最小不動点だとか始代数だとかいう話があります．この記事 にもいい感じに書いてあります．知ってる人は飛ばしてください．
とりあえずなんか自己関手 $F$ ³ があるとします．このとき $\varphi: F(A) \rightarrow A$ のようなかたちの射を $F$ 代数といいます．

type Algebra f a = f a -> a

$F$ 代数 $\varphi: F(A) \rightarrow A$ と $\psi: F(B) \rightarrow B$ に対して，

\require{AMScd}
\begin{CD}
F(A) @>\varphi>> A \\
@VVF(f)V @VVfV \\
F(B) @>\psi>> B \\
\end{CD}

が可換になるような $f: A \rightarrow B$ を $\varphi$ から $\psi$ への $F$ 準同型といいます．
ここで $F$ 代数を対象，$F$ 準同型を射とすると，$F$ 代数の圏 ⁴ を考えることができます．この始対象を $F$ 始代数といいます．要するに $mu: F(I) \rightarrow I$ が $F$ 始代数であるとは，任意の $F$ 代数 $\varphi: F(A) \rightarrow A$ に対し，

\begin{CD}
F(I) @>mu>> I \\
@VVF(f)V @VVfV \\
F(A) @>\varphi>> A \\
\end{CD}

が可換になるような $f: I \rightarrow A$ が一意に存在するということです．
$F$ 始代数は存在すれば同型を除いて一意なので，これを $mu_F: F(\mu F) \rightarrow \mu F$ と書き，$\varphi$ に対して一意に定まる射を $cata(\varphi): \mu F \rightarrow A$ と書くことにします．
始代数に関する結果として，$mu_F$ によって $F(\mu F) \simeq \mu F$ が成り立つという Lambek の定理 があります．これによると $mu_F$ の逆射があるので，これを $unMu_F$ と名付けます．

\begin{CD}
F(\mu F) @>mu_F>> \mu F \\
@VVF(cata(\varphi))V @Vcata(\varphi)VV \\
F(A) @>\varphi>> A \\
\end{CD}

左側を回って辿ることを考えれば，$cata$ が Haskell 上で以下のようにして定義できます．

newtype Mu f = Mu { unMu :: f (Mu f) }

cata :: Functor f => Algebra f a -> Mu f -> a
cata phi = phi . fmap (cata phi) . unMu

これが有限の再帰的データ構造と何の関係があるのか説明していませんでした．さっきの List の定義をみると，data List a = Nil | Cons a (List a) と自分自身を参照しています．これは x についての方程式 x = Nil | Cons a x の解が List a だということを言ってるので，data ListF a x = Nil | Cons a x などと書くと，ListF a の不動点が x = List a だということになります．特に有限リスト全体は「ListF a を有限回適用して構成できるもの全体」=「ListF a の最小不動点」です．
data ListF a x = Nil | Cons a x を x についての関手にできることは明らかなので，ListF a 始代数を考えることができます．これは ListF a の最小不動点とみなすことができます（これが記号 $\mu F$ を用いた理由でもあります）．Lambek の定理より ListF a の不動点みたくなっていて，「始」が最小っぽさを表しているというイメージです．
これをもとに Mu を用いてデータ構造たちを定義してみると，こんな感じになります．

data MaybeF a = None | Some a deriving (Functor)
type Maybe_ a = MaybeF a

data ListF a x = Nil | Cons a x deriving (Functor)
type List a = Mu (ListF a)

data BinTreeF a x = Tip a | Join x x deriving (Functor)
type BinTree a = Mu (BinTreeF a)

data RoseTreeF a x = Fork a (List x)
type RoseTree a = Mu (RoseTreeF a)

たとえば List Int の値は Mu Nil とか Mu (Cons 4 (Mu (Cons 7 Nil))) みたいな形になっています．

こんな感じで有限の再帰的データ構造を $F$ 始代数として表したとき，$F$ はデータ構造を一段階展開するような役割になっています．cata の型をみると (f a -> a) -> Mu f -> a なので，これは「部分構造について既に計算済みになっているデータを一段階ぶん畳み込む処理 :: f a -> a」を与えると，これを帰納的に適用して全部畳み込んでくれる関数 Mu f -> a を作ってくれるということで，まあそれはそう感のある話ですね．ということで例の関数たちは cata を用いると

sumMaybe :: Maybe_ Int -> Int
sumMaybe None = 0
sumMaybe (Some n) = n

elemMaybe :: Eq a => a -> (MaybeF a) -> Bool
elemMaybe e None = False
elemMaybe e (Some x) = e == x

sumList :: List Int -> Int
sumList = cata phi
  where
  phi Nil = 0
  phi (Cons m n) = m + n

elemList :: Eq a => a -> List a -> Bool
elemList e = cata phi
  where
  phi Nil = False
  phi (Cons x b) = e == x || b

sumBinTree :: BinTree Int -> Int
sumBinTree = cata phi
  where
  phi (Tip n) = n
  phi (Join m n) = m + n

elemBinTree :: Eq a => a -> BinTree a -> Bool
elemBinTree e = cata phi
  where
  phi (Tip x) = e == x
  phi (Join lb rb) = lb || rb

sumRoseTree :: RoseTree Int -> Int
sumRoseTree = cata phi
  where
  phi (Fork m l) = m + sumList l

anyList :: (a -> Bool) -> List a -> Bool
anyList p = cata phi
  where
  phi Nil = False
  phi (Cons x b) = p x || b

elemRoseTree :: Eq a => a -> RoseTree a -> Bool
elemRoseTree e = cata phi
  where
  phi (Fork x l) = e == x || anyList id l

となります．一段階ぶん畳み込む処理を phi に書いて，cata phi ってやるとなんかできるという感じが伝わると思います．
これでデータ構造の再帰的になっている部分を統一的に扱えるようになりましたが，まだ一般化には程遠いです．ListF a x が実は a についても関手にできる（つまり Bifunctor ⁵ ）という事実と，代数的データ型の直和のところでは場合分け，直積のところでは二項演算の適用をしているだけだという共通点が，一般化への鍵になります．次節より論文の内容に入ります．

τ 演算子

ここからしばらく記号の準備が続きます．パラメータ多相（ジェネリクス）のある言語を使われる方はご存知でしょうが，List a って a について関手になっていて欲しいですよね．つまり Mu (ListF a) を a についての関手にしたいということで，このときに ListF が第一引数についても関手になること（すなわち Bifunctor であること）を使います．より一般には， $n$ 引数関手 $F$ について，$n - 1$ 引数関手 $\tau F$ が以下のようにして定義できます．

\tau F \ a_1 \dots a_{n - 1} = \mu(F \ a_1 \dots a_{n - 1}) \\
\tau F \ f_1 \dots f_{n - 1} = cata(mu_{F \ b_1 \dots b_{n - 1}} \circ \ F \ f_1 \dots f_{n - 1} \ id_{\mu (F \ b_1 \dots b_{n - 1})})

定義における始域や終域が整合していることを確認してください．ここではカリー化による部分適用っぽい記法を用いていて，$n$ 引数の $F$ に $n - 1$ 個の引数を部分適用すると $1$ 引数関手が残るので，$\mu$ 作用素が使えるみたいな感じになってます．$2$ 変数関手に対するものに限りますが，$\tau$ 演算子を Haskell で実装してみるとこんな感じです．

newtype WrappedBifunctor f a b = Wrap { unwrap :: f a b }
instance Bifunctor f => Functor (WrappedBifunctor f a) where
  fmap f (Wrap a) = Wrap (second f a)

newtype Tau f a = Tau { unTau :: Mu (WrappedBifunctor f a) }

instance Bifunctor f => Functor (Tau f) where
  fmap g = Tau . (cata (Mu . Wrap . first g . unwrap)) . unTau

Bifunctor f に対して Tau f が Functor であるということを宣言しています．ここで first を使っている点が重要です．また，Bifunctor に $1$ つだけ引数を適用したものが Functor になるということを利用したいのですが，型クラスに適合させるためにはコンストラクタが必要 ⁶ なので，WrappedBifunctor というものを定義しています．

Regular functor

一般の関手についてだと掴みどころがなさすぎですが，例たちを含むデータ構造を定義するのに用いられるような関手は，多項式関手 ⁷ に $\tau$ 演算子を加えたものと，それらの組み合わせによって構成されるような比較的単純なものに限ります．論文ではこの関手のクラスを regular functor と呼んでいて，$n$ 引数の regular functor の全体は以下の BNF ⁸ で定義されています:

\begin{align}
F^{(n)} ::= & \\
& | \ 1^K \\
& | \ Ex^n_i \\
& | \ + \ (\text{only if $n = 2$}) \\
& | \ * \ (\text{only if $n = 2$}) \\
& | \ F^{(k)} \circ F_1^{(n)} \dots F_k^{(n)} \\
& | \ \tau F^{(n + 1)} \\
\end{align}

上から順に説明すると，$1^K$ は常に終対象 ⁹ $1$ を返す $n$ 引数の定数関手，$Ex^n_i$ は $i$ 番目の引数をそのまま返す $n$ 引数の射影関手，$+$ と $*$ は $2$ 引数関手とみなした直和と直積です．$F^{(k)} \circ F_1^{(n)} \dots F_k^{(n)}$ は $k$ 引数 regular functor $F^{(k)}$ と $k$ 個の $n$ 引数 regular functor $F_1^{(n)} \dots F_k^{(n)}$ の合成で，

(F^{(k)} \circ F_1^{(n)} \dots F_k^{(n)}) \ a_1 \dots a_n = F^{(k)} \ (F_1^{(n)} \ a_1 \dots a_n) \dots (F_k^{(n)} \ a_1 \dots a_n) \\
(F^{(k)} \circ F_1^{(n)} \dots F_k^{(n)}) \ f_1 \dots f_n = F^{(k)} \ (F_1^{(n)} \ f_1 \dots f_n) \dots (F_k^{(n)} \ f_1 \dots f_n)

の規則で関手になっているものです．最後の $\tau F^{(n + 1)}$ はさっきの $\tau$ 演算子で $n + 1$ 引数 regular functor を $n$ 引数にしたもの．この BNF に従うと，例のデータ構造たちは

Maybe = + \circ 1^K \ Ex^1_1 \\
List = \tau(+ \circ 1^K \ (* \circ Ex^2_1 \ Ex^2_2)) \\
BinTree = \tau(+ \circ Ex^2_1 \ (* \circ Ex^2_2 \ Ex^2_2)) \\
RoseTree = \tau(* \circ Ex^2_1 \ (List \circ Ex^2_2)) = \tau(* \circ Ex^2_1 \ ((\tau(+ \circ 1^K \ (* \circ Ex^2_1 \ Ex^2_2))) \circ Ex^2_2))

というふうになります．

crush 演算子

ここまでが準備で，本節からやっと本題です．$n$ 引数 regular functor $F$ に対し，$crush: F \ \underbrace{a \dots a}_n \rightarrow a$ のような型をもつ $crush$ を， $F$ の構成について帰納的に定義します．これは，全てのプリミティブ型が $a$ であるようなデータ構造 $F \ a \dots a$ を畳み込んで $a$ 型の値を得るような関数の定義を，$F$ の構造から自動的に導出できるということです．
また，$a$ には一定の付加構造が要求されます．論文では，$crush$ を定義する過程で必要なものを順次付け加えていくという形式で書かれていますが，これは結論から言えば二項演算 $\oplus: a \times a \rightarrow a$ とその単位元 $\nu \in a$ です．
以下，BNF の各ケースごとに定義を考えていきます．

終対象の定数関手のケース

$1^K \ a \dots a = 1$ なので定義すべきは $crush: 1 \rightarrow a$ ですが，これは $a$ の元を一つ選べばよいだけです．従ってここでは $\nu$ を選びます．
$1$ は $0$ 個の直積と考えることもできますが，$\oplus$ の単位元 $\nu$ を選んでおけば，後の直積のケースとも整合します．

射影関手のケース

$Ex^n_i \ a \dots a = a$ なので定義すべきは $crush: a \rightarrow a$ で，$id_a$ とすればよいです．

直和のケース

定義すべきは $crush: a + a \rightarrow a$ ですが，直和のそれぞれのケースに対して値をそのまま返せばよいです．

直積のケース

定義すべきは $crush: a * a \rightarrow a$ ですが，これには $\oplus$ を用いればよいです．

合成のケース

$(F^{(k)} \circ F_1^{(n)} \dots F_k^{(n)}) \ a \dots a = F^{(k)} \ (F_1^{(n)} \ a \dots a) \dots (F_k^{(n)} \ a \dots a)$ なので，定義すべきは $crush: F^{(k)} \ (F_1^{(n)} \ a \dots a) \dots (F_k^{(n)} \ a \dots a) \rightarrow a$ です．
また，構造帰納法の仮定より $c: F^{(k)} \ \underbrace{a \dots a}_k \rightarrow a$ と $c_i: F_i^{(n)} \ \underbrace{a \dots a}_n \rightarrow a$ の型をもつ各 crush 関数を利用できます．
これらを組み合わせると，$crush = c \circ (F^{(k)} \ c_1 \dots c_k)$ とすればよいことがわかります．

τ 演算子のケース

$(\tau F^{(n + 1)}) \ \underbrace{a \dots a}_n = \mu(F^{(n + 1)} \ \underbrace{a \dots a}_n)$ なので，定義すべきは $crush: \mu (F^{(n + 1)} \ \underbrace{a \dots a}_n) \rightarrow a$ です．
また，構造帰納法の仮定より $c: F^{(n + 1)} \ \underbrace{a \dots a}_{n + 1} \rightarrow a$ の型をもつ crush 関数を利用できます．
これより，$crush = cata(c)$ とすればよいことがわかります．

以上により $crush$ が定まりました．これは $a$ の二項演算と単位元のとり方に依るので，これを付け加えて $crush \ (\oplus) \ \nu$ と書くことにします．　

マイナーチェンジ

この時点で既に，任意の regular functor $F$ に対して $sum: F \ Int \dots Int \rightarrow Int$ の型をもつ $sum$ 関数が $sum = crush \ (+) \ 0$ と表せたりと，かなり強力な感じがします．さらに様々な例を統一的に扱うために，$crush$ の変種をいくつか定義します．

crushf

まずは $f: b \rightarrow a$ を追加で受け取って，各プリミティブ値に $f$ による前処理を一斉に行ってくれる $crushf: F \ b \dots b \rightarrow a$ です．これは $F$ の関手性を利用すれば簡単に定義できて，$crushf \ (\oplus) \ \nu \ f = (crush \ (\oplus) \ \nu) \circ (F \ f \dots f)$ となります．

crushM

$\oplus$ の単位元を見つけるのが手間だとか，単位元がないだとかいうことがあります．そこで $\oplus_M: Maybe \ a \times Maybe \ a \rightarrow Maybe \ a$ なる二項演算を，

one \ u \oplus_M one \ v = one \ (u \oplus v) \\
one \ u \oplus_M none = one \ u \\
none \oplus_M one \ v = one \ v \\
none \oplus_M none = none

で定めると，$\oplus$ から $none$ を単位元とする二項演算が作れます ¹⁰．これを用いて，$crushM: F \ a \dots a \rightarrow Maybe \ a$ が $crushM \ (\oplus) = crushf \ (\oplus_M) \ none \ one$ と定義できます．

crushMf

最後に，$crushf$ と $crushM$ を組み合わせた $crushMf: F \ b \dots b \rightarrow Maybe \ a$ です．定義は簡単で， $crushMf \ (\oplus) \ f = crushf \ (\oplus_M) \ none \ (one \circ f)$ です．

crush 演算子の利用例

論文に載ってる例を列挙します．まずは特に説明の要らなさそうなものたちから．

$sum: F \ Int \dots Int \rightarrow Int$
$sum = crush \ (+) \ 0$

$size: F \ a \dots a \rightarrow Int$
$size = crushf \ (+) \ 0 \ (const \ 1)$

$elem: a \rightarrow F \ a \dots a \rightarrow Bool$
$elem \ e = crushf \ (\vee) \ False \ (== e)$

$flatten: F \ a \dots a \rightarrow [a]$
$flatten = crushf \ (++) \ [] \ singleton$

ここで $singleton: a \rightarrow [a]$ は $singleton \ x = [x]$ です．
変種の $crushM$ は空のデータ構造に対して割り当てるべきふさわしい値がなさげな場合に役立ちます．例えば，

$first: F \ a \dots a \rightarrow Maybe \ a$
$first = crushM \ (\ll)$

が有用そうな例です．ここで $(\ll)$ は $u \ll v = u$ で定まる二項演算です．
ここまでの例に登場した二項演算は全て結合律を満たすものでしたが，$crush$ の定義には結合律は含まれていません．結合律を満たさない二項演算を用いたものにも有意義な例があります．たとえば $m \odot n = max (m, n) + 1$ とすると，データ構造の深さを計算する関数が

$depth: F \ a \dots a \rightarrow Maybe \ Int$
$depth = crushMf \ (\odot) \ (const \ 0)$

で定義できます．
最後の例はデータ構造の形を保ったまま二分木に変換する関数

$binned: F \ a \dots a \rightarrow Maybe \ (BinTree \ a)$
$binned = crushMf \ join \ tip$

です．

で，これ Haskell で実装できんの？

結論から言うと，かなり怪しいです．そもそも，関手の型に引数の個数の情報を持たせなきゃいけないとすると，依存型が必要になります．GHC 拡張を使ってなんかやっていけるのかもしれませんが，Haskell 初心者なのでよくわからん．論文の例たちは Bifunctor まで扱えれば十分で，$\tau$ 演算子を使って最終的には $1$ 引数関手になるというやつしかないし，実際のユースケースもそんなもんだろということで，実装してみた やつを貼っておきます．最終的には

sum_ :: CrushableFunctor f => f Int -> Int
sum_ = crush (+) 0

size :: CrushableFunctor f => f a -> Int
size = crushf (+) 0 (const 1)

elem_ :: (CrushableFunctor f, Eq a) => a -> f a -> Bool
elem_ e = crushf (||) False (== e)

flatten :: CrushableFunctor f => f a -> [a]
flatten = crushf (++) [] (\x -> [x])

first_ :: CrushableFunctor f => f a -> Maybe a
first_ = crushM const

depth :: CrushableFunctor f => f a -> Maybe Int
depth = crushMf (\m n -> (max m n) + 1) (const 0)

binned :: CrushableFunctor f => f a -> Maybe (BinTreeF a)
binned = crushMf join tip

とトゥルーエンド感ある感じになっている．

まとめ

Haskell 書く人は「なんだ，要するに Foldable の話じゃん」とお気づきかと思います．たぶんそうで，データ構造の定義をみて Foldable のインスタンスを自動導出するみたいな感じの話をしてるんだと思います．Foldable より明確に強い点は $n$ 引数関手まで扱える点ですが，結局そこまであんまり実装できてないのでこの記事意味ないんじゃね！？

1. Programming in Haskell 2nd Edition ↩

2. Calculate Polytypically! ↩

3. どんな圏の自己関手かという話になりますが，今回の議論にはあんま関係ないので忘れてください．一応 Haskell の型と関数がなす圏 $\mathbf{Hask}$ が該当するのかなって感じなんですが，実は $\mathbf{Hask}$ って圏じゃない らしい．じゃあこの議論なんの意味があるのかって？俺が知りてーよ． ↩

4. コンマ圏 みたいな話． ↩

5. 2 引数関手 Bifunctor についての数学的な定義は nlab, Haskell の型クラスは Hackage, 解説記事 を参照． ↩

6. haskell-jp にお世話になりました． ↩

7. 定数関手，恒等関手，直和，直積で構成される関手くらいの意味． ↩

8. Backus–Naur form ↩

9. 終対象の数学的な定義は nlab を参照．大体は一点集合のようなものがこれに該当し，$\mathbf{Hask}$ においては Unit 型のこと． ↩

10. いわゆる単位元の添加というやつ． ↩