Selectionモナド入門

Selectionモナドは2010年にEscardóとOlivaによって["Selection Functions, Bar Recursion, and Backward Induction"](https://www.cs.bham.ac.uk/~mhe/papers/selection-escardo-oliva.pdf)で紹介されました。継続モナドによく似ていますが少し違っており、ゲーム理論の解法の一つである後ろ向き帰納法や探索アルゴリズムなど色んなパターンを取り扱うことができます。`transformers`というよく知られたライブラリでは[`Control.Monad.Trans.Select`](http://hackage.haskell.org/package/transformers-0.5.6.2/docs/Control-Monad-Trans-Select.html)というモジュールとして実装が提供されています。

Selectionモナドの型を見てみましょう。

```hs
newtype Select r a = Select { runSelect :: (a -> r) -> a }
```

一方、継続モナドの型はこちらです。

```hs
newtype Cont r a = Cont { runCont :: (a -> r) -> r }
```

どちらも`a`を取って`r`を返す関数を引数に取る高階関数になっていますがその返り値が`a`なのか`r`なのかの違いがあります。実はSelectionモナドが与えられれば継続モナドを作ることができます。すなわちSelectionモナドから継続モナドへの自然変換を

```hs
selectToCont :: Select r a -> Cont r a
selectToCont (Select e) = Cont $ \p -> p (e p)
```

のように実装することができます。

この記事ではSelectionモナドを使ったいくつかの例と、`Monad`としての実装を見ていきたいと思います。

## Selection関数
それではSelectionモナドの具体例を見ていきましょう。この章では["What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common"](http://www.cs.bham.ac.uk/~mhe/papers/msfp2010/)を参考に手短に要約しながら解説していきたいと思います。

まずはモナドとしてではなく単なる関数（Selection関数）としての性質を見ていきたいと思います。そのため

```hs
type J r x = (x -> r) -> x
```

という形でSelection関数に`J`という名前をつけておきます。

例えばある実数値関数の最大値を与える点を探す問題

```math
\underset{x}{\rm argmax}\ f(x)
```

を考えると${\rm argmax}$は$x$を受け取って実数を帰す関数$f$を受け取って$x$の値を返す関数と考えることができ、Selection関数と思うことができます。これを実装すると

```hs
argmax :: [x] -> J Int x
argmax []       p = undefined
argmax [x]      p = x
argmax (x:y:zs) p = if p x < p y
                      then argmax (y:zs) p
                      else argmax (x:zs) p

argmin :: [x] -> J Int x
argmin xs p = argmax xs (\x -> - p x)
```

のようになり（あまり効率的な実装ではありませんが...）、評価関数の符号を入れ替えることで`argmin`を実装することもできました。

他にも平均値の定理より実数関数$p$が与えられると

```math
\int^1_0 p(x)dx = p(a)
```

を満たすような$a$が存在しますが、$p$が与えられたときにこの$a$を返すような操作はSelection関数と思うことができます。ただしこの関数を具体的に実装することは難しそうです。

また単純な検索関数

```hs
find :: [x] -> J Bool x
find []     p = undefined
find [x]    p = x
find (x:xs) p = if p x then x else find xs p
```

もSelection関数を使って表すことができます。これを使えば

```hs
-- | 継続のパターン
type K r x = (x -> r) -> r

-- | Selection関数から継続のパターンへの変換
overline :: J r x -> K r x
overline e = \p -> p (e p)

forsome, forevery :: [x] -> K Bool x
forsome       = overline . find
forevery xs p = not (forsome xs (not . p))
```

というように、リストのある値が条件を満たすかを調べる関数`forsome`とリストの全ての値が条件を満たすかを調べる関数`forevery`のような関数を実装することができます。HaskellのPreludeで提供されている`any`や`all`と大体同じものです。

さらに2変数の実数値関数$q(x, y)$があった時に上記2つを組み合わせて

```math
\underset{x}{\rm argmax}\int^1_0q(x, y)dy
```

のような式を考えて適切な$x, y$を求める操作を考えることが出来ると思います。これは$argmax$と平均値の定理という２つのSelection関数の積を取るような操作だと考えることができるでしょう。この操作を具体的に実装してみましょう。

```hs
-- | ２つのSelection関数の積
times :: J r x -> (x -> J r y) -> J r (x, y)
times e0 e1 p = (a0, a1)
  where
    a0 = e0 (\x0 -> overline (e1 x0) (\x1 -> p (x0, x1)))
    a1 = e1 a0 (\x1 -> p (a0, x1))
```

`times`を眺めると`(x, y)`を評価する関数`p`から巧妙に`x`と`y`それぞれを評価する関数を作り出しているのが分かると思います。この実装を利用して、同じ型にはなってしまいますがn個のSelection関数の積を求める関数を実装してみましょう。

```hs
otimes :: J r x -> (x -> J r [x]) -> J r [x]
otimes e0 e1 p = a0 : a1
  where
    a0 = e0 (\x0 -> overline (e1 x0) (\x1 -> p (x0 : x1)))
    a1 = e1 a0 (\x1 -> p (a0 : x1))
```

`otimes`は`x`のSelection関数と`x`を受け取って`[x]`のSelection関数を返す関数を組み合わせて`[x]`のSelection関数で、一つ前のSelection関数の結果に依存しながらSelection関数の積を計算していくことができています。もっと発展させて一つ前まで全ての結果に依存しながらSelection関数の積を計算していく関数を定義してみましょう。

```hs
bigotimes :: [[x] -> J r x] -> J r [x]
bigotimes [] = \p -> []
bigotimes (e:es) = e [] `otimes` (\x -> bigotimes [\xs -> d (x:xs) | d <- es])
```

実はこの`bigotimes`関数は一つ前までの値への依存を無視すると`[J r x] -> J r [x]`という型になっており、`J r`すなわち`Select r`がモナドであること知っていれば[`sequence`関数](http://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Traversable.html#v:sequence)に対応していることが分かるかと思います。`bitotimes`はSelectionモナドを語る時には欠かせない重要な関数です。

### エイト・クイーン
実際にSelection関数を使って問題を解いてみましょう。ここで解いてみる問題は[エイト・クイーン](https://ja.wikipedia.org/wiki/%E3%82%A8%E3%82%A4%E3%83%88%E3%83%BB%E3%82%AF%E3%82%A4%E3%83%BC%E3%83%B3)です。
<img src="https://qiita-image-store.s3.amazonaws.com/0/17134/57379977-16ba-0a2a-dad7-93e29869f996.png" width=200 />
画像出典: [エイト・クイーン - Wikipedia](https://ja.wikipedia.org/wiki/%E3%82%A8%E3%82%A4%E3%83%88%E3%83%BB%E3%82%AF%E3%82%A4%E3%83%BC%E3%83%B3)

チェスにおいてクイーンは縦・横・斜めの全ての方向の任意のマスに移動できるコマです。このクイーンを８個、互いに互いのコマを1手で取ることができないようにチェス盤に配置することが出来るかと言うのがエイト・クイーンという問題です。この問題は解くことができて解が全部で12個あることが知られています。

```hs
-- | n個のクイーンを配置することを考える
n = 8

-- | コマの縦もしくは横の位置
--   横から何列目か、上から何行目かをIntで表す
type Coord = Int

-- | コマの座標(x, y)
type Pos = (Coord, Coord)

-- | ２つの座標が衝突していないことを検証する
attacks :: Pos -> Pos -> Bool
attacks (x, y) (a, b) =
     x == a                     -- 縦がかぶっていないか
  || y == b                     -- 横がかぶっていないか
  || abs (x - a) == abs (y - b) -- 斜めがかぶっていないか

-- | 全ての座標が衝突していないことを検証する
valid :: [Pos] -> Bool
valid []       = True
valid (u : vs) = not (any (\v -> attacks u v) vs) && valid vs
```

まずはエイト・クイーンに固有な関数を実装していきました。次にこれまでに定義したSelection関数に関する関数を組み合わせてエイト・クイーンを解いてみましょう。

```hs
-- | 与えられた配置が衝突しているかどうかを返す
p :: [Coord] -> Bool
p ms = valid (zip ms [0..(n-1)])

-- | 既存の配置が与えられた時の新しいコマのSelection関数のリスト
epsilons :: [[Coord] -> J Bool Coord]
epsilons = replicate n epsilon
  where
    epsilon hs = find ([0..(n-1)] \\ hs)

-- | 最適なコマの配置
optimalPlay :: [Coord]
optimalPlay = bigotimes epsilons p

main :: IO ()
main = print optimalPlay
```

実行してみると

```hs
[0,4,7,5,2,6,1,3]
```

となりエイト・クイーンを解くことができました :clap: 

Repl.it上で動作するコードはこちら
<https://repl.it/@lotz84/GivingBewitchedCodec>

### 三目並べ
三目並べは２人のプレイヤーが3×3マスの盤面に○と☓を交互に書いていき、先に縦・横・斜めに同じ記号が揃えられた方の勝ちというゲームです。
<img src="https://qiita-image-store.s3.amazonaws.com/0/17134/a33f3dfb-aa68-ce54-cf4a-eeb8df1b8979.png" width=400 />
画像出典: Googleで「[三目並べ](https://www.google.com/search?q=三目並べ)」と検索した結果出てくるゲームより

三目並べは先手・後手ともに最善を尽くすと必ず引き分けとなることが知られていますが、エイト・クイーンのときと同じようにSelection関数を使って最善の手を計算し、引き分けになることを実際計算してみましょう。

```hs
-- | ２人のプレイヤー
data Player = X | O

-- | 評価関数の値
-- 以下のような値を取る
-- Xが勝ち: 1
-- Oが勝ち: -1
-- 引き分け: 0
type Result = Int

-- | 盤面上の位置
--  0 | 1 | 2
-- -----------
--  3 | 4 | 5
-- -----------
--  6 | 7 | 8
type Pos = Int

-- | XとOが行ってきた手番の組
type Board = ([Pos], [Pos])

-- | 手番に勝ちパターンが含まれているか
--   引数の手番のリストはソートされていることを仮定している
wins :: [Pos] -> Bool
wins ms = any (`isSubsequenceOf` ms)
  [[0,1,2],[3,4,5],[6,7,8],[0,3,6]
  ,[1,4,7],[2,5,8],[0,4,8],[2,4,6]]

-- | 手番を評価する
value :: Board -> Result
value (x,o)
  | wins x = 1
  | wins o = -1
  | otherwise = 0

-- | ソートされたリストに要素を追加する
insert :: Ord x => x -> [x] -> [x]
insert x [] = [x]
insert x (vs@(y : ys))
  | x == y = vs
  | x < y = x : vs
  | otherwise = y : insert x ys

-- | 勝敗が決まるか手番がなくなるまでゲームを進行する
outcome :: Player -> [Pos] -> Board -> Board
outcome whoever [] board = board
outcome X (m : ms) (x, o) =
  if wins o then (x, o)
  else outcome O ms (insert m x, o)
outcome O (m : ms) (x, o) =
  if wins x then (x, o)
  else outcome X ms (x, insert m o)
```

まずは三目並べに固有な関数をざっと実装してみました。次にSelectionに関する関数を組み合わせて、今度は三目並べを解いてみましょう。

```hs
-- | 手番のリストから結果を返す
p :: [Pos] -> Result
p ms = value (outcome X ms ([],[]))

-- | これまでの手番から次の最適な手番を返す関数のリスト
--   偶数番目はXにとって最善な手を、
--   奇数番目はOにとって最善な手を計算していることに注意
epsilons :: [[Pos] -> J Result Pos]
epsilons = take 9 all
  where
    all = epsilonX : epsilonO : all
    epsilonX h = argmax ([0..8] \\ h)
    epsilonO h = argmin ([0..8] \\ h)

-- | 最善な手番
optimalPlay :: [Pos]
optimalPlay = bigotimes epsilons p

-- | 最善な手番の結果
optimalOutcome :: Result
optimalOutcome = p optimalPlay


main :: IO ()
main = do
  putStrLn $ "最善な手番: " ++ show optimalPlay
  putStrLn $ "最善な手番の結果: " ++ show optimalOutcome
```

実行してみると

```hs
最善な手番: [0,4,1,2,6,3,5,7,8]
最善な手番の結果: 0
```

となり最善な手番の結果、引き分けとなることがわかりました。

Repl.it上で動作するコードはこちら
<https://repl.it/@lotz84/AdorableMediumTelephone>

ちなみにこの計算、膨大なゲームの展開を計算していくため非常に時間がかかります。ローカルのPCで実行したときは結果が出るのに約1分20秒かかりました（Repl.it上だと終わりません…）。しかし重要なのはエイト・クイーンも三目並べも同じパターンを使って解けているということです。同じパターンを使って書けるということは抽象化の可能性を秘めており、本質的な構造が裏に隠されているはずです。（計算時間に関しても実装の工夫で改善の余地はありそうです）

## Selectionモナド
実は（表題にもある通り）Selection関数はモナドのインスタンスにすることができます。

```hs
newtype Select r a = Select { runSelect :: (a -> r) -> a }
```

まずは`Functor`のインスタンスを定義してみましょう。

```hs
instance Functor (Select r) where
  fmap f (Select g) = Select $ \p ->
    let p' = (. f) p
     in f (g p')
```

難解に見えますが一つずつ型を見ていきましょう。

```hs
f        :: a -> b
(.)      :: (b -> r) -> (a -> b) -> a -> r
(. f)    :: (b -> r) -> a -> r
p        :: b -> r
p'       :: a -> r
g        :: (a -> r) -> a
f (g p') :: b
```

合成関数演算子`(.)`を使って`a -> b`を`(b -> r) -> a -> r`に置き換えてるのがポイントですね。次に`Applicative`のインスタンスを定義してみましょう。

```hs
instance Applicative (Select r) where
  pure a = Select $ \_ -> a
  Select gf <*> Select gx = Select $ \p -> do
    let h f = f (gx (p . f))
        f   = gf (p . h)
     in h f
```

また一つずつ型を見ていくと、

```hs
gf         :: ((a -> b) -> r) -> (a -> b)
gx         :: (a -> r) -> a
p          :: b -> r
p . f      :: a -> r
gx (p . f) :: a
h          :: (a -> b) -> b
p . h      :: (a -> b) -> r
f          :: a -> b
```

このようにうまく組み合わせることで`b`の値を計算しています。最後に`Monad`のインスタンスを定義してみましょう。

```hs
instance Monad (Select r) where
  Select g >>= f = Select $ \p -> do
    let h x = runSelect (f x) p
        y   = g (p . h)
      in h y
```

これもまた一つずつ型を見ていくと、

```hs
g :: (a -> r) -> a
f :: a -> Select r b
p :: b -> r
h :: a -> b
p . h :: a -> r
y :: a
```

となりうまく`b`の値が計算できていることが分かるかと思います。

最後に実装した`Select`モナドを使って前章で見た`bitotimes`もう一度実装してみましょう。

```hs
bigotimes :: [[x] -> Select r x] -> Select r [x]
bigotimes [] = pure []
bigotimes (e:es) = do
  x  <- e []
  xs <- bigotimes es
  pure (x:xs)
```

これだけです！`overline`も`otimes`も必要なくモナドを使うと`bigotimes`をスッキリと実装することができました。

参考までにSelectionモナドを使ったバージョンのエイト・クイーンのプログラムをこちらに載せておきました。
https://repl.it/@lotz84/EuphoricChocolateTaskscheduling

ちなみにここで紹介した`Select`モナドは`transformers`ライブラリの[`Control.Monad.Trans.Select`](http://hackage.haskell.org/package/transformers-0.5.6.2/docs/Control-Monad-Trans-Select.html)で提供されています。Selectionモナドのトランスフォーマー版である`SelectT`もあります。

## まとめ
Selectionモナドの存在は2019/3/30に新宿で行われた[Gordon Plotkin先生に学ぶAlgebraic Effect](https://connpass.com/event/125885/)でPlotkin先生に紹介されて初めて知りました。この記事で紹介した例だけでなく証明論への応用[^1]だったり、計算機科学版のチコノフの定理を応用して`(Int -> Bool) -> r`のような型を持つ関数の`Eq`インスタンスを定義できたり[^2]Selection関数を尤度関数と絡めることで機械学習に応用できる可能性も秘めているようで、まだまだ面白い話はたくさんありそうです。Selectionモナドこれから流行るといいですね！

[^1]: [What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common](http://www.cs.bham.ac.uk/~mhe/papers/msfp2010/)
[^2]: [Seemingly impossible functional programs](http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/)