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 とデータ構造を対応付ける手法である
* プログラムの変更は変更前の動作を保存しつつ変更後の動作を追加することで表現する
* 異なるバージョンのプログラムを同時に実行し、トレースを比較することでデバッグを支援する手法を提案する

# 連絡/質問
* 研究計画書?
    * 指導教員
* LOLA 2015
    * abstract submission : 2015/04/20
    * operational semantics

# 春休み期間でやってたことなど
* 関数の型が変わる変更を表す Delta
    * 良い定義できず
    * 内部変数の型情報を無くしたら動くことは確認できました
    * のでどうにかすれば定義できることは分かった
    * Dependent Type/ ghc pragma/ meta programming
* adjointness と Solution to Universal Mapping Problem を追ってました
    * Introduction to Higher Order Categorical Logic

# 変更時に異なる型を含む Delta
* 型を合わせるように書こうと思ったけれど無理でしたという話
    * 定義を変えないといけなさそうです
    * ExistentialQuantification, TemplateHaskell?
* 現 Delta でもそれぞれのシーケンスごとでは型はあってます
    * 型情報を取ると動きました


# 型が変わる変更を Delta で表す時のの問題点
```
x :: A, y :: C
f :: A -> B, g :: C -> D
x* >>= f* = (fst (f x, g x),
             snd (f y, g y))
```
* 型整合していない計算が候補として存在している
* 型整合していない値は使わないけれど、型チェック時に弾かれる


# 現Deltaの定義で中の値を Dynamic にする
* value も function も格納できる型 Dyamic
* Dynamic と Dynamic で apply できる
    * 型が合わないと Nothing になる
    * 型が当ってると Just になる
* これを Delta の値として使うと、計算はできた
    * ので型があってないのが問題

# 型の変更を含む Delta
* 理想
  * apply function
    * `` (x, x') >>= (f, f') ``
  * variable type
    * `` (x, x') :: (Delta a) in (x :: a)``
  * function type
    * `` (f, f') :: a -> (Delta b) in (f :: a -> b)``

# 型変数を減らす?
* T A の中に B があっても問題無いのでは? という案
    * `` data Delta a | ModifyInt Int (Delta a) | Mono a ``
* 問題 : 関数をどうするか
    * A -> T B
    * T B の中に (C -> D) を埋め込む?
    * ってことは型チェック無理

# 型変数をその場で追加する ExistentialQuantification
* 型変数をその場で生成できたりします
`` data Delta b a = forall c. Delta a (Delta b c) | Mono a ``
* こうすると headDelta の型が不定になる
    * a? b? c?

# 問題点
* tuple で考えると
* T A から `` (a, a') :: (A, C)`` を作る
* A -> T B から `` (f, f') :: (A -> B, C -> D) `` を作る必要がある
* C と (C -> D) の情報が完全に隠れているので推論できない
* Dependent Type でどうにかする?

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