# HG changeset patch # User Yasutaka Higa # Date 1413881147 -32400 # Node ID b58c0ab4f5e408bafad9c0a608c2a7b392f11528 # Parent 916d62123b1ca023bc1f4ab06bd7767891e76cc7 Add slides for seminar diff -r 916d62123b1c -r b58c0ab4f5e4 slides/20141021/slide.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slides/20141021/slide.md Tue Oct 21 17:45:47 2014 +0900 @@ -0,0 +1,58 @@ +title: モナドによるプログラムの拡張 +author: Yasutaka Higa +cover: +lang: Japanese + + + +# 研究目的(modified) +* プログラミングにおいて、ソースコードを改変するとプログラムの挙動も変わる +* しかし、バージョン互換を維持する場合など、ソースコードを変更した後も同じ結果を得たい場合もある +* プログラムの改変をモナドによる拡張としてとして記述することで過去のプログラムの挙動も保存したい +* これによりリファクタリング支援や後方互換性の確保、拡張による実行結果の変化の検出などを行なう + + +# Summary +* 中間発表予稿提出が今月末(10/30) +* 教官室 Mac mini の domain を教えてください +* Similar の Functor 則の証明 in Agda +* Similar の Monad 則の証明中 in Agda +* あと例題欲しい + * Haskell で version compatible なコードを書く予定 + +# Proof Functor-laws to similar +* Functor-laws [(Haskell)](http://www.haskell.org/haskellwiki/Functor) +* refl で問題無し + +``` + fmap id = id + fmap (p . q) = (fmap p) . (fmap q) +``` + + +# Proof Monad-laws to Similar (Category) +* Monad-laws (Category) + * mu and eta + +``` +join . fmap join = join . join +join . fmap return = join . return = id +return . f = fmap f . return +join . fmap (fmap f) = fmap f . join +``` + + +# Proof Monad-laws to Similar (Haskell) +* Monad-laws (Haskell) + * return and bind + +``` + return a >>= k = k a + m >>= return = m + m >>= (\x -> k x >>= h) = (m >>= k) >>= h +``` + +# Check Point +* 3 つめでちょっとつまってます + +