title: Categorical Formalization of Program Modification
author: Yasutaka Higa
profile : Concurrency Reliance Laboratory (Kono lab) <br> Department of Information Engineering <br> University of the Ryukyus
lang: English

# Formalization of Program Modification
* To improve the reliability of a program
* Development process has to be formalized
* Especially program modifications are important
* Let's formalize modification using Monad

# Formalization using Monad
* Monad is a notion of Category theory
* Monad represents meta computations in functional program
* We proposed Delta Monad representation of program modifications
* We give definitions and the proof
* Delta Monad can be used with other monads

# Merits of formalizing program modifications
* Formal methods give verification of program based on mathematics and logics
* Such as lambda calculus and corresponding proofs
* Moggi[1989] , introduce Monad as notion of meta computation in program
* A meta computation represented as a Monad has one to one mapping
* We define program modification as meta computation which includes all modifications

# Definitions of Program
* A program is a typed lambda calculus
* lambda term
    * variables : x,y
    * lambda : \x -> f x
    * function applications : f x
* type
    * type variable   : A, B
    * functional type : A -> B

# Every lambda term has a type
```
    y   :: B
    f   :: A -> B
    f x = y
```
* ``=`` is a function definition
* `` f x `` is a application function ``f``
* `` f x `` has type B

# Definition of Delta in Haskell
```
data Delta a = Mono a | Delta a (Delta a)
```

* ``data`` is a data type definition in Haskell
* `` a `` is a type variable
* `` Mono a`` and `` Delta a (Delta a) `` has a type `` Delta a``
* Delta can be stores all modification like list structure

# How to define meta computation in Haskell
* original function : f  :: a -> b
* meta function     : f' :: a -> Monad b
* Original function combination : f ( g ( x ))
* Meta function combination : (x >>= f') >>= g'
* f' returns various value which type is Monad
* Meta computation defined by f' and ``>>=``
* cf. ``>>=`` is an infix function

# Definition of Delta meta computation
```
 >>= :: (Delta a) -> (a -> Delta b) -> (Delta b)
 (Mono x)    >>= f = f x
 (Delta x d) >>= f = Delta (headDelta (f x))
                           (d >>= (tailDelta . f))
```

* Meta function f is applied to all the versions in a Delta Monad
* Delta data types is accessed by a pattern match
* ``headDelta`` takes first version of Delta
* ``tailDelta`` takes the rest versions

# An example of Program using Delta Monad
* Two versions of a simple program are shown
* Gives Delta Monad representation of the versions
* Various computation can be possible in the Delta

# An Example Program: numberCount (Version 1)

```
generator x     = [1..x]
numberFilter xs = filter isPrime xs
count xs        = length xs

numberCount x = count (numberFilter (generator x))
```

# An Example Program: numberCount (Version 2)

```
generator x     = [1..x]
numberFilter xs = filter even xs
count xs        = length xs

numberCount x = count (numberFilter (generator x))
```

# An Example of Program includes two versions
```
generator x     = Mono [1..x]
numberFilter xs = Delta (filter even xs)
                        (Mono (filter isPrime xs))
count x         = Mono (length x)

numberCount x = count =<< numberFilter =<< generator x
```

# Execute Program includes two version
* result
    * Version 1 : 168
    * Version 2 : 500

```
*Main> numberCount 1000
Delta 500 (Mono 168)
```

# Combine Delta Monad with other Monads
* Delta Monad can be used with other monads
* Meta computations can be added function to Delta
    * Exception, Logging , I/O, etc...

# An Example Delta Monad with Traces
```
*Main> numberCountM 10
DeltaM (Delta (Writer (4, ["[1,2,3,4,5,6,7,8,9,10]",
                           "[2,3,5,7]",
                           "4"]))
       (Mono  (Writer (5, ["[1,2,3,4,5,6,7,8,9,10]",
                           "[2,4,6,8,10]",
                           "5"]))))
```

# How to use Delta Monad in program development
* Executing selected versions
* Comparing traces of versions
* Version Control Systems are formalized by Delta Monad
* Combination of other Monads make development more reliable

# Conclusion
* Program Modifications are formal defined
* Program Modifications are meta computation
* Program Modifications are Delta Monad
* Monad-laws are proved in Agda
* Delta Monad include all necessary aspects of modifications?
* What is products/colimits over program versions?

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