Edited at 2017-12-31

Haskell (その2) Advent Calendar 2017 Day 20

Haskellと層

層とプログラミング

はじめに

Haskellは、モナドという圏論用語を言語仕様に採用した初めての実用プログラミング言語です。歴史的には、Godementが1958年に、層コホモロジーの計算のため使ったのが(コ)モナドの最初の例だと言われています。

層は何らかの空間の「形」を代数的に計算するための仕組みで、局所的な性質と大域的な性質の関係を圏論的に表現するフレームワークと言えます。

一言で言えば、層とは関数とその定義域の組の集りのようなものです。いろいろな大きさの鉱物の結晶が積み重なって、地球全体を地層が覆っている様子をイメージするとわかりやすいかもしれません。層を使うと、定義域が重なりあう部分関数の関係と、それらが全体に波及していく様子を、圏論的に、すっきり表すことができます。

層はいわゆる"幾何的論理(geometric logic)"のモデルでもあり、実はモナドも幾何的論理で表現できるので、層はモナドの一般化でもあります。

例として、HaskellのMap/Setは、Ordインスタンスの作るHaskのサブカテゴリのモナドですが、これを層として表現することができます。

関数言語の文献ではあまり層が言及されているケースはないようなので、層をプログラミングで使ういくつかのメリットを私見で挙げてみます。

データ構造に同値関係を入れた商構造を圏論的に表現できる。
データ構造の部分的性質の広い領域への伝播を、圏論的に表現できる。
データ構造の上に定義される部分関数同士の間の代数と、定義域との関係を圏論的に表現できる。

例えば、data Month = Jan | Feb | .. | Decに、Jan.. Dec, Jan..という巡回的な流れを考えたい場合。後述のグロタンディーク位相を適当に定義し、この巡回構造を表現することが出来ますし、またこのMonth空間の上の状態モナドの層を考えることによって、月の「局所的変動」(先月、来月)が他のデータ(年など)に与える影響を、被覆(covering)写像として表現することもできます。

デメリットもあります。

型レベルで層をコーディングするには、引き戻し(pullback)、イコライザー(equalizer)などが必要。 $H a s k$ で表現することは無理なので、実装はケースバイケースな値レベルのコードになりがち。
高階関数の層は、上記2.の性質は実現しにくい。メモ化、有限写像としての表現など、パターンマッチ可能な一階のデータに落す必要がある。

層の圏

(ただのお話です。詳細はMacLane and Moerdijk[1]を参照してください)

一般に、圏 $C$ から $S e t$ への反変関手

C^{o p} \to S e t

を $C$ の前層(presheaf)と呼びます。米田埋め込み $y$ は最も重要な前層の例です。

圏 $C$ にグロタンディーク位相 $J$ が定義されているとき、前層の部分圏として層の圏 $S h (C, J)$ を定義することができます。層とは、「局所関数」に対し、その制限が適当に定義できるような、特殊な前層のことです。

P (C) \overset{e}{\to} \prod_{i \in I} P (C_{i}) \overset{p_{2}}{\underset{p_{1}}{⇉}} P (C_{i} \times_{C} C_{j})

この $e$ が全ての $C$ の被覆{ $f_{i} : C_{i} \to C$ }につきイコライザーであるとき、前層 $P$ は層です。
$S e t$ の図式であることに注意して下さい。局所関数の制限が、制限の仕方によらず定義できるという意味です。

$S h (C, J)$ から前層圏 ${S e t}^{C^{o p}}$ への埋め込み $i$ は左随伴 $a$ を持ちます。 $a$ はsheafification functorと呼ばれます：

{S e t}^{C^{o p}} \overset{a}{\underset{i}{⇄}} S h (C, J)

a ⊣ i

この左随伴によって、任意の前層から層を作ることができます。

`Ord`インスタンスの"位相"

Haskellで具体的に層を構成してみましょう。

まず第一に、扱いたいデータ構造Xの位相を定義します。
圏 $J$ を次のように定義します。

対象: Xの開区間の有限和
射： (たかだか一つの)包含関係 $C \subset D$

$J$ は引き戻しを持ち、共通部分で表わされます。

この $J$ は、普通の意味での位相にはなっていませんが、いわゆるグロタンディーク位相の基底にはなっています。 $(X, J)$ をサイト(site)と呼びます。

詳細な定義は、Wikipediaの記事及び
MacLane and Moerdijk[1]を参照してください。プログラミング上大事なことは、

上のような基底Jがグロタンディーク位相の公理を満たす限り、その上の層の性質も、層のセクション(後述)の計算も、全て(近似ではなく)厳密な正しさを保証できる。
普通の位相の公理に比べ、グロタンディーク位相の公理はより一般的で満たしやすい。

セクション

開区間C=(a,b)とその開区間全体で定義された値fの組(f,C)をセクション(切ったもの、切片)と呼びます。
射 $D \subset C$ に対し,関数fの定義域をDへ制限しても、(f,D)はセクションになっています。

   (0,3)     ^
   / \       |
(0,2) (1,3)  |
  \   /      |
   (1,2)     |

このような開区間の包含関係の図式を考えると、セクションをどのような包含関係の道にそって制限しても、同じものが得られることがわかります。

逆に、二つのセクション(f,C),(g,D)が $C \cap D$ 上で等しいなら、貼り合わせてより広いセクション $(f \lor g, C \cup D)$ を作ることができます。この、条件つき同等性を仮にEqOnクラスとして定義してみます。


data Section k a = Section { ivmap :: IntervalMap k a }
type Domain  k   = Section k ()

class EqOn a d where
   eqOn :: d -> a -> a -> Bool

-- 制限
restrict :: (Ord k)
         => Section k a -> Domain k -> Section k a
-- 貼り合せ
glue     :: (Ord k, EqOn Domain a)
         => Section k a -> Section k a  -> Maybe (Section k a)

グロタンディーク位相と層の公理は、このrestrict、glueを繰返しても元の性質が保たれることを保証してくれます。例えば、定義域の各点で、有限ステップでノーマライズする項のセクションをいくら制限したり貼り合わせても、計算の有限性は変わりません。いわば、「形」に関する帰納法が可能になるとも言えます。

被覆

こんどは全順序でなく、円のように巡回するデータ構造を考えてみましょう。

data Month = Jan
            | Feb
            | Mar
            | Apr
            | May
            | Jun
            | Jul
            | Aug
            | Sep
            | Oct
            | Nov
            | Dec
            deriving (Enum, Ord)

基底として、次の集合をとってみます。

c   = [Jan .. Dec]
c0  = c \\ [Dec] = [Jan .. Nov]
c1  = c \\ [Jul] = [Aug .. Dec, Jan .. Jun]
c01 = [Jan..Jun]
c10 = [Aug..Nov]
0   = []

    c     ^
   / \    |
 c0   c1  |
 |  X  |  |
 c01  c10 |
   \  /   |
    0     |

前層Fを次の反変関手とします。

-- 対象
F(x) | x == c    = Void
     | otherwise = Int

-- 射

F(c0  -> c)  = const 0  :: Void -> Int
F([]  -> x)  = const 0  :: Int -> Int
F(c01 -> c0) = id    :: Int -> Int
F(c01 -> c1) = (+1)  :: Int -> Int
F(c10 -> c0) = id    :: Int -> Int
F(c10 -> c1) = id    :: Int -> Int

   Fc     |
   / \    |
 Fc0  Fc1 |
 |  X  |  |
Fc01 Fc10 |
   \  /   |
    F0    v

これはそのまま層になっていて、12月から1月にかけて年(Int)が変わる様子を、圏論的に表しています。

セクションの列(c0,2017), (c1,2018), (c0, 2018),(c1,2019), (c0,2019), (c1,2020)..を貼り合わせて、「円」[Jan..Dec]の上に、螺旋状に年をつなげて行くことができます。この年号の螺旋から、年を忘れる関手はグロタンディーク位相の意味で局所同相になります。このような局所同相な関手を被覆(covering)と言います。

結論

モナドが層の計算の中でテキストに最初に記述されてから、来年でちょうど60年。プログラミングで使われる、あらゆる計算可能なデータ構造の幾何を、層は非常に正確に、厳密に捉えてくれます。関数言語の文脈で明示的に層が使われることはあまりないようですが、(コ)モナド、米田マップ、カン拡張他の圏論のアイデアとともに、いずれは関数プログラマの道具箱の中に入ってくるのではないでしょうか。

局所的な順序はあっても、大域的な順序がつけられない、非ユークリッド的なデータ構造は多くあります。多次元的なデータでは猶のことです。層を使って、幾何的構造を生かしつつ、厳密な推論を可能にしよう、という主張が本記事の趣旨でした。

[1]: Saunders MacLane, Ieke Moerdijk,
Sheaves in Geometry and Logic – A first introduction to topos theory
Springer Verlag, 1992

層とプログラミング

@makoraru

Toot

Haskellと層

層とプログラミング

はじめに

層の圏

Ordインスタンスの"位相"

セクション

被覆

結論

Report article

Feedback

`Ord`インスタンスの"位相"