About Me

• κeen
• @blackenedgold
• Github: KeenS
• GitLab: blackenedgold
• Idein Inc.のエンジニア
• Lisp, ML, Rust, Shell Scriptあたりを書きます

今日の話

• Effectのハンドラを自分で書く

Effectsって？

• Idrisの標準添付ライブラリ
• Algebraic Effectの実装ライブラリ
  • Eff言語のEffectを参考に設計したらしい
• IOとかRandomとかStateとか色々あるよ

使ってみよう

Step 1

.ipkgに effects を足す

package hoge

version = "0.1.0"

-- ..

-- これ
pkgs = effects

使ってみよう

Step 2

Effectsをインポート

module Main

import Effects
import Effect.StdIO

使ってみよう

Step 3

Effectを使って好きなプログラムを書こう

hello : Eff () [STDIO]
hello = do
   putStr "what's your name: "
   name <- getStr
   putStr "what title do you prefer: "
   title <- getStr
   putStrLn $ "Hello " ++ name ++ title
   pure ()

使ってみよう

Step 3

STDIO Effectを走らせると IO モナドになるよ

main : IO ()
main = run hello

$ ./main
what's your name: keen
what title do you prefer: -san
Hello keen-san

Effect便利

• 複数のEffectを1つの do 記法で書けるよ

game : Eff () [STDIO, RND]
game = do
  -- set the random seed
  -- RND
  srand 111
  -- generate an random number
  n <- rndInt 0 100
  -- enter the main loop
  -- IO
  mainLoop n

Effectの中身

• Effect = 返り値 * リソース * リソースの更新
• EFFECT = パラメータ * Effect

Effect : Type
Effect = (x : Type) -> Type -> (x -> Type) -> Type

data EFFECT : Type where
     MkEff : Type -> Effect -> EFFECT

Effectたち

State

data State : Effect where
  Get :      sig State a  a
  Put : b -> sig State () a b

STATE : Type -> EFFECT
STATE t = MkEff t State

get : Eff x [STATE x]
get = call $ Get

put : x -> Eff () [STATE x]
put val = call $ Put val

Effectたち

StdIO

data StdIO : Effect where
     PutStr : String -> sig StdIO ()
     GetStr : sig StdIO String
     PutCh : Char -> sig StdIO ()
     GetCh : sig StdIO Char

STDIO : EFFECT
STDIO = MkEff () StdIO

-- putStr, putStrLnなどなど

Effect文脈

• hello についてた Eff () [STDIO] の話
• 複数の Effect をまとめた「どんな種類のEffectが起きるか」の文脈。
• Eff は元を辿ると長い EffM
• EffM = モナドっぽいの * 返り値 * Effect文脈 * 文脈更新関数

data EffM : (m : Type -> Type) -> (x : Type)
            -> (es : List EFFECT)
            -> (ce : x -> List EFFECT) -> Type where
  -- ...

Effect文脈

• Effectの更新をしないならもう少し簡単にできる
• さらにモナドっぽいのは一般化して使うので省略してよさそう

Eff : (x : Type) -> (es : List EFFECT) -> Type
Eff x es = {m : Type -> Type} -> EffM m x es (\v => es)

EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT) -> Type
EffT m x es = EffM m x es (\v => es)

Effect文脈

• 重要なのは EffM はモナドトランスフォーマじゃ ない 点
  • Effectの更新が入る
  • Extensible Effectとはそこが違う？
• Idrisの do 記法は (>>=) の糖衣構文なのでモナドじゃなくても使える

(>>=)   : EffM m a xs xs' ->
          ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''
(>>=) = EBind

run について

• モナドっぽいものはモナドじゃない
  • pure さえあればいい
• m を Identity にとればただの型にもなる
  • IO とかのため一般化
• あと本来はEffectの初期値も必要

run : Applicative m =>
      (prog : EffM m a xs xs') -> {default MkDefaultEnv env : Env m xs} ->
      m a
runWith : (a -> m a) -> Env m xs -> EffM m a xs xs' -> m a
runPure : (prog : EffM Basics.id a xs xs') ->
          {default MkDefaultEnv env : Env Basics.id xs} -> a

小まとめ

• Effect単体は Effect
• それらをまとめた文脈が Eff a [EFFECT]
• Eff を run するとモナドっぽいものが出てくる

ハンドラの話

• 所望の Effect に Handler を実装すると run できるようになる
• そのときに実装する型で run のあとに取り出せる型が変わる

interface Handler (e : Effect) (m : Type -> Type) where
  handle : (r : res) -> (eff : e t res resk) ->
           (k : ((x : t) -> resk x -> m a)) -> m a

ハンドラの例

• この例だと StdIO を run すると IO モナドが出てくることが分かる

implementation Handler StdIO IO where
    handle () (PutStr s) k = do putStr s; k () ()
    handle () GetStr     k = do x <- getLine; k x ()
    handle () (PutCh c)  k = do putChar c; k () ()
    handle () GetCh      k = do x <- getChar; k x ()

ハンドラを書いてみよう

• IO だと扱いづらいよね
• 入力を文字列リストで与えて出力を文字列リストで取り出せるpureなハンドラを書いてみよう
• 以下の型の関数を書くのが目的

runToStr : List String -> Eff ret [STDIO] -> (ret, List String, List String)
runToStr input eff = ?unimplemented

型定義

• 入力と出力でそれぞれ State を使うよ
  • 外側が出力、内側が入力
  • タプルにして1つのステートにした方がよかったかも？
• run するとこの型が出てくるよ

StringIO : Type -> Type
StringIO a = StateT (List String) (State (List String)) a

操作関数

• 入力は色々面倒くさい

read : StringIO String
read = do
    ss <- lift get
    let hd = fromMaybe "" $ head' ss
    let tl = fromMaybe [] $ tail' ss
    lift $ put tl
    pure hd

write : String -> StringIO ()
write s = modify (\ss => the (List String) (s::ss))

ハンドラ

• インターフェースの実装には型エイリアスは書けないみたい？
• StdIO を run すると StateT (List String) (StateT (List String) Identity) が出てくるよ！

implementation Handler StdIO (StateT (List String) (StateT (List String) Identity)) where
    handle () (PutStr s) k = do write s; k () ()
    handle () GetStr     k = do s <- read; k s ()
    handle () (PutCh c)  k = do write $ singleton c; k () ()
    handle () GetCh      k = (k ' ' ())

runToStr

• ハンドルしよう
• run が勝手に StringIO を推論してることに注目

runToStr : List String -> Eff ret [STDIO] -> (ret, List String, List String)
runToStr input eff = let
   writer = run eff
   reader = runStateT writer (the (List String) [])
   ((ret, output), input) = runState reader input
   in (ret,  output, input)

実行

• テストするときとかは print せずに結果を比較しようね

main : IO ()
main = printLn $ runToStr ["keen", "-san"] hello

$ ./main
((), (["Hello keen-san\n", "what title do you prefer: ", "what's your name: "], []))

まとめ

• Effectsは Eff 、 Effect 、 run をおさえよう
• Effect の Handler は上書きできるよ
• run した結果は Handler が実装されてる型だよ

参考文献

• The Effects Tutorial
• Edwin Brady. 2013. Programming and reasoning with algebraic effects and dependent types. SIGPLAN Not. 48, 9 (September 2013)