Codataの話

星にゃーん（@takoeight0821）

関数型プログラミングでよく出てくる「データ（代数的データ）」。

その双対である「余データ」を考えると、オブジェクト指向っぽくなることを見ていきます。

前置き：「データ」とは

コンストラクタを用いて構成的に作る値→データ（代数的データ）

code:List.hs

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

data Maybe a = Nothing | Just a

デストラクタ（値を分解する手続き）を用いて値を作れないか？

→余データ（Codata）

デストラクタを用いて値を定義する

code:Stream.hs

codata Stream a = {

.head : a,

.tail : Stream a

}

余パターン

code:Stream.hs

ones :: Stream Int

.head ones = 1

.tail ones = ones

オブジェクト指向っぽく余パターンを書いてみる

code:Stream.hs

ones :: Stream Int

ones.head = 1

ones.tail = ones

各デストラクタが、ちょうどOOPで言うメソッドに対応する。

フィボナッチ数列

code: fibonacci.hs

fibo.head = 1

fibo.tail.head = 1

fibo.tail.tail = zipWith (+) fibo (fibo.tail)

1, 1, 2, 3, 5, ... = fibo

1, 2, 3, 5, ... = fibo.tail

2, 3, 5, 8, ... = fibo.tail.tail

インターフェースと実装をCodataで

code:Set.hs

codata Set = {

.isEmpty : Bool,

.contains : Int -> Bool,

.insert : Int -> Set,

.union : Set -> Set

}

code:Set.hs

finiteSet : List Int -> Set

(finiteSet xs).isEmpty = xs == []

(finiteSet xs).contains y = elemOf xs y

(finiteSet xs).insert y = finiteSet (y:ys)

(finiteSet xs).union s = fold (\x t -> t.insert x) s xs

emptySet = finiteSet []

code:Set.hs

evens = evensUnion emptySet

evensUnion : Set -> Set

(evensUnion s).isEmpty = False

(evensUnion s).contains y = isEven y || s.contains y

(evensUnion s).insert y = evensUnion (s.insert y)

(evensUnion s).union t = evensUnion (s.union t)

参考文献など

Featherweight JavaからCodataを持つ言語へのコンパイルを定義している。

Codataで関数を表現できることも示している。

(\x.x) 42 ==> { .app x -> x }.app 42

同じ著者。CodataとCopatternおよびその実装について論じている。

CodataをDataに変換できる。

遅延評価が必要になる。

Codataについて述べた日本語の記事。

Copatternを持つ言語の一つAgdaでの使い方。