エムスリーテックブログ

エムスリー(m3)のエンジニア・開発メンバーによる技術ブログです

代数的データ型とその双対性

こんにちは,エムスリーエンジニアリンググループの榎田(Twitter: @niflh)です.今年度の4月に新卒で入社しました.入社してからは AI・機械学習チームというところで機械学習プロダクトのインフラのお仕事をしていましたが,11月末からチームを異動し,Unit4 というチームにいます.このチームでは医療系ポータルサイト m3.com のメディア系サービスや,全ページに共通で表示するヘッダーメニューの開発などをしています.

これらの開発では Scala が使われていることを異動後に知りました.私は直近で Scala を使う案件は持たない予定ですが,少なくともレビューで Scala のコードは読むので,いい機会だと思って年末年始から勉強を続けています.その際に読んだ "Essential Scala"*1 という本にて,「代数的データ型」(Algebraic Data Type, ADT)という概念が紹介されていました.この概念について,主に理論的な観点から色々調べてみたら面白かったので,その話をします.

本稿の内容は次のとおりです.

  • ADT の構成要素である, product/sum type の概念を説明する.
  • "Essential Scala" における product/sum type の解釈を紹介しつつ,intersection/union type と比較して解釈する見方も紹介する.
  • product type と sum type,および intersection type と union type の間に共通して現れる「双対性」について述べる.

対象読者は次の条件のうちどれか一つを充たす方を想定しています.

  • "Essential Scala" を読んだことがある
  • ADT なる概念を見たことがあって,興味がある
  • 数学が好き*2

product type と sum type

"Essential Scala" においては,「ADT とは,product type と sum type を組み合わせたデータ型のこと」だとされています*3.まずはこの product/sum type とはどういうものか述べていくことにします.

product type

BC が何らかの型であるとします*4BC の product type とは,BC のタプルからなる型のことを言います.Scala のコードに起こすならば,

case class A(b: B, c: C)

ないしは

trait A {
  def b: B
  def c: C
}

となります.

sum type

ふたたび,BC が何らかの型であるとし,更に BC には重なりがないとします*5.型 ABC の sum type であるとは, B 型または C 型のどちらかであることを言います. tagged union であると言っても同じことです.Scala のコードに起こすならば,

sealed trait A
case class B extends A
case class C extends A

となります.

ADT のパターンたちの見方

Essential Scala における見方

"Essential Scala" において,先程の product/sum type はそれぞれ,has-a/is-a,and/(x)or をモデリングする手段であるとして説明されています.本にも次のような表でまとめられていました;

f:id:ehlfin:20200310231152p:plain
Essential Scala における ADT をまとめた表

この表に従えば,product type は「A 型の値は B 型の値と C 型の値を持つ (A has a B and C) 」を表したものだと言えますし, sum type は「 A 型の値は,実際には B 型または C 型どちらか一方の値である (A is a B or C)*6 」ことを表しているとされています.これらの解釈じたいは,大きく不自然なものだとは思いません.寧ろ,実際のアプリケーションに組み込む上での使い方を想像しやすくなるなどのメリットが考えられるので,このような自然言語による直感的な意味づけは一定の意義があることでしょう.

ところで,見て分かる通り,この表にはまだ穴が空いています."Essential Scala" では,この穴を簡単に埋め,次の話題へと移っていきます.本稿でも,表の空欄に対応するものをそれぞれ簡単に洗い出しておくことにしましょう.

まず is-a and パターン.文章を書けば A is a B and C ということになるので,B 型と C 型の両方の性質をそなえているということになります.コードに落とすなら

trait B
trait C
trait A extends B with C

でしょう. B 型と C 型の共通部分であると言っても同じことです.

次いで has-a or パターン.文章では A has a B or C となります.なのでコードとしては

sealed trait A
final case class D(b: B) extends A
final case class E(c: C) extends A

となります.注意しておくべきこととして,これはいわゆる (untagged) union type にはなりません*7

私はここまで見たところで,この has-a/is-a, and/or という座標軸のとり方に,どことない違和感を感じ始めました.その違和感の源泉と,私にとって「自然な」座標軸を提示することを,以下では試みることにします.

別の見方

私が疑問を抱くのは, has-a パターンが存在する中で is-a パターンが別に定義されていることの意義です.has-a or パターンに現れた型 DE について,こういう実装をしたらどうでしょう.

case class D(b: B) extends A {}

このように,field として b を持つのみで,それ以外に有意な実装を持たないような実装がありえます.これは本質的には B 型の値と同一視できるでしょう*8.だとすると, is-a or パターンが has-a or パターンの特別な場合に帰着してしまうので,わざわざパターンを分けておく必要がなくなります.

もっと言うと,この中に「集合の共通部分 intersection type」だと見做せるパターンが出てきましたが,その相方としては「集合の和集合 (untagged) union type」を用意してほしい,というのが個人的な気持ちです.つまり,product/sum type というペアと,intersection/union type というペアで整理したほうが個人的には受け入れやすい気がする.この主張は「気持ち」という言葉を使っていることから分かる通り,なんとなくで言っている部分も多いですが,強いて理由を見出すならば以下の2つです.

  • product/sum type は「材料にする2つの型の共通部分のインスタンスでも,どちらの型から来たか区別する」が,intersection/union type は「材料にする2つの型の共通部分のインスタンスは,どちらの型から来たか区別しない」という違いを持つ.このことによって,棲み分けが明確になる.
  • product/sum type と intersection/union type という見かけが異なる二組はどちらも,ある共通の「双対性」で結ばれたペアであるという特徴を持つ.

1つ目については,BC とが同じ型であった場合を考えると振る舞いがよく分かるでしょう.product type は左右の区別がありますし,sum type はそもそも disjoint になるようなものしか扱わない(2つの型に共通部分があっても無理やり区別する).一方,BB の intersection や union は B 型として扱われるべきです*9

product/sum, intersection/union の双対性

さて,2つ目の理由について述べていくために,まずはさきほどのペアに共通する特徴について説明していくことにします.

product/sum type の数学的な特徴

product という名前は,数学における「直積」と呼ばれる概念に由来すると思われます.ここで, BC を何らかの集合とするとき, B C の(集合としての)直積 B \times C とは,


\{\, (b,c) \,|\, b \in B, c \in C\, \}

なる集合として定義されます.言葉遣いは数学のそれですが,やはり要するに B と C のタプルのことです.

プログラミングをしているときに意識することは少ないのでしょうが,直積については,次のような注目すべき性質があります*10


直積の性質.次のような関数 pB, pC を考える;

def pB(a: A): B = a.b
def pC(a: A): C = a.c

X および関数 fB(x: X): BfC(x: X): C が任意に与えられたとき,全ての x: X に対して pB(f(x)) = fB(x) および pC(f(x))=fC(x) を充たすような関数 f(x: X): A が一意的に存在する.言い換えれば,次の図式を可換にするような f(x: X): A が一意的に存在する.

f:id:ehlfin:20200310230520p:plain
直積の性質


主張はなんだかものものしいですが,この f はややこしい関数ではなく,ほかの関数の組み合わせで作れます*11.出力を A 型にしたいので,B 型と C 型の値が必要ですが,それは fBfC を使えばできます.擬似コードを起こすならば例えば;

def f(x: X): A = new A(fB(x), fC(x))

このようにして定義した f が,上の図式を可換にする唯一の関数であることの詳細な検証は省略します*12

product が「直積」を想起させたように,sum という名前は,数学において「直和」と呼ばれるものと似ています.ここで,BC を何らかの集合とするとき,BC の(集合としての)直和 B \oplus C とは,


\{ \,(x,i)\, |\, x \in B \cup C \}

なる集合として定義されます.2つ目の i は,どちらの集合に属しているかを示す目印です*13*14. 直和についても,直積とよく似た…というより,直積の「裏返し」とでも呼ぶべき性質が成り立つことが知られています.


直和の性質.次のような関数 iB, iC を考える;

def iB(b: B): A = b
def iC(c: C): A = c

型 X および関数 gB(b: B): XgC(c: C): X が任意に与えられたとき,全ての a: A に対して g(iB(a)) = gB(a) および g(iC(a))=gC(a) を充たすような関数 g(a: A): X が一意的に存在する.言い換えれば,次の図式を可換にするような g(a: A): X が一意的に存在する.

f:id:ehlfin:20200310230541p:plain
直和の性質


直和において現れた図式は,直積において現れた図式の「矢印を全て逆向きにしたもの」であることに注意してください.この,「矢印の向きが全て逆」という現象を指して,「直和と直積は互いの双対」という言い方をします.

g の構成についても述べておきます.gA 型を受け取るわけですが,実際には B 型が来る可能性もあれば, C 型が来る可能性もあります.なので,実際にどの型が来たかに応じて場合分けをすればよいです;

def g(a: A): X = {
  a match {
    case b: B => gB(b)
    case c: C => gC(c)
  }
}

これが上の性質を充たす唯一の関数であることは,直積の場合と同様にして証明できます.

intersection type / union type の特徴

さて,intersection/union は,その名の通りただの集合の共通部分・和集合なのですが,この共通部分についても,同様の図式を書くことができます.それを見るために,次のような約束を導入してみます.

約束.2つの集合  A B がある時に, A B の部分集合である時,すなわち  A \subset B のときに, A \to B と書くことにする*15

そうすると,集合の共通部分に関して,先ほどと非常によく似た図式を書くことができます. B \cap C \subset B なので, B \cap C \to Bです.同様に, B \cap C \to C です.さて, X を適当な集合とし, X \to B かつ  X \to C であったとします.矢印を使わずに書くと  X \subset B かつ  X \subset C ということなので, X \subset B \cap Cです.矢印のことばにすれば,  X \to B \cap C という矢印が伸びたことになります.図式にまとめると以下のとおりです.

f:id:ehlfin:20200312233607p:plain
共通部分の図式

この議論を「ほとんどそのまんま繰り返すことで」,以下の図式も得られます.

f:id:ehlfin:20200312233744p:plain
和集合の図式

共通部分と和集合の図式は,矢印の向きが全て逆になっていることに注意してください.先ほどと同じ「双対性」がここにも顔を出します.

ふたつのペアに共通する特徴

product/sum type と intersection/union type について,まったく同じ形の図式が書かれることがわかりました.この「共通のパターン」には名前がついていて,product/intersection type のほうに現れた図式のことをまとめて product と,sum/union type のほうに現れた図式のことをまとめて coproduct と呼びます*16.見かけが異なる2つのペアから,まったく同じ図式が導かれることそのものが,個人的には面白いと感じています.

勉強した感想

Scala も ADT もはじめて勉強しましたが,周辺まで広げるといろいろな世界が広がっていて面白いなと思いました.色々と疑問が尽きないところもあるので,お詳しい方は是非いろいろ教えて下さい.

気になっていること

私はこのあたりの話を専門的に修めたわけではなく,断片的な知識の寄せ集めしか持っていません.そんな中,例えば次のようなことが気になっています.

  • この「双対性」があることに下支えされている,(日常のプログラミングに現れるような)具体的なありがたみをなにか見いだせないか.
  • product/sum type を再帰的に組み合わせたデータ構造は,なぜ(ADT という)特別な名前付けをされるほどに重要視されているのか.例えば,「ADT は,プログラム上有用な概念たるところの xxxx が表現できる最小の集合である」といった形の特徴付けができないか.
  • product/sum type は (co)product と見做せたが,では一般化して (co)limit を取った時に出てくる対象の,プログラム的な対応物はなにか*17
  • Curry-Howard-Lambek 対応について.特に圏論と対応をつけることで初めて見えるものはなにか.Curry-Howard 対応だけでは見えないものはなにか.

We are hiring!

弊社はテックブログの幅広さを見ればわかるように,いろいろなバックグラウンドを持つギークなエンジニアがいるのが特徴です.このような話が好きな人,この記事に数学的な間違いを見つけた人はぜひご応募ください!*18

jobs.m3.com

*1:公式で pdf が配布されているので無料で読めます.こちらからどうぞ: https://underscore.io/books/essential-scala

*2:本稿に,圏論を強く意識した側面があるのは事実です.が,ADT を使う上で圏論の知識が必須であるとはまったく考えていません.運用に圏論の知識を要求する概念は様々な面で実用的でないと考えます.…とはいえ,私がこのような記事を書いたのは,そのような「実用的でない」ものを好きであるからに他ならないのですが.

*3:この定義の一般性・妥当性については,本稿では議論しません.本当は複数書籍を当たって ADT の定義を見比べるのが良いのでしょうが.

*4:本稿では「型」の厳密な定義はせず,暗黙のうちに何かしらの集合と同一視して話をします.このようないい加減な立場を取る理由は2つです;ひとつは,意味論を厳密に取り扱うことは本稿の目的ではないこと.もうひとつは,型理論の形式的な取り扱いが私の能力を越えることです.

*5:どうしても B 型と C 型の値を区別したいが故にこのような記述をしています.重なりがあった場合は,class field にダミー変数を置いた新しい class を定義するなどの方法を使って最初から無理やり別の型として扱うか,sum type 定義時にどちらの型なのかを区別する情報を付与するなどの処理が考えられるでしょう.

*6:ほんとうは A is a B xor C と書くべきだと思いますが,自然言語の仕様で or と書くのが一般的であるようです.個人的には仕様というよりバグだと思っているので修正の pull request を出したいのですが,我々が使っている自然言語がどのリポジトリで管理されているのか,私は寡聞にして知りません.

*7:パターンの名前こそ has-a or ですが,実態は has-a xor パターンと呼ぶべきものであることを繰り返しておきます.

*8:単元集合 \{x\}とその要素  x を同一視することとほぼ同義のことを主張しているつもりです.勿論,状況によってはこの同一視が許されないケースもあります(自然数の定義をしている時など).しかし ADT が本領を発揮すると想定されるような状況で,この同一視が問題になるケースはどれくらいあるのでしょうか.あまりないのでは,と思っています.

*9:べきです,という言い方をしているのは,実際のライブラリ等でどう扱われるかを私が広く知っているわけではないからです.例えば, D extends B with B というナンセンスな書き方がコンパイルを通るかどうかも私は確かめていません.

*10:なぜこれが「注目すべき」性質なのか,ひとことでわかりやすく説明するのは容易ではないと考えます.その理由の一端について,私の理解をお伝えすることが,本稿の大きな目的の一つです.

*11:f に対応する矢印を点線で書いている理由はここにあります.ほかのデータから(半ば自動的に)作れることを指してか「f は自然に伸びる,自然性を充たす」という言い方もされます.

*12:実際に可換にしていることは計算すればわかります.逆に,もし可換になっていたとするとこのような形にならざるを得ないです.

*13:こう書くと少し曖昧なところはありますが,雰囲気は伝わるでしょう.本当に厳密にやりたいのであれば,例えば Wikipedia の定義にあるように,適当な添字集合を使って定義してください.

*14:たとえ  B C に共通部分があった場合でも,実際には B から来てますか? C からですか?ということを区別しているという点で,sum type と非常によく似ていると言えるでしょう.

*15:この矢印は包含写像を表していると思えば良いです.

*16:これらはいずれも圏論由来の概念です.圏論を知っている人へ向けてもう少し正確に述べると, product/sum type は型を集合と同一視して,集合の圏で (co)product を取ると得られるが,intersection/union type は,型の親子関係から定まる半順序構造を圏と見做したときの (co)product である,ということを述べています.

*17:おそらく colimit が recursive data structure, limit が (infinite) stream に対応するのだろうなということまでは予想していますが,手元で証明をつけていません.

*18:間違いを見つけたら,たとえば入社後に私にこっそり優しく教えて下さい.私はあまりメンタル強くないので,マサカリはご遠慮ください.