リストモナドをPythonで再現したい part 2
前回のおさらい
Python で Haskell のリストモナドを再現しました。
def foldr(f, z, xxs):
if xxs == []:
return z
x = xxs[0]
xs = xxs[1:]
return f(x, foldr(f, z, xs))
def concat(xxs):
plus = lambda x, y: x + y
return foldr(plus, [], xxs)
def ret(a):
"""
return :: a -> m a の代わり
"""
return [a]
def bind(ma, a_to_mb):
"""
(>>=) :: m a -> ( a -> m b) -> m b の代わり
"""
return concat(list(map(a_to_mb, ma)))
前回は以下の一文で締めました。
次回はこれを満たすことを確認したいと思います。
今回はこれを確認したいと思います。
モナド則を満たすのか？
モナドは以下を満たしていないといけません。
-
return a >>= fとf aは等価 -
m >>= returnとmは等価 -
(m >>= f) >>= gとm >>= (\x -> f x >>= g)は等価
一般的な証明をするわけにもいかないので、簡単な具体例で確認します。
とはいえ、まず Python で無理やり実装しているので、ちょっとした読み替えが必要です。
-
return aはret(a)と読み替えられます。 -
ma >>= fはbind(ma, f)と読み替えられます。
return a >>= f と f a が等価
a と f を以下とします。
>>> a = 2
>>> f = lambda x: [x, x * 2]
return a >>= f は bind(ret(a), f) で表せます。
すると、
>>> bind(ret(a), f)
[2, 4]
>>> f(a)
[2, 4]
合ってますね。
a を文字列にしても大丈夫なようです。
>>> a = "ABC"
>>> f = lambda x: [x, x * 2]
>>> bind(ret(a), f)
['ABC', 'ABCABC']
>>> f(a)
['ABC', 'ABCABC']
m >>= return と m が等価
同じく a と f を以下とします。
>>> a = 2
>>> f = lambda x: [x, x * 2]
m はただリストにぶち込むだけなので、こうなります。（ですよね？？？）
def m(a):
return [a]
return と同じですが、多分合ってると思います。
ここで m は関数ですが、そのまま使うのは難しいので何かしらの a に適用した結果を使います。
>>> bind(m(a), ret)
[2]
>>> m(a)
[2]
大丈夫そうです。
文字列版も試します。
>>> a = "ABC"
>>> f = lambda x: [x, x * 2]
>>> bind(ret(a), f)
['ABC']
>>> m(a)
['ABC']
同じく大丈夫そうです。
(m >>= f) >>= g と m >>= (\x -> f x >>= g) が等価
最後です。
>>> a = 2
>>> f = lambda x: [x, x * 2]
>>> g = lambda x: [x + 1, x + 5]
ちょっと式が複雑になります。
最初は(m >>= f) >>= g の表現です。
m >>= f は bind(m, f) ですが、これも具体的な値 a を入れることにします。
すると bind(m(a), f) となりますから、これを bind(XXXX, g) の XXXX の場所に入れて bind(bind(m(a), f), g) が得られます。
もう一方 m >>= (\x -> f x >>= g) は、 bind(m(a), YYYY) の YYYY の場所に (\x -> f x >>= g) つまり lambda x: bind((f), g) を代入すれば良いので bind(m(a), lambda x: bind(f(x), g)) です。
実際に計算させると
>>> bind(bind(m(a), f), g)
[3, 7, 5, 9]
>>> bind(m(a), lambda x: bind(f(x), g))
[3, 7, 5, 9]
一致します。
文字列バージョンも試します。
>>> a = "ABC"
>>> f = lambda x: [x, x * 2]
>>> g = lambda x: [x + "p", x + "q"]
>>> bind(bind(m(a), f), g)
['ABCp', 'ABCq', 'ABCABCp', 'ABCABCq']
>>> bind(m(a), lambda x: bind(f(x), g))
['ABCp', 'ABCq', 'ABCABCp', 'ABCABCq']
一致します。
次は do 記法の再現か？
やりたい・・・！
Discussion