view slides/20141021/slide.md @ 163:b8e16c48a5a4 default tip

Update template
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 17 Jan 2017 17:18:41 +0900
parents b58c0ab4f5e4
children
line wrap: on
line source

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 つめでちょっとつまってます

<!-- vim: set filetype=markdown.slide: -->