読者です 読者をやめる 読者になる 読者になる
ようこそ。睡眠不足なプログラマのチラ裏です。

Observableコンピューテーション式はモナド則を満たしているか否か。

プログラミング F#2.0 F# Rx コンピューテーション式 Haskell モナド

前回のエントリ「F#でRxる。よく訓練されたF#erはコンピューテーション式をつくる。」で紹介いたしました、
Observableコンピューテーション式について補足します。モナド則を満たしているか否かについてです。


Haskellにおいて、モナドモナド則を満たしているとき、

1. (return x) >>= f == f x
 
2. m >>= return == m
 
3. (m >>= f) >>= g == m >>= (\x -> f x >>= g)

以上の三つの条件に満足しています。



モナドのすべてによると、最初の規則は return が >>=*1 に関して左単位元に なっていることを要請していて、
二番目の規則は return が >>= に関して右単位元になっていることを要請してる。 最後の規則は >>= に関する一種の結合法則とのことです。
これを初めて読んだときはさっぱりわかりませんでした。今も確信を持ってわかったとは言いきれませんが、まぁ、なんとなく雰囲気はつかんでいるつもりです。



Observableのコンピューテーション式では、どうでしょうか。

namespace FSharp.Rx.UT

open System

module Tests = 
  open System.Reactive 
  open NUnit.Framework
  open FsUnit
  open FSharp
  open FSharp.Rx
      
  [<TestFixture>]
  type ``monad soku `` () =
    [<Test>] 
    // モナド則1: return x >>= f == f x
    // return された値を保持するための変数(というか継続)は、なくしてしまうことができますよの規則
    // モナドで計算を繋ぐにしろ、もともと繋がっている計算をモナドでくるんでも一緒だね
    member test.``monad soku1`` () =
      observable {
        let! a1 = observable{ let! a = observable {return fun x -> x * 2} 
                              let! b = observable {return 3} 
                              return a b}
        let! a2 = observable{ return 3 |> fun x -> x * 2 }
        return a1 |> should equal a2
      } |> Rx.subscribe(fun _ -> ()) |> ignore 

    [<Test>] 
    // モナド則2: m >>= return == m
    // bindしてreturnしても結局同じことだよねの規則
    // あるいは、結局最後の式が return されることになるので、明示的な return は意味ナッシンというお話
    member test.``monad soku2`` () =
      let m1 = observable{ let! a = observable {return "F#"} 
                           return a}
      let m2 = observable{ return "F#" }
      Reactive.Testing.Extensions.AssertEqual(m1, m2)

    // モナド則3: m >>= (\x -> f x >>= g) == (m >>= f) >>= g
    // 多段ネストしたモナドでも(どんなに深くても)、結局のところ一段のモナドと等価ですよの規則
    [<Test>] 
    member test.``monad soku3`` () =
      let m1 = observable{ let! a = observable {return 3} 
                           let! b = observable {return 4}
                           let! x = observable {let! d = observable{return a}
                                                let! e = observable{return b}
                                                return d + e}
                           let! c = observable {return fun x -> x * 2}
                           return c x}
      let m2 = observable{ return 3 + 4 |> fun x -> x * 2 }
      Reactive.Testing.Extensions.AssertEqual(m1, m2)

  // nunit-gui-runner
  let main () = NUnit.Gui.AppEntry.Main([|System.Windows.Forms.Application.ExecutablePath|]) |> ignore
  main ()
 


ごくごく単純な確認ですので、正確な証明とまではいきませんが、
Observableコンピューテーション式が、モナド則を満たしているであろうことをゆるく確認することができます。
てゆうか、Observableコンピューテーション式は、単純にRxのObservableをはめ込んで適用しただけの代物なので、
Rxがそもそもモナド則を満たしているというのが本当のところです。RxのObservableはまさにモナドなのです。





[追記]

@nobuhisa_kさんに、コメントにてナイスつっこみを頂きました!
おっしゃるとおりで、上記のモナド則3の確認は間違えていますね。
モナド則3は、誤解を恐れずイメージしやすいように大雑把に言うと、「(2 * 3) * 4 * 5 == 2 * (3 * 4) * 5」だよねみたいな。
モナドにおいてもこれと同じことが成立していて欲しいと。していなきゃ困ると。


ということで、丸パクリで書き直してみました。


お手軽にお試しできる版

let x = 1
let m = observable { return 3 }
let f x = observable { return 4 + x }
let g x = observable { return 2 * x }
let (>>=) m f = observable {let! x = m
                            return! f x}

let return' x = observable { return x }

let prove (left,right) = 
  observable {let! x = (left:IObservable<'a>)
              let! y = (right:IObservable<'a>)
              return x = y}

prove (return' x >>= f, f x) |> Rx.subscribe(fun b -> printfn "モナド則1 : %b" b) |> ignore // true
prove (m >>= return', m) |> Rx.subscribe (fun b -> printfn "モナド則2 : %b" b) |> ignore // true
prove ((m >>= f) >>= g, m >>= (fun x -> f x >>= g)) |> Rx.subscribe(fun b -> printfn "モナド則3 : %b" b) |> ignore // true

よりテストっぽく

namespace FSharp.Rx.UT

open System

module Tests = 
  open System.Reactive 
  open NUnit.Framework
  open FsUnit
  open FSharp
  open FSharp.Rx
      
  [<TestFixture>]
  type ``Observable モナド則`` () =
    let (>>=) m f = observable {let! x = m
                                return! f x}
    let return' x = observable { return x }

    let x = 1
    let m = observable { return 3 }
    let f x = observable { return 4 + x }
    let g x = observable { return 2 * x }

    let assertEqual (left, right) = Reactive.Testing.Extensions.AssertEqual((left:IObservable<'a>), right)
    let (==) left right = assertEqual (left, right)

    [<Test>] 
    // モナド則1: return x >>= f == f x
    member test.``モナド則1`` () =
      return' x >>= f == f x

    [<Test>] 
    // モナド則2: m >>= return == m
    member test.``モナド則2`` () =
      m >>= return' == m

    [<Test>] 
    // モナド則3: (m >>= f) >>= g == m >>= (\x -> f x >>= g)
    member test.``モナド則3`` () =
      (m >>= f) >>= g == (m >>= (fun x -> f x >>= g))

  // nunit-gui-runner
  let main () = NUnit.Gui.AppEntry.Main([|System.Windows.Forms.Application.ExecutablePath|]) |> ignore
  main ()


わかりやすい。これならHaskellな人にも怒られなさそうですw
コンピューテーション式(Computation Expressions)をつくったら、
こんな風にモナド則を満たしているかどうか確認するとよいですね(実際はもっと抽象化した方がいい)。
これでモナド則ももうこわくないでござる。


あわせて読みたい

モナド則を満たすべき理由 - HaHaHa!(old)
http://haskell.g.hatena.ne.jp/nobsun/20080928/p1


これは参考になる

*1:bind