title: Categorical Formalization of Program Modification
author: Yasutaka Higa
profile:
lang: Japanese


# 研究目的 (Categorical Formalization)
* プログラムの信頼性を向上させるために開発手法に着目する
* プログラムの信頼性が変化するのはプログラムを変更した時である
* プログラムの変更を形式化することにより、信頼性を保ちながらプログラムを変更する
* Kleisli Category の Kleisli Triple と対応のある Monad によってプログラムの変更を記述する

# 研究目的 (Parallel Debugger)
* 本研究では Monad を用いてプログラムの変更を定義する
* Monad とは meta computation とデータ構造を対応付ける手法である
* プログラムの変更は変更前の動作を保存しつつ変更後の動作を追加することで表現する
* 異なるバージョンのプログラムを同時に実行し、トレースを比較することでデバッグを支援する手法を提案する

# 近況報告
* プロシン行ってきました
    * 結構ジャンルはなんでもありでした
    * 機械学習、量子コンピュータ、言語処理系、ソシャゲの解析、HPC、分散FS、etc
* 任意の Monad と組み合せ可能な Delta を Haskell で定義してみました
    * 証明はまだです
    * Agda で type constraints を書けずに止まってます

# 任意の Monad と組み合せ可能な Delta : DeltaM
* 元は MonadTrans を使おうという話でした
* 例として MaybeT IO a は IO Maybe a らしい
* DeltaT を作ると DeltaT IO a は IO (Delta a)
* この場合、「全ての関数は Delta を返す」を満たさない
* 外側に Delta があって内側が任意の Monad であれば実行できる DeltaM にしてみました
* DeltaM IO a は Delta (IO a) です

# 定義中に思ったこと
* Delta と定義が微妙に違います
* 1つの関数のバージョンが上がった時に全てのバージョンを上げないといけません
* function のバージョンを知ることができないから
    * 特に Monad Wrapped value を撮る時に個数が分からない
    * Dependent type で Delta に付属させたりすれば良いのかもしれませんが
* 途中の bind で m a を返さないといけないので型を合わせるためにこうしてみました
    * meta code segment って type にそのまま mapping できるかちょっと疑問に思ったりなんだり

# Agda で苦戦中
* type constraints が書けない
* instance (Monad m) => Monad (DeltaM m)  とか書きたい
* Functor を Record にすることはできましたが
* Functor 受けとってそれに対して fmap ができない
* うーん……

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