Haskellと余代数(Coalgebra) - 朝日ネット　技術者ブログ

ここではHaskellの中級者向けのトピックを簡単に取り上げたいと思います。

今回は余代数(Coalgebra)についてです。Haskellを書いていると『余（なんとか）』という言葉をみかけることがあります。これは英語の接頭辞 Co- の訳で、ここでは代数(Algebra)の双対(Dual)という意味で余代数と呼ばれています。

さてHaskellやOCamlのデータ型は一般に代数的データ型(Algebraic data type)と呼ばれます。このデータ型にパターンマッチングを加えて、（オブジェクト指向言語などと比較したときの）関数型言語の特徴と紹介されることも多いと思います。実はこのデータ型にはもともと余データ(Codata)と呼ばれるような相方がいたのですが、人類が扱うには早すぎたのか、データ型に比べると余データは長らく影の存在でありました（ちなみに余データは口語上はコデータと呼ぶかもしれませんが、ここでは文章なので余データと書くことにします。）

データ型と余データ型
余データとオブジェクト指向
システムの抽象化
余帰納法
採用情報

データ型と余データ型

データ型とは、みなさんが普段Haskellで使ってる代数的データ型のことであり、コンストラクタを使ってデータを構成的に作るものです。Haskellの場合はたとえば無限リストが作れてしまいますが、一般的には有限な構成からなるデータを扱います。一方、余データ型とはコンストラクタを無限に適用する構成（より一般的には非整礎(non-wellfounded)な構成）を許すようなデータを扱うものです。すでに述べたようにHaskellでは無限リストがそれに該当しますので、実は余データ型とみなすことができます。Haskellではこのように区別が曖昧なのですが、たとえばAgdaであれば２つは厳格に区別されます。

データ型（代数的データ型）の理論的背景には圏論の代数(Algebra)が関係しています。同様に、余データ型の背景には余代数(Coalgebra)が関係しています。つまりこの２つは理論上では双対な関係にあるということです。圏論において双対というのは、圏の対象はそのままに射の向きだけを逆にした圏のことをいいます。

イメージしやすいように、データと余データの定義を少し比べてみましょう。たとえばリストのデータ型は（GHCのGADTs拡張を使って）以下のように定義できます：

data List a where
  Nil   :: List a
  Cons  :: a -> List a -> List a

さてHaskellには余データのデータ宣言というものは存在しませんが、仮にもしあるとすれば、無限リストを以下のように定義できます：

-- codataのデータ宣言がもしあったら
codata Stream a where
  Head  :: Stream a -> a
  Tail  :: Stream a -> Stream a

上の宣言では無限リストをStreamとして定義しています。この余データ型の宣言の仕方だと要素が有限個のStreamは作れませんが、余データでは無限しか扱えないというわけではありません。宣言方法を変えれば有限リストも無限リストも同時に扱えるようにできますが、今は説明上このようにしておきます。

この２つを見比べると、明らかに異なるのは矢印の向きが逆になっているところです。Listの宣言では、コンストラクタの型をみたとき一番右（つまり戻り値）が必ずListになっており、コンストラクタによってどのようにListの値が構築されるかを定義しているように読むことができます。つまり、

NilはListである
Cons x xsはListである

といった具合です。一方Stream型の宣言では、矢印の向きが逆になっており、たとえばHeadはStream aを受け取ってaを返しているので、これではHeadを使ってStreamを構築することができません。実際、codata宣言で列挙されているものはコンストラクタではなくてむしろデストラクタとしてみることができ、Streamをどのように分解できるかを定義しているように読めます。つまり、

StreamにHeadを適用すると現在の値が得られる
StreamにTailを適用すると次の新しいStreamが得られる

という具合です。だとすると、コンストラクタなしでどのようにしてStreamの値を作るのか？デストラクタだけでは値を構築できないではないか？という疑問がわきます。実は余データの値をもっともエレガントに作成する方法は余パターン(co-pattern)を使うことです（口語ではコパターンと呼ぶかもしれません）。

余パターンとは、代数的データ型のパターンマッチングに対応するような、余データ型に対するパターンマッチングのようなものです。余パターンもHaskellには存在しませんが、もしあったとすれば、これを使って以下のように無限に「１」が続くStream型の値を構築できます：

-- 余パターンの記法がもしあったら
ones :: Stream Int
Head ones  = 1
Tail ones  = ones

一見すると普通の関数定義のような、あるいは何かのパターンマッチングのようにも見えますが、よくよく見るとどちらとも違うことが分かります。もっとも大きな特徴は、余パターンではonesの構成方法に関して何ら言及しておらず、デストラクタを適用したときの振る舞い(Behavior)のみが定義されているという点です。もしonesが通常のデータ型であれば、これをパターンマッチングにかけることでonesの構成方法を見ることができますが、余データ型に対してはそのような覗き見はできません。そもそもonesの宣言の時点で構成方法に関して何も書かれていないのですから、できるはずもありません。

余データとオブジェクト指向

ここまでみると、余データとはなんて不思議なものなんだ、と思うかもしれませんが、実は余データというのは決して机上の空論ではなくて、むしろプログラマーにとってはとても馴染み深い存在なのです。それにはStream型の宣言をオブジェクト指向風のインターフェース宣言のように読んでみてください：

codata Stream a where
  Head  :: Stream a -> a
  Tail  :: Stream a -> Stream a

Streamとは

Headメソッドがあり、呼ぶと現在の値を返す
Tailメソッドがあり、呼ぶと新しいStreamオブジェクトを返す

オブジェクト指向ではメソッドを呼ぶには必ずレシーバーとなるオブジェクトが必要ですから、それがちょうどメソッド（HeadとTail）の最初の引数になっているわけです。

このとき、先ほどみたonesをオブジェクトと見立てて、Streamインターフェースを実装するかのように書くこともできます：

-- もし余パターンをオブジェクト指向風に書けたら
ones :: Stream Int
ones.Head  = 1
ones.Tail  = ones

これはちょうど次のように読めます。 onesオブジェクトは

Headメソッドを呼ぶと1を返す
Tailメソッドを呼ぶとones自身を返す（オブジェクト指向風にいうとthisを返す、みたいな感じですね）

どうでしょうか、なにか不思議な余データでしたが、オブジェクト指向だと思ったらすらすら読めるようになったのではないでしょうか。余データという言葉は聞き馴染みのないものかと思いますが、実際にはプログラマーたちはすでにオブジェクト指向言語で使っていたわけです。つまり関数型言語といのうは代数的データ型をメインにしたプログラミング言語であり、オブジェクト指向言語というのは余データ型をメインとしたプログラミング言語であり、これは偶然ではないのかもしれないと思わせる話です。

オブジェクト指向言語が書ければ実は余データもわかるということですので、別の例でも確認してみましょう。余データを使った二分木は次のように定義できます、

codata BinTree a where
  Node      :: BinTree a -> a
  Children  :: BinTree a -> (BinTree a, BinTree a)

オブジェクト指向風にいうと、BinTreeインターフェースには２つのメソッドがあり、Nodeメソッドを呼ぶと現在の値が返り、Childrenメソッドを呼ぶと左右の子どもの木が返る、という感じです。

さっそくBinTreeを使ってCalkin-Wilf 木を実装してみます。Calkin-Wilf 木とは有理数を重複なくすべて列挙する二分木です。

en.wikipedia.org

cwTree :: BinTree (Int, Int)
cwTree = cwTree' 1 1

cwTree' :: Int -> Int -> BinTree (Int, Int)
(cwTree' a b).Node      = (a, b)
(cwTree' a b).Children  = (cwTree' a (a+b), cwTree' (a+b) b)

このcwTree'オブジェクトには内部状態としてaとbの２つのIntがあります（aは現在の分子、bは現在の分母）。これはオブジェクト指向でいうところの属性(Attribute)にあたるもので、オブジェクト指向と同様にカプセル化されているためNodeメソッドを呼ぶ以外では値を参照する方法はありません（余データはパターンマッチできない！）。

余データが無限を扱う方法は、ちょうどHaskellの無限リストと同じように、無限の値全体を一挙に扱うのではなくて、要求に応じて次の値を生成するような、１ステップずつ処理する形になります。なので多くの場合は余データのデストラクタのいずれかは、型として余データ自身を返します。たとえば上のBinTreeの例でいえばChildrenは戻り値にTree自身を含んでおり、これに対して再帰的にNodeやChildrenを呼ぶことで１ステップずつ値を取得していくという仕組みです。このような再帰処理を通常の再帰(recursion)と対比して区別したいときは余再帰(co-recursion)と呼ぶことがあります。

余データに関数を適用したいときはどのようにすればよいでしょうか。たとえば二分木を無限リストStreamに変換する関数toStream :: BinTree a -> Stream aを考えます。toStreamの戻り値はStream、つまり余データですから、全体としては余パターンの形で実装され、元の木を余再帰的に変換していくことになります：

toStream :: BinTree a -> Stream a
toStream t = toStream' [t]
  where
  toStream' :: [BinTree a] -> Stream a
  (toStream' (t:ts)).Head  = t.Node
  (toStream' (t:ts)).Tail  = let (l,r) = t.Children in toStream' (ts ++ [l, r])

これらのトピックは Codata in Action (2019) [PDF] にまとめられていますので、より詳しく見たい方はそちらを参考にしてみてください。

システムの抽象化

余データはオブジェクト指向でいうところのオブジェクトのようなものだ、というをみてきましたが、実はそれは余データの一面にすぎません。余データにはもっと広い表現力があり、それはシステムを表現しているといわれます。よくプログラムとは入力を受け取り、処理して出力する関数だ、という話がありますが、この例えだとずっと動き続けるプログラム（ないしはプロセス）には当てはまりません。たとえばオペレーティングシステムであったり、Webサーバーであったり、はたまた自動販売機であったり、このようなシステムは余データとしてみることができます。

余データの理論的な話をするときは余代数(Coalgebra)が登場します。余代数はいわゆるシステムを数学的な視点から適切な粒度で抽象化したものといえます。ここでは余代数がどのようにシステムを抽象化するのか簡単に見ていきたいとおもいます。

さて余データをオブジェクトとしてみたとき、余代数ではどのように表現されるのでしょうか。例としてStreamインターフェースは以下のような定義でした：

codata Stream a where
  Head  :: Stream a -> a
  Tail  :: Stream a -> Stream a

砕けた議論ですが、ここでHeadとTailをくっつけて同時に適用するようなメソッドs.Next = (s.Head, s.Tail) を考えたとき、これでStreamのメソッドをNextで置き換えても本質的には変わらないと考えられます：

codata Stream a where
  Next  :: Stream a -> (a, Stream a)

このときStreamは余代数では次のように表わされます：

$S \xrightarrow{\text{Next}} (A \times S)$

ここでSはStreamオブジェクトの内部状態であり、Aは出力の型です。codataの定義と比べると、なんとなく同じ形になっているようにみえます。矢印の先に $S$ 自身が再び現れているのがポイントです。この $S$ に対してNextを呼び続けることで無限に値が取得できるということが表現されています。

同様の話はBinTreeでもみることができます。BinTreeインターフェースの定義はこうでした：

codata BinTree a where
  Node      :: BinTree a -> a
  Children  :: BinTree a -> (BinTree a, BinTree a)

ここでNodeとChildrenをくっつけて同時に適用するメソッドs.NextT = (s.Node, s.Children)としたとき、これ使ってBinTreeの定義を以下のように書き換えても本質的には変わらないと考えられます：

codata BinTree a where
  NextT  :: BinTree a -> (a, (BinTree a, BinTree a))

このときBinTreeは余代数で次のように表されます：

$S \xrightarrow{\text{NextT}} (A \times S \times S)$

もう少しシステムらしい例として、入力と出力がある有限オートマトンであるミーリマシン(Mealy Machine)をみてみます。ミーリマシンは状態遷移図で書くとプログラマーにも馴染み深いものです。ミーリ・マシン - Wikipediaから例を引用します。

f:id:oganet2:20220107164720p:plain — 入力を１クロック遅延させるミーリマシンの状態遷移図

この状態遷移図は、矢印のラベルに {入力}/{出力} の組が書かれており、開始状態は $S_0$ です。この例にあるミーリマシンの処理内容は、入力を１クロック遅延させるもので、たとえば入力{1,0,0,1,1,0,...}を与えると、出力は{0,1,0,0,1,1,0,...}となります（先頭に0がついて、入力全体が１つ後ろにシフトしています）。

ミーリマシンを余代数で表わすと次のようになります。ここでAは入力、Bは出力の型になります。

$S \times A \longrightarrow (B \times S)$

現在の内部状態Sと入力Aが与えられると、出力Bと次の状態Sが得られるということです。説明は省きますがこれは次のように書き直すことができ、

$S \longrightarrow (B \times S)^ A$

そうすると今までみてきたものと同じように $S \rightarrow [ \dots S \dots$ ]の形になります。

さて今度は逆に、この余代数から余データのインターフェース定義を考えてみると、

codata MealyMachine a b where
  Trans  :: MealyMachine a b -> a -> (b, MealyMachine a b)

と書けそうです。あるいはもっとオブジェクト指向風に、出力の取得と状態遷移の操作を分けたいならば、メソッドを２つに分けることもできるでしょう：

codata MealyMachine a b where
  Get        :: MealyMachine a b -> b
  TransOnly  :: MealyMachine a b -> a -> MealyMachine a b

インターフェースが分かったので、実際にこのミーリマシンdelayを余パターンで実装してみましょう。

data S  = S0 | S1 | S2

delay :: S -> MealyMachine Int Int
(delay S0).Trans 0  = (0, delay S2))
(delay S0).Trans 1  = (0, delay S1))
(delay S1).Trans 0  = (1, delay S2))
(delay S1).Trans 1  = (1, delay S1))
(delay S2).Trans 0  = (0, delay S2))
(delay S2).Trans 1  = (0, delay S1))

これらのトピックは Introduction to Coalgebra. Towards Mathematics of States and Observations (2012) [PDF] にまとめられていますので、より詳しく見たい方はそちらを参考にしてみてください。

余帰納法

Haskellのデータ型の背景には代数(Algebra)があり、普段使っている分、こちらのほうが分かりやすいかもしれません。代数は余代数の双対であり、矢印の向きが逆になったものです。たとえばリストの代数は

$1 + (A \times X) \longrightarrow X$

と表されます。これはちょうどHaskellのリストの定義が

data List a = Nil | Cons a (List a)

となっているのに対応しています。Nilを $1$ 、List aを $X$ で置き換えると代数の表現と形が似ています。

このリスト型はコンストラクタのNilとConsのあらゆる組み合わせの値{Nil, Cons a Nil, Cons a (Cons a Nil), Cons a (Cons a (Cons a Nil)), ...}を含んでいるわけですが、このようなものは特別に始代数(Initial Algebra)と呼ばれます。特別な理由のひとつは、始代数には帰納法(Induction)がついてくることです。帰納法はプログラミング言語で証明を行うときに原理として利用されます。

といってもHaskellを使っているのであれば、自然と帰納法を使っていることと思います。たとえば、上のリストに対して帰納法を使ってみます。リストに対する帰納法は関数で明示的に書き下せば次のようになります：

list_induction
    :: r                        -- Nil の場合
    -> (a -> List a -> r -> r)  -- Cons a as の場合で, as対する結果(r)から新しい結果(r)を返す
    -> List a                   -- 対象のリスト
    -> r                        -- 結果の値
list_induction nil cons Nil          = nil
list_induction nil cons (Cons x xs)  = cons x xs (list_induction nil cons xs)

簡単にいえば、帰納法とはデータ型のすべてのコンストラクタに対して結果を計算する方法を定義することです。リストでいえばNilから結果(ここではr)を計算する方法と、Cons x xsから結果を計算する方法を決めたならば、リストに対する関数が定義されるということです。

これを使えば、たとえばリストの長さを計算する関数lenを次のように帰納的に定義することができます：

len :: List a -> Int
len = list_induction 0 (\a as r -> 1+r)

ここまであからさまな書き方はしないと思いますが、Haskellを書いていれば普段から同じようなコードを書いていることと思います。あるいはPreludeにあるtakeだったら、list_inductionの戻り値の型がr = Int -> List aになることに注意すると、

take :: Int -> List a -> List a
take n xs = list_induction nil cons xs n
  where
  nil :: Int -> List a
  nil n = Nil

  cons :: a -> List a -> (Int -> List a) -> (Int -> List a)
  cons a as k 0 = Nil
  cons a as k n = Cons a (k (n-1))

と書けます。

これらの話は余代数にも同じように言えます。たとえば上で見た余データであるStreamは実は終余代数(Final Coalgebra)であり、それには余帰納法(Coinduction)がついてきます。これは関数で書き下すと、

stream_coinduction
    :: (s -> (a, s))  -- 現在の状態(s)から次の値(a)と新しい状態(s)を生成する
    -> s              -- 初期状態
    -> Stream a       -- 結果の値
stream_coinduction next s = x
  where
    (a, s') = next s
    x.Head = a
    x.Tail = stream_coinduction next s'

となります。余帰納法とは、余データ型のすべてのデストラクタに対して結果を定義することです。StreamでいえばHeadとTailのそれぞれにの場合について結果を定義するということです。

これを使うと、たとえば自然数の列{1, 2, 3,...}を生成するStream Intは、次のように余帰納的に定義できます：

nat :: Stream Int
nat = stream_coinduction (\n -> (n, n+1)) 1

この辺のトピックは A Tutorial on (Co)Algebras and (Co)Induction (1997) [PDF] が分かりやすいかもしれません。

いかがでしたでしょうか。余代数の雰囲気が伝わりましたら幸いです。

採用情報

朝日ネットでは新卒採用・キャリア採用を行っております。