「茨城」の読みは「いばらぎ」ではない
いばらき、と読め
型からHello world
Restricted Wordsに参加した。
"Hello World"という文字列を出力するプログラムを、文字・文字列・数値リテラルを使わずに書くという問題。で、回答のコードがこちら。
import Data.Reflection -- cabal install reflection main = putStrLn $ map toEnum [ reflect ([] :: [D (D (D (SD (D (D (SD Z))))))]) , reflect ([] :: [(SD (D (SD (D (D (SD (SD Z)))))))]) , reflect ([] :: [(D (D (SD (SD (D (SD (SD Z)))))))]) , reflect ([] :: [(D (D (SD (SD (D (SD (SD Z)))))))]) , reflect ([] :: [(SD (SD (SD (SD (D (SD (SD Z)))))))]) , reflect ([] :: [D (D (D (D (D (SD Z)))))]) , reflect ([] :: [SD (SD (SD (D (SD (D (SD Z))))))]) , reflect ([] :: [(SD (SD (SD (SD (D (SD (SD Z)))))))]) , reflect ([] :: [D (SD (D (D (SD (SD (SD Z))))))]) , reflect ([] :: [(D (D (SD (SD (D (SD (SD Z)))))))]) , reflect ([] :: [D (D (SD (D (D (SD (SD Z))))))]) ]
reflectは、型レベルにエンコードされた値を値レベルに戻す関数なのだ。
class Reifies s a | s -> a where -- | Recover a value inside a 'reify' context, given a proxy for its -- reified type. reflect :: proxy s -> a
通常は、なんとunsafeCoerceを駆使してインスタンスを動的に生成するという方法で、値を実行時に型にエンコードするのが普通の使い方。コワイ！だが、Reifiesにはもう一つ、Intのインスタンスもある。
data Z -- 0 data D (n :: *) -- 2n data SD (n :: *) -- 2n+1 data PD (n :: *) -- 2n-1
[Z]という型をreflectすると0、[D n]という型をreflectすると2 * n、[SD n]という型をreflectすると2 * n + 1になる。これを利用して、型から自然数を生み出せるのだ。
Prelude Data.Reflection> reflect ([] :: [(D (SD (D (SD (D (SD Z))))))]) 42
あとはtoEnum :: Int -> Charで文字に変換して、リストを作ればOK。なんて卑怯純粋で安全な方法！
Given
give :: a -> (Given a => r) -> rという関数は、動的にGivenクラスのインスタンスを生成するgiveで与えた値は、given :: Given a => aによっていつでもどこでも取り出せる。何かと便利だ。
モナドとはモナドである
この記事を読む前に、絶対に理解出来ないモナドチュートリアルに一度目を通してみてほしい。モナドを理解していく上で、とても重要なことが書かれている。
改めて言おう、モナドはモナドだ。コンテナだとかプログラマブルセミコロンだという説明では、モナドのすべてを正確に表せるとは言い難い。では、モナドを過不足なく説明できる、モナド以外の言葉はあるのか？
実は、モナドを表現し、かつモナドで表現される言葉は存在する。その一つは手続きである。手続き型言語の「手続き」だ。
手続きとは何か
手続きは結果を持つ
おおよそすべての手続きは何らかの結果を持つ。Haskellの()、C言語のvoid、PythonのNone、Rubyのnilなども結果の一種だ。結果が出ないとしたら、そのプログラムは停止しないか、途中で異常終了するだろう。
手続きには最小単位が存在する
処理系が扱っている以上、手続きが際限なく分解できるということはあり得ない。抽象的な文脈なら、「文字を出力する」のも最小単位と見てよいだろう。
「手続きAを実行した後手続きBを実行する」といったものも手続きである
当たり前だが、大事な性質だ。これによって手続きを組み合わせ、大きなプログラムを作ることができる。
「何もしない」のも手続きである
何もしなくても手続きになる。ならないと色々と困る。ただし、「結果を持つ」という性質は満たさなければならない。
さて、手続きの4つの性質を確認したが、以下のような疑問が残る。
- 「Aを実行した後Bを実行する」とき、Aの結果はどこに行くの？
多くの手続き型言語では代入構文を使って手続きの結果を保存している。Pythonならこんな感じだ。
s = raw_input()
しかし、結果を利用するためだけに変数の仕組みを持ち出すのは美しくない。「変数なんてどの言語でも備えているだろ」と思うかもしれないが、今回はそうではないのだ。そこで、「関数」を使おう。
- 「Aを実行し、その結果を手続きを返す関数に渡す。そして、返ってきた手続きBを実行する。」
要するに、「現在のスコープに結果がある」という条件を満たせばよい。
Haskellで手続きを表現する
以上の点を踏まえて、Haskellで手続きを表現する方法を考えてみよう。
手続きは「結果」を持つ。
結果の型をaとすると、少なくとも手続きの型はT aのようになる。単なる値と区別しないと作る意味がない。
手続きには最小単位が存在する
とりあえず、以下のものを最小単位としてみよう。
Helloworld :: T () -- Hello, worldを表示する。 GetLine :: T String -- 文字列を入力する。 PutStrLn :: String -> T () -- 文字列を引数に取り、その文字列を表示するという手続きを返す。
ちょっと待った！HelloworldやMyGetLineはコンストラクタなのに(コンストラクタは大文字で始まる)、自由に型を指定することができるのか？
できる、そう、GADTならね。GHCのGADTs拡張を使うと、コンストラクタとその型を列挙して代数的データ型を定義できる。
{-# LANGUAGE GADTs #-} data T x where Helloworld :: T () -- Hello, worldを表示する。 GetLine :: T String -- 文字列を入力する。 PutStrLn :: String -> T () -- 文字列を引数に取り、その文字列を表示するという手続きを返す。
GADTはとても便利な機能だ。以降の性質も、GADTを使って表現しよう。
「Aを実行し、その結果を手続きを返す関数に渡す。そして、返ってきた手続きBを実行する。」
これを実現するには、手続きAと、結果を受け取る関数がコンストラクタの引数に含まれていればよい。
infixl 1 :>>= data T x where Helloworld :: T () GetLine :: T String PutStrLn :: String -> T () (:>>=) :: T r -> (r -> T a) -> T a
(:>>=)という演算子はなにかに似ている気がするが、今は考えないでほしい。
「何もしない」のも手続きである
ただ結果を保持するだけのコンストラクタを追加する。
data T x where Helloworld :: T () GetLine :: T String PutStrLn :: String -> T () (:>>=) :: T r -> (r -> T a) -> T a Return :: a -> T a
これで、文字を入出力するという操作ができる、手続きの枠組みができた。では、使ってみよう。
Return 42 :: T Int -- 42を返す Helloworld :>>= \_ -> Return 42 -- Hello, world!した後42を返す GetLine :>>= PutStrLn -- 入力した文字列をそのまま返す GetLine :>>= PutStrLn . reverse -- 入力した文字列を逆転させて返す
確かに表現力はある。実は、これがモナドだ。
正体
モナドは、上で定義した4つの性質のうち、「結果を持つ」「合成できる」「何もしない」が保証される構造だ。
Haskellの強力な仕組みである型クラスを使うと、このように表現できる。
class Monad m where return :: a -> m a (>>=) :: m a -> (a -> m b) -> m b
instance Monad T where return = Return (>>=) = (:>>=)
Monadのインスタンスにすると、これから出てくる様々なモナドを、returnと(>>=)という二つの関数で統一的に扱える。しかも、do記法というHaskellの非常に便利な機能を使えるようになる。
do記法を用いると、さながら手続き型言語のように手続きを記述することができる。いや、do自体が手続き型言語であると言った方が良いだろう。
echoReversed = do s <- GetLine PutStrLn (reverse s)
もっと様々な手続きを書きたければ、Tに新たなコンストラクタを追加すればよい。モナドは、実はとても簡単に作れるものなのだ。
もっと簡単に
(:>>=)とReturnはモナドに必ず必要なため、この部分だけを切り出した構造を作れば、より簡単にモナドを作れそうだ。
data Program x where (:>>=) :: Program r -> (r -> Program a) -> Program a Return :: a -> Program a
ところが、これだけだと手続きの最小単位がないため意味がない。手続きの最小単位のための型を別に作るようにしてみよう。
data Program t x where Unit :: t a -> Program t a (:>>=) :: Program t r -> (r -> Program t a) -> Program t a Return :: a -> Program t a data MyActions x where Helloworld :: MyActions () GetLine :: MyActions String PutStrLn :: String -> MyActions () type T = Program MyActions x
こうして得られたTもやはりモナドになる。機能を拡張したいときは、Programを変えずに、MyActionsを変更すれば大丈夫。
このような、機能の最小単位の集まりからモナドを作る仕組みは、Operationalモナドと呼ばれている。これからのHaskellプログラミングで、非常に大きな役割を果たすだろう。
IOの世界
今までモナドを自作してきたが、HaskellではIOモナドという非常に重要なモナドがあらかじめ定義されている。なんと、IOモナドは、処理系がモナドを分解して、現実世界に対する副作用に変換できるのだ！
IOモナドとして表現される手続きをmainとして定義すると、処理系がそれを解釈してコンピュータに副作用を発生させる。これにより、Haskellのプログラムは使えるようになる。
main = putStrLn "Hello, world!"
これを実行すれば、あなたのターミナルにはHello, world!と表示されるだろう。神秘的だ…
IOモナドの中身をプログラムが把握することはできないが、Operationalモナドの中身を把握することは可能だ。これは、処理系が現実世界の中身を把握できなくても、IOモナドの中身を把握できるのと似ている。ということは、Operationalモナドを解釈してIOに影響を及ぼす処理系を作れるのではないだろうか？……作れる。
toIO :: Program MyActions a -> IO a toIO (Unit HelloWorld) = putStrLn "Hello, world!" toIO (Unit (PutStrLn str)) = putStrLn str toIO (Unit GetLine) = getLine toIO (Return a) = return a toIO (m :>>= k) = toIO m >>= toIO . k
そう、まさに言語と処理系の関係。Operationalモナドは、一つの手続き型言語を、命令の一覧から自動生成してしまうモナドなのだ。しかも、IOなどの特定の
ここで作ったOperationalモナドは、より洗練された実装がある。実用する際はこちらを使おう。
ここで紹介した以外にも、Haskellの世界には様々なモナドがある。モナドの六つの系統やモナドのすべてを参考に、様々なモナドを使って、そして作ってみてほしい。
まとめ
モナドの六つの系統[Functor x Functor]
モナドは「アクション」を表す抽象的な構造である。モナドは、Haskellにさまざまな概念に対する記述能力をもたらす。
モナドの基礎
return :: a -> m a: 純粋な値をモナドで包む。m >>= f :: m a -> (a -> m b) -> m b: モナドmに包まれた値をfに渡し、その結果として現れたモナドを結合する。- 固有アクション: それぞれのモナドに固有の方法でモナドを生み出す。
- 実行: モナドに包まれた値を、より根源的な形に還元する。
モナド則
モナドに以下の三つの制約を課すことによって、最低限度の記述能力を保証している。
return a >>= k == k a
m >>= return == m
m >>= (\x -> k x >>= h) == (m >>= k) >>= h
より強い制約は、より強い力を生み出す。
モナドの分類
モナドは、以下の6つの系統に分類できる。
隣り合っているものほど相性がよく、近い性質を持つことが多い。
内包系
Identity, Maybe, Either, [], Iterateeなど
値を何らかの形で包みつつ、モナドの性質を付与したもの。失敗する可能性のある計算に使用できるものも多い。ストリームを扱うモナドIterateeは、継続系の性質も併せ持つ。
Nothing :: Maybe a(固有アクション)計算をすべてに終わりにする。これが出現すると、(>>=)は一切意味をなさなくなる。
出力系
主にWriter
値を出力できるという性質を備えたモナド。
tell :: Monoid w => w -> Writer w ()(固有アクション)モナドに値を送り込む。モナドが結合できるという制約から、送る値も結合可能でなければならない。runWriter :: Writer w a -> (a, w)(実行)計算の結果と、書き込まれた値を取り出す。
環境系
主にReader
モナドの中で値を取り出し、自由に使用できるという性質を持つ。
ask :: Reader r r(固有アクション)環境から値を取り出す。runReader :: Reader r a -> r -> a(実行)環境を設定し、その下で行われた計算の結果を求める。環境に持たせる値はどんなものでもよい。
世界系
IO, STM, ST, Q, Freeなど
現実を含む、世界に作用できる特殊なモナド。Haskellにおける、副作用を表現する唯一の方法である。
putStrLn :: String -> IO ()(固有アクション)現実世界の標準出力に文字列を送る。getLine :: IO String(固有アクション)現実世界の標準入力から、一行分の文字列を取り出す。unIO :: IO a -> (State# RealWorld -> (# State# RealWorld, a #))(実行)GHCのIOの中身は、現実世界を受け取り、変更後の現実世界と結果を返す関数である。通常、我々がこの型 を目にすることはない。liftF :: Functor f => f a -> Free f a(固有アクション)すべてのFunctorには、自由モナド(free monad)と呼ばれるモナドが対応する。自由モナドは強力な抽象化、コードの分離を行うことができる*1。singleton :: t a -> Program t a(固有アクション)なんと、この世にはすべてのデータ型にモナドを対応させる仕組みが存在するのだ*2。筆者はこれを最強のモナドの一つだと確信している。
状態系
主にState
モナドの中なら、値を読み込んだり書き込んだりできる。
get :: State s s(固有アクション)現在の状態を読み込む。put :: s -> State s ()(固有アクション)現在の状態を置き換える。runState :: State s a -> s -> (a, s)(実行)初期状態を与えて、結果と変更後の状態を取得する。
継続系のCodensityモナドを使うと、環境系モナドの性質を状態系モナドに変化させることができる。
継続系
Cont, CC, Parser, Codensity, Logicなど
「継続」と呼ばれる、計算の結果を受け取る関数を扱うモナド。表現力が高く、興味深い性質を示すものも多い。
cont :: ((a -> r) -> r) -> Cont r a(固有アクション)継続を受け取る関数からモナドを作る。rの型がわかっているとき、非常に柔軟な処理が可能となる。runCont :: Cont r a -> (a -> r) -> r(実行)継続を渡し、計算の結果を求める。dnew :: CC (Dynvar CC a)(固有アクション)限定継続モナドCCの中で、変更可能な変数*3を具現化する。IOなどの現実世界と関わる処理は一切ない。
ほとんどのモナドはこの継続系の変種として表現できるという面白い特徴を持つ。Logicモナドは継続系でありながら非常に内包系に近い特性を持つ*4。
まとめ
良いプログラムを書くには、これら六系統のモナドをバランス良く使いこなしていくことが大事である。
参考文献
Freeモナドを超えた！？operationalモナドを使ってみよう
限定版IOみたいなモナドを簡単に作れたら、コードが分離できるしテストもしやすくなるのになあ…
数か月前なら、
と返されるだろう。だが今は違う。Freeモナドよりも簡単にモナドを作れるモナド、Operationalモナドがあるのだ。
Freeモナドについて復習しよう。FreeモナドはFunctorを基にMonadを作れる構造であり、Functorで自分自身を包むことによってモナドの力を得ている*2。FunctorそのものはDeriveFunctor拡張を使って簡単に作れる。
{-# LANGUAGE DeriveFunctor #-} import Control.Monad.Free data CharIO a = PutCh Char a | GetCh (Char -> a) | LiftIO (IO a) deriving Functor putCh ch = wrap $ PutCh ch (return ()) getCh = wrap $ GetCh return liftIO = wrap . LiftIO . fmap return
CharIOを標準入出力上で動かす場合は以下のようになる。
type MyIO = Free CharIO runCharIO :: Free CharIO a -> IO a runCharIO (Free (PutCh ch cont)) = putChar ch >> runCharIO cont runCharIO (Free (PutCh cont)) = getChar >>= runCharIO . cont runCharIO (Free (LiftIO m)) = m >>= cont runCharIO (Pure a) = return a
チャーチエンコード(Boehm-Berarducciエンコード？)されたバージョンはより高速に動作する。
import Control.Monad import Control.Monad.Free.Church type MyIO = F CharIO runCharIO :: MyIO a -> IO a runCharIO m_ = runF m_ return w where w (PutCh ch cont) = putChar ch >> cont w (GetCh cont) = getChar ch >>= cont w (LiftIO m) = join m
ここからが本題
ところが、Operationalモナドはより簡単にモナドを構成できる。ここでは、実装の一つであるfree-operationalパッケージを使う。
{-# LANGUAGE GADTs #-} import Control.Monad.Operational.Simple -- 必要なアクションの型を並べる data CharIO x where GetCh :: CharIO Char PutCh :: Char -> CharIO () LiftIO :: IO a -> CharIO a type MyIO = Program CharIO getCh :: Program CharIO Char getCh = singleton GetCh putCh :: Char -> Program CharIO () putCh = singleton . PutCh liftIO :: IO a -> Program CharIO a liftIO = singleton . LiftIO
驚くべきことに、Functorすら使わずにモナドを作れる。しかも、他のモナドに変換するのも非常に簡単だ。
runCharIO :: MyIO a -> IO a runCharIO = interpret advent where advent GetCh = getChar advent (PutCh ch) = putChar ch advent (LiftIO m) = m
なぜこんなことができるのか――そこには、Coyoneda*3と呼ばれるFunctorの力が隠されていた。
{-# LANGUAGE GADTs, Rank2Types #-} data Coyoneda t x where Coyoneda :: t r -> (r -> a) -> Coyoneda t a instance Functor (Coyoneda t) where fmap f (Coyoneda t g) = Coyoneda t (f . g) liftCoyoneda :: t a -> Coyoneda t a liftCoyoneda t = Coyoneda t id
なんとこのCoyonedaは、ただのデータ型からFunctorを生み出せるのだ！！
Operationalモナド(上の例ではProgram)は、本質的には以下のようになっている。
type Program t = Free (Coyoneda t)
何もないところからFunctorが作れて、FunctorがあればMonadが作れる――したがって何もないところからMonadを作れる、という理屈だ。
それは、元の構造をアクションに変形するsingleton関数によって表現できる。
-- liftCoyoneda :: t a -> Yoneda t a -- liftF :: Functor f => f a -> Free f a singleton :: t a -> Program t a singleton = liftF . liftCoyoneda
あとはinterpretを定義すれば、adventのような関数を与えるだけで動かせる。
interpret :: Monad m => (forall x. instr x -> m x) -> Program instr a -> m a interpret eval (Free (Coyoneda t f)) = eval t >>= interpret eval . f interpret _ (Pure a) = return a
欲しいアクションの型を並べれば、freeなモナドが手に入る。
じゃあいつ使うか？
今でしょ！
追記: minioperationalという、シンプルかつ高速なOperationalモナドの実装を作ったのでぜひ使ってみてほしい。
Indexed Monadの世界
もっと、モナドの力を引き出したくはないか？
え？アクションの前後で型を変えたい？いやいやいや、モナドは自己関手の圏上の単なるモノイドだよ、そんなことができ…る…！？えっ、できるの…マジで…？
できる。そう、Haskellならね。
{-# LANGUAGE QuasiQuotes #-} import Control.Monad.Indexed.State import Control.Monad.Indexed import Language.Haskell.IndexedDo hoge :: IxState Int [Int] () hoge = [ido|do imodify (*10) imodify show imodify reverse imodify (++"123") imodify $ map fromEnum |]
*ghci> runIxState hoge 42
((),[48,50,52,49,50,51])
明らかに、計算の途中で型が変わっている！ 勿論、型さえ合えばループや条件分岐を使うこともできる。
この何やら恐ろしいモナドのようなものが一体どういう仕組みになっているのか、じっくり調べてみよう。
IxStateの定義はこうだ。
newtype IxState i j a = IxState { runIxState :: i -> (a, j) }
Stateモナドのような形をしているが、これは状態の型が変わるため、Monadのインスタンスにはできない。ならば…より多くの制約を持ったモナドを作ればよい。
class IxMonad m where -- indexedパッケージで提供されているクラスとは多少異なるので注意 ireturn :: a -> m i i a ibind :: (a -> m j k b) -> m i j a -> m i k b
このiやjといったパラメータ(添字)によって、アクションが正しく合成されるということが保証できる。これがIndexed monadである。
すると、IxStateをそのインスタンスにできる。
instance IxMonad IxState where ireturn a = IxState $ \s -> (a, s) ibind f m = IxState $ \s -> let (a,s') = runIxState m s in runIxState (f a) s'
しかし、足りないものがある。そう…do記法だ。Indexed monadの力をフルに使うために、indexed-do-notationというパッケージを作った。これは、普通のdo記法とまったく同じようにindexed monadを扱うことができる。使うには、普通のdo記法を[ido|…|]で包めばよい(QuasiQuotes拡張を有効にする必要がある)。
こうして我々は、モナドを超えるモナド、インデックスド・モナドを手に入れたのだ。
Free indexed monad
モナドに対してFreeモナドがあるように、インデックス付きモナドにもインデックス付きFreeモナドがある。早速作ってみよう。
{-# LANGUAGE GADTs #-} data IxFree f i j x where Pure a :: a -> IxFree i i a Free :: f i j (IxFree f j k a) -> IxFree f i k a
パラメータが増えた点を除けば普通のFreeモナドと変わらない。それは実装も同じだ。
instance IxFunctor f => IxMonad (IxFree f) where ireturn = Pure ibind k (Pure a) = k a ibind k (Free f) = Free $ imap (ibind k) f
IxFunctorはFunctorのindexed版。fmapの代わりに、添字の関係を保存しつつ中身だけを変えるimapが定義されている。
class IxFunctor f where imap :: (a -> b) -> f i j a -> f i j b
そして、IxFreeは、IxFunctorによってIxMonadを生成できるのだ。
このIxFreeを使って、Coqのタクティクスのようなものを作ってみよう。ゴールの書き換えが添え字の変化に対応している。
{-# LANGUAGE QuasiQuotes, GADTs #-} import Control.Monad.Indexed -- indexed import Control.Monad.Indexed.Free -- indexed-free import Language.Haskell.IndexedDo -- indexed-do-notation import Control.Applicative import Data.Void -- void data Proof i j x where Intro :: (p -> a) -> Proof (p -> q) q a Apply :: (p -> q) -> a -> Proof q p a instance IxFunctor Proof where imap f (Intro g) = Intro (f . g) imap f (Apply e a) = Apply e (f a) intro :: IxFree Proof (a -> b) b a intro = Free $ Intro ireturn apply :: (a -> b) -> IxFree Proof b a () apply p = Free $ Apply p (ireturn ()) exact :: a -> IxFree Proof a b () exact p = Free $ Apply (const p) (ireturn ())
以下のように証明が書ける。当然、証明が間違っていると型エラーになる(ここ重要)。
ex0 :: IxFree Proof ((a -> b) -> (b -> c) -> a -> c) () () ex0 = [ido|do ab <- intro bc <- intro a <- intro apply bc apply ab exact a |] ex1 :: IxFree Proof ((Either a b -> Void) -> (a -> Void, b -> Void)) () () ex1 = [ido|do e <- intro exact (e . Left, e . Right) |] ex1' :: IxFree Proof ((a -> Void, b -> Void) -> (Either a b -> Void)) () () ex1' = [ido|do (ha, hb) <- intro e <- intro case e of Left a -> exact $ ha a Right b -> exact $ hb b |]
驚くべきことに、この証明から実際のHaskellのプログラムを作ることも可能だ。
runProof :: Show r => IxFree Proof a b r -> a runProof (Pure r) = error $ "Unexpected end of proof" ++ show r runProof (Free (Intro f)) = runProof . f runProof (Free (Apply a cont)) = a (runProof cont)
*ghci> :type runProof ex0
runProof ex0 :: (a -> b) -> (b -> c) -> a -> c
*ghci> runProof ex0 (+11) (*3) 11
66
いやはや、indexed monad恐るべし…
オレはようやくのぼりはじめたばかりだからな このはてしなく遠いモナド坂をよ…
