もっと、モナドの力を引き出したくはないか？

え？アクションの前後で型を変えたい？いやいやいや、モナドは自己関手の圏上の単なるモノイドだよ、そんなことができ…る…！？えっ、できるの…マジで…？

できる。そう、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恐るべし…

オレはようやくのぼりはじめたばかりだからな　このはてしなく遠いモナド坂をよ…

モナドとわたしとコモナド

Indexed Monadの世界

Free indexed monad