Monad と OS

Menu Menu

琉球大学工学部 河野真治

90年からソニーCSLにいました

    Muse OS
    Apertos 
    Aperiol
とかいう名前の Reflective Operating System 

    AIBO に使われた
が結局はつぶれました。

同僚の横手は PS3 のMeta OSを設計

Reflection

Interpreter の階層で作られたメタ計算 

    Reification   meta から object への反映
    Reflection    object から meta への反映

Apertos

要するに 

    Process はメタ
    Kernel  はメタメタ
これに直交した 

    Muse Core (System call handler)

Apertos の System Call

system call は reflection 

    f --> syscall A --->
    g --> syscall B --->
    h --> syscall C --->
メタ計算は神。何しても良い。

一方、Haskell では

    Monad を使ってメタ計算を表現する
Monad って何? 

    型変数を少なくとも一つ持つデータ構造
型変数は Java の Generic に相当するもの。

Monad 

    f : a -> b
型a を入力として型bを返す関数。これのメタ計算は 

    f': a -> T b
つまり Reflection しかないメタ計算でもある

f と f' は a b それぞれに isomorphic に一対一対応 ( これがメタ計算の双対性)

Monad のηとμ

ηは return 、つまり、デフォルトのメタ計算 

    η b  : b -> T b
という型を持つ関数。これは自然変換である必要があります。 

    f'(x) = η(b) f(x)
が何もしないメタ計算に相当します。 

    f' x = return (f x)

自然変換って何?

可換性がある関数のこと。

ここで T(f) は、 

    T(f) : T a -> T b
つまり、map 関数のこと。mapを持つデータ構造を Functor とも言います。

Monad の結合

    f : a -> b
    g : b -> c
のメタ版、 

    f : a -> T b
    g : b -> T c
で、(もうダッシュは付けません) 

    f (g x) = μ c (T f) g
とします。ここでμは、 

    μ a : T (T a) → T a
つまりμは、f と g の二つのメタ計算を合成する計算になります。

Monad の結合

μが二つのT(メタなデータ構造)を一つのTに変換

Monad の結合法則

    f : a -> b
    g : b -> c
    h : c -> d
で、 

    h (g f) = (h g) f
は成立します。では、メタ計算ではどうか?

メタ計算の結合法則

メタ計算 

    f : a -> T b
    g : b -> T c
    h : c -> T d
があった時に、 

    h (g f) : a -> T d
    (h g) f : a -> T d
で、 

    h (g f) = (h g) f 
    λ x -> (h (g f)) x = λ x -> ((h g) f) x
となって欲しい。(Curry 化が整合して欲しいという希望)

Monad の要請

    η T = T η = id
    μ T μ = μ μ T
この可換性を満たしていれば、Monad の結合法則が満たされます。

証明は面倒。そもそも、この式、どうやって読むんだよ。

Monad で何でも表せるらしい

    並列計算
    IO
    失敗する計算
    例外処理
    継続

Monad は全世界に一つ

    Monad の合成は難しい
    結局、Monad を分解して合成
    lift とか liftIO とかで Monad の組み合わせを上下する

そういえば kernel も全世界に一つ

つまり、 

    Monad = kernel
だよね。

T って kernel では何に相当するの?

    Process 構造体とか
    Scheduler とか
正確には、それにちょっかいを出したい object level の関数の希望(Reflection)。

Tの結合法則は kernel では何に相当するのか?

System call は呼び出された順に整合的に処理される必要がある 

    f --> syscall A --->
        ....
    g --> syscall B --->
    h --> syscall C --->
これと、 

    f --> syscall A --->
    g --> syscall B --->
        ....
    h --> syscall C --->
これは、同等ってこと?

Haskell での計算の順序

Haskell では入力が完全に決まらなくても計算が進む。 

    h (g f) と (h g) f
では計算の進み方が異なる。結果は同じはず。

Monad でも同じであって欲しい。そうすれば元のプログラム(圏)とメタプログラム(Kleisli圏)が対応することになる。

つまり

    f --> syscall A --->
    g --> syscall B --->
    h --> syscall C --->
の f g h は平行実行されて良いが、結果は唯一に定まるというのが Monad の制約。

これは、今のOSで成立しているのか? 

    library call が thread safe
ってことと同等なの? (しょぼい、しょぼすぎる)

まとめ

    OS はメタ計算
    Reflection では自由過ぎる
    Monad のメタ計算の双対性
    Monad は thread safe 
    もう少し OS に使える部分ないの?
琉球大学工学部 河野真治 / Wed Sep 24 07:22:23 2014