付録アイデア。Selectionモナド

[Seasawher]

三目並べの評価処理もこれで書けるという話を聞いた

[Seasawher]

Selection モナドは、雑に言うと

「候補 α の中から、結果評価 α → r を見て、ひとつの α を選ぶ」

というモナドです。

型はこうです。

def Selection (r α : Type) : Type :=
(α → r) → α

r は評価値、報酬、勝敗、真偽値などです。

基本実装

def Selection (r α : Type) : Type :=
(α → r) → α
namespace Selection
def pure {r α : Type} (x : α) : Selection r α :=
fun _ => x
def bind {r α β : Type}
(e : Selection r α)
(f : α → Selection r β) : Selection r β :=
fun k =>
let x := e (fun x => k (f x k))
f x k
instance {r : Type} : Pure (Selection r) where
pure := pure
instance {r : Type} : Bind (Selection r) where
bind := bind
instance {r : Type} : Monad (Selection r) where
pure := pure
bind := bind
end Selection

ポイントは bind です。

let x := e (fun x => k (f x k))
f x k

これは、

1. まず x : α を選ぶ
2. ただし x の良さは「その後 f x で最終的に何が選ばれるか」で評価する
3. その x を使って次の選択に進む

という意味です。

典型例：最大値を選ぶ

有限な候補リストから、スコアが最大のものを選ぶ Selection を作れます。

def argmax [Ord r] (xs : List α) (default : α) : Selection r α :=
fun score =>
xs.foldl
(fun best x =>
match compare (score x) (score best) with
| .gt => x
| _ => best)
default

例：

#eval
(argmax [1, 2, 3, 4, 5] 0) (fun x => -(x - 3) * (x - 3))

これは 3 を選びます。

do 記法で「複数手の最適化」ができる

たとえば x と y を選んで、最終スコアを最大化したいとします。

def chooseNat (xs : List Nat) (default : Nat) : Selection Int Nat :=
argmax xs default
def choice : Selection Int (Nat × Nat) := do
let x ← chooseNat [0, 1, 2, 3, 4, 5] 0
let y ← chooseNat [0, 1, 2, 3, 4, 5] 0
pure (x, y)

評価関数を与えると、Selection が (x, y) を選びます。

#eval choice (fun (x, y) =>

• ((x : Int) - 2)^2 - ((y : Int) - 4)^2)

期待される選択は (2, 4) です。

何ができるか

Selection モナドでできることは主にこれです。

1. 最適化問題を書く

Selection Score α

は「α 型の候補を、Score によって選ぶ計算」です。

argmax を使えば最大化、argmin を使えば最小化になります。

2. ゲーム木探索を書く

r = Bool にすると、

Selection Bool Move

は「勝てるような手を選ぶ」計算になります。

複数手先まで読むとき、bind が「後続の選択を考慮して現在の手を選ぶ」ので、ゲーム木探索っぽくなります。

3. バックトラックとは違う探索を書く

List モナドは「全部の可能性を列挙する」モナドです。

List α

一方 Selection モナドは、

(α → r) → α

なので、「全部列挙」ではなく「評価関数を見て代表元を選ぶ」モナドです。

つまり、

List : 全候補を返す
Option : 成功した候補を返す
Selection : 評価に基づいて候補を選ぶ

という感じです。

直感

Selection モナドは「未来の評価関数を受け取って、現在の選択を決める」モナドです。

そのため、普通の State モナドや List モナドよりも「ゲーム」「探索」「最適化」に近いです。

ただし、実用的には Selection r α だけだと候補集合を内包していないので、たいていは

argmax : List α → α → Selection r α

のように、有限候補を別途与える形で使います。