2013-06-09

Yoneda lemmaとOperational Monad

Haskell 圏論

最近Haskellerの間で人気になりつつある(？)Operational Monadというものについての記事です。

サンプルプログラム

Operational Monadは http://hackage.haskell.org/package/free-operational で定義されています。後でも説明しますがこれはFree Monadの構造をもったモナドになります。

以下のコードはhttps://gist.github.com/myuon/5737483に載せておきました。

{-# LANGUAGE GADTs #-}
import Control.Monad
import Control.Monad.Operational.Simple

data Simple a where
  End :: Simple a  
  Put :: String -> Simple ()
  Get :: Int -> Simple String

ここではGADT拡張を使います。上ではSimpleというデータ型のコンストラクタの宣言を、型クラスの函数宣言のようにして作っています。

Free Monadの記事(Free Monadを使ってみよう！ - みょんさんの。とFree Monadを使ってみよう！(2) - みょんさんの。)のところでもやりましたが、Free Monadとして使うために、必要な値を受け取ってSimple型を返す函数を作ってあげなければいけません。
それが以下です。

put :: String -> Program Simple ()
put = singleton . Put
 
end :: Program Simple a
end = singleton End
 
get :: Int -> Program Simple String
get = singleton . Get

最後に、これをrunするためのものが必要ですね。ここで使われているinterpretという函数はControl.Monad.Operational.Simpleで定義されています。

run :: Program Simple a -> IO a
run = interpret step
  where
    step :: Simple x -> IO x
    step (Put a) = putStrLn a
    step End = putStrLn "End" >> undefined
    step (Get n) = replicateM n getChar

これでおしまいです。あとは適当なプログラムを書いて走らせましょう。

tinyProgram = do
  put "hello, world!"
  end
  
main = run tinyProgram

実行結果

hello, world!
End
Operational.hs: Prelude.undefined

Operational Monad

上で作ったtinyProgramはdo記法を使っていることからも、Simple型がモナドとして機能していることは分かります。しかし、私達はSimple型をMonadはおろかFunctorにすらしていません。しかしなぜこんなことができるのでしょうか？結論から言ってしまえば、Simple型はOperatinal Monadの力によってFunctorを経てFree Monadの構造が与えられているのです。

どういうことでしょうか。Operational Monadの定義から考えてみましょう。

-- http://hackage.haskell.org/packages/archive/free-operational/0.3.0.0/doc/html/src/Control-Monad-Operational-Simple.html#Program

newtype Program instr a = Program { toFree :: Free (Yoneda instr) a }

実は、重要なのはここだけです。FreeというのはFree Monadですが、その中にYonedaというものが見えると思います。これはつまり、


inst	ただのデータ型
Yoneda instr	Functor
Free (Yoneda instr) a	Free Monad

という関係になっているのです！

次に出てくる疑問は、ではただのデータ型をFunctorにしているYonedaというのは何？ということでしょう。これは圏論で登場する米田の補題という有名な補題に関係があります。

(Yoneda f) functor

米田の補題を理解するためには少しだけ準備が必要ですが、ここに書ききれるものではないので簡単に説明だけして終わることにします。
興味がある方は補足のところを読んで下さい。

米田の補題で重要なのは、普通の集合と函手の集合には全単射の関係があるということです。つまり、ある集合から1つ元を取り出すと、函手が1つ作れる、あるいはその逆も可能という対応関係です。

つまり、自分でデータ型を、函手に対応づけすることができる = データ型から函手を作ることができるという対応です。

以下に定義を示します。

-- http://hackage.haskell.org/packages/archive/kan-extensions/3.1.1/doc/html/src/Data-Functor-Yoneda-Contravariant.html#Yoneda

data Yoneda f a where
  Yoneda :: (b -> a) -> f b -> Yoneda f a

instance Functor (Yoneda f) where
  fmap f (Yoneda g v) = Yoneda (f . g) v

ご覧の通り、(Yoneda f)はFunctorになっていますね！これは、与えられたfというデータ型を使って、(Yoneda f)というFunctorを創りだすことができるということを示しています。まさに魔法のようですね！

何度も言いますが、与えられたデータ型を使って、(Yoneda f)というFunctorを創りだすことができることが「米田の補題」によって保障されているわけです。

(補足)Yoneda lemma

米田の補題は圏論では非常に有名な補題(というか定理)で、ここから色々な定理を示すことができる強力な定理です。
補題のステートメントは単純で、
$F:\mathscr{C} \to Set$ が函手(functor)のとき、 $\Phi:Set^{\mathscr{C}^{op}}(\mathscr{C}(-,c), F) \simeq F(c)$ なる写像が存在する(つまり上の写像 $\Phi$ が全単射となる)ということです。
ここで、 $\Phi(\alpha) = \alpha_c 1_c$ 、つまり $\alpha:F \to \mathscr{C}(-,c)$ という自然変換を $\alpha_c 1_c$ という元に対応させています。

上で出てきた函手 $\mathscr{C}(-,c)$ を、Yoneda函手 $Y_c$ と言います。

これは函手圏 $Set^{\mathscr{C}^{op}}$ の射である自然変換の集合と、集合圏の対象である集合との間に全単射の関係があるということを意味しています。

これによって、自然変換と集合の元を対応させることができます。これが、Haskellでは一体どういった意味を持つのでしょうか？

data Yoneda f a where
  Yoneda :: (b -> a) -> f b -> Yoneda f a

instance Functor (Yoneda f) where
  fmap f (Yoneda g v) = Yoneda (f . g) v

Yonedaは射(b -> a)と対象(f b)を受け取ってYoneda f aなるデータ型を返します。f(に対して定義されたfmap)を上で出てきた函手Fだと思いましょう。

圏論	Haskell
$\mathscr{C}$ の射	(b -> a)
$F:\mathscr{C} \to Set$	fmap :: (b -> a) -> f b -> f a
$Y_c:\mathscr{C} \to Set$	fmap :: (b -> a) -> (Yoneda f) b -> (Yoneda f) a
$\alpha:F \to Y_c$	nat1 :: forall2 b. f b -> (Yoneda f) b
$\alpha_c:F(c) \to Y_c(c)$	Yoneda (b -> a) :: f b -> (Yoneda f) a
$\alpha_c(1_c) \in Y_c(c)$	Yoneda (b -> a) (f b) :: (Yoneda f) a

米田の補題が言っているのは、(Yoneda f) a と nat :: forall b. f b -> (Yoneda f) b とが確かに対応すること、つまりこの意味でのYonedaが

data Yoneda f a where
  Yoneda :: (b -> a) -> f b -> Yoneda f a

と定義することができる(このような写像が常に存在する)ことを言っていたのです。

参考文献

Freeモナドを超えた！？operationalモナドを使ってみよう - モナドとわたしとコモナド Operational Monadの存在をここで知りました
http://hackage.haskell.org/package/free-operational YonedaとFree Monadを使ったOperational Monadの実装
http://hackage.haskell.org/package/kan-extensions Yoneda等が定義されているパッケージ
Understanding Yoneda | Bartosz Milewski's Programming Cafe 自然変換をHaskellで表現するとはどういうことか、などに興味があれば読んでみて下さい。補足のところで説明もなく使ったforallの扱いなどが丁寧に解説されています。

*1:プログラム中には直接は出て来ませんが、forallを取り除いたバージョンが liftYoneda = Yoneda id として定義されています。

*2:圏論でいう``natural in d"に対応するのがHaskellでのforall d.に対応すると考えてよいみたいです。詳しくは参考文献の4を参照。

2013-05-30

PSh圏とcolimit

圏論

PSh圏とcolimit

位相空間Xに対して、X上の前層Fとは、Xの開集合から集合への写像
$F(U) \quad \quad (U \in \mathcal{O}(X))$
(で、かつ制限写像というものが定められているものの)のことです(詳しくは層 (数学) - Wikipedia等を参照)。

ここで、 $\mathcal{O}(X)$ に包含関係で順序を入れてこれを順序集合の圏( $\mathscr{C}$ と表記)とみなします。するとFは、
$F: \mathscr{C}^{op} \to Sets$
なる反変函手であって、この函手を対象、函手の間の自然変換を射とするような函手圏 $\mathbf{Sets}^{\mathscr{C}^{op}}$ が定義できます。
(余談ですが、 $\mathbf{Sets}^{\mathscr{C}^{op}}$ は米田の補題でもおなじみの圏です。米田函手は $Y:\mathscr{C} \to \mathbf{Sets}^{\mathscr{C}^{op}}$ という函手だったので、これは位相から前層への写像とみることができます。)

こうしてできたXの上の前層の圏を $PSh(X)$ とかきます。

さらにX上の前層が層であるとは、Xの全ての開集合 $U$ について、既約性条件と閉条件と呼ばれる2つの条件をみたすようなもののことです。これを圏の言葉で書くと、
対象 $F(U)$ と射 $F(U) \to \Pi_i F(U_i)$ が $\prod_i F(U_i) \Rightarrow \prod_{(i_0,i_1) \in I \times I} F(U_{i0} \times U_{i1})$ のequalizerである*1といえます。

前層はただの反変函手に過ぎませんがよい性質を持っています。例として次の命題を挙げます。

Def: 函手 $F: \mathscr{C}^{op} \to Sets$ が $h_X:=\mathscr{C}(-,X) \quad : \quad \mathscr{C}^{op} \to Sets$ と自然同型であるとき、この函手を表現可能とよぶ。

Prop: 全ての前層は表現可能な前層のcolimitである。

とても面白い性質です！

前層がlimitを持てばequalizerも持つはずなので上のことから自然に層になります。
(またnLabによるとこのcolimitはcoendを使って書くとすっきり表現できるらしいのですが、まだそこまでは理解が追いついていないです。)

参考文献

Stacks Project — Tag 006D 前層の定義
Stacks Project — Tag 0071 層の定義
representable functor in nLab 表現可能函手の定義
presheaf in nLab 最後にあげた命題の証明ものってます

*1:ここで⇒は、2本の平行射を表します

2013-02-23

テキストフォーマットが欲しいという話

Haskell

Haskellで時々Formatがしたくなる時があります。
しかしこれと言って便利そうなものが見当たらず、自作しました。

myuon/FuncFormat · GitHub

import Text.FuncFormatとすれば使えるようになります*1。

ほんの少しだけTemplateHaskellの闇魔術を利用しているので、準クォートによって分かりやすく(?)テキストを整形することが可能です。
以下はそのサンプルです。

{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE OverloadedStrings #-}
import Text.FuncFormat
import Data.Text
import Control.Lens

-- [format| {_1} |] f (a,b) == pack $ show $ f _1 (a,b)

main = putStrLn $ unpack $ [format| {_1}, {_2}!|] view view ("hello", "world")
-- output: hello, world!

やっていることは単純で、[format|と|]で囲まれた部分を文字列として受け取って、Parsecを用いてパースして函数を適用させて元の文字列に埋め込んでいるだけです(詳しい使い方はgithubのREADMEでも読んで下さい)。

ちょっとだけ裏話

Control.Lensを使ってタプルから値を取得する、というアイデアは最初からあったのですが、実は[format| {_1} {_2}|] view ("hello",100)などとして埋め込もうとすると、「viewの型が文字列なのか数値なのか分からない！」とコンパイラに怒られます。上の例だとview _1 ("hello",100)とview _2 ("hello",100)を同じ文脈で評価していますが、前者の場合viewは文字列を返し、後者の場合は数値を返すことになるので同じ函数が場所によって異なる型として推論されてしまってコンパイラに怒られるというわけです。

という事情があって、仕方なく[format| {_1} {_2}|] view view ("hello!", 100)とすることで、{}の中の函数と[format|...|]に続く函数がそれぞれ対応するということにしてコードを組みました。

ちなみにですが、やたらとviewにこだわっていたのは、

[format| {_1}!|] (\x (y,z) -> set x y z) ("hello", (10,100))

のようにしてview(値を取り出す)以外にも、set(値を更新/書き換えて反映させる)などが出来るようにするためです。

もちろん、[format| {f} |] g xがg f xとして解釈できるのであれば別に_1やviewを使う必要もありません。
これによって、少なくともある程度抽象度を保ったままテキストのフォーマットができるようになっています(ると思い込んでいます)。

今のところはこれで特に不満もありませんが、もうすこしフォーマット以外に便利な使い方を思いついたら反映させるかもしれません。という訳で、Haskellでも(たった100行そこらで(!))Formatは簡単にできるのだという話でした☆

(まぁどうでも良いことなんですが、あんまり何も考えずにこういうのを作って、作った後で同じ事をしているパッケージを見つけたのでちょっと悲しかったです…先に調べておくべきでした><)

参考

TextFormat - github 今回私が作ったもの

以下は私の今回作ったのとは一切関係のない、別のパッケージです

*1:Data.Text.Formatにしたかったのですが、すでにそういうパッケージがHackageに存在したので避けました

Just $ A sandbox

プログラミングと計算機科学とかわいさ

Yoneda lemmaとOperational Monad

サンプルプログラム

Operational Monad

(Yoneda f) functor

(補足)Yoneda lemma

参考文献

PSh圏とcolimit

PSh圏とcolimit

参考文献

テキストフォーマットが欲しいという話

ちょっとだけ裏話

参考