IdrisでStateモナド

本記事では、関数型言語に触れているよくでてくる モナド について書きます。

Stateモナドを数学的に実装する

Idrisでやってみた。
Control.Monad.Stateにもある。そこではモナド変換子として実装されている。

module MyState

%default total
-- %language ElabReflection
-- %hide return

-- Stateモナド
record State (stateType : Type) (a : Type) where
  constructor ST
  runState : stateType -> (a, stateType)

implementation Functor (State stateType) where
  map f (ST g) = ?rhs1

implementation Applicative (State stateType) where
  pure x = ST $ \s => (x, s)
  (ST f) <*> (ST a) = ?rhs2

implementation Monad (State stateType) where
  m >>= k = ST $ \s =>
              let (x, s0) = runState m s
              in runState (k x) s0

-- プレリュードでやってる
-- return : Monad m => a -> m a
-- return = pure
get : State x x
get = ST $ \s => (s, s)
put : s -> State s ()
put s = ST $ const ((), s)
-- -------------------------


-- アキュムレータ
-- xを取り、stateに加え、更新したstateを出力
accumulator : Int -> State Int Int
accumulator x = do
  state <- get
  let y = state + x
  put y
  return y
-- 実行
-- bind(>>=)は左から右へ進む
-- > runState ((accumulator 3) >>= accumulator) 4
-- (14, 14) : (Int, Int)

-- アキュムレータ2
accumulator2 : List Int -> State Int (List Int)
accumulator2 [] = return []
accumulator2 (x::_) = do
  state <- get
  let y = state + x
  put y
  return [y]
partial -- ↓どこが全域でないか分からないが……
multiple : State Int (List Int)
multiple = do
  (a::_) <- accumulator2 [1] -- [2]が返る
  (b::_) <- accumulator2 [1] -- [3]が返る、参照透過じゃない！（と、見せかけている）
  (c::_) <- accumulator2 [2]
  (d::_) <- accumulator2 [3]
  (e::_) <- accumulator2 [0]
  (f::_) <- accumulator2 [-1]
  return [a, b, c, d, e, f]
-- 実行
-- runStateの中でだけ、状態が保持される
-- > runState multiple 1
-- ([2, 3, 5, 8, 8, 7], 7) : (List Int, Int)

元記事のメイン内容だけど、随伴からStateモナドが作られるのですね。
知らなかった。
自分もそこまでやるかは分からない。