\documentclass[conference]{IEEEtran}

\usepackage[cmex10]{amsmath}
\usepackage{url}
\usepackage{listings}

\lstset{
  frame=single,
  keepspaces=true,
  stringstyle={\ttfamily},
  commentstyle={\ttfamily},
  identifierstyle={\ttfamily},
  keywordstyle={\ttfamily},
  basicstyle={\ttfamily},
  breaklines=true,
  xleftmargin=0zw,
  xrightmargin=0zw,
  framerule=.2pt,
  columns=[l]{fullflexible},
  numbers=left,
  stepnumber=1,
  numberstyle={\scriptsize},
  numbersep=1em,
  language={},
  tabsize=4,
  lineskip=-0.5zw,
  escapechar={@},
}

\ifCLASSINFOpdf
  % \usepackage[pdftex]{graphicx}
  % declare the path(s) where your graphic files are
  % \graphicspath{{../pdf/}{../jpeg/}}
  % and their extensions so you won't have to specify these with
  % every instance of \includegraphics
  % \DeclareGraphicsExtensions{.pdf,.jpeg,.png}
\else
  % or other class option (dvipsone, dvipdf, if not using dvips). graphicx
  % will default to the driver specified in the system graphics.cfg if no
  % driver is specified.
  % \usepackage[dvips]{graphicx}
  % declare the path(s) where your graphic files are
  % \graphicspath{{../eps/}}
  % and their extensions so you won't have to specify these with
  % every instance of \includegraphics
  % \DeclareGraphicsExtensions{.eps}
\fi


% correct bad hyphenation here
\hyphenation{op-tical net-works semi-conduc-tor}


\begin{document}
%
% paper title
% Titles are generally capitalized except for words such as a, an, and, as,
% at, but, by, for, in, nor, of, on, or, the, to and up, which are usually
% not capitalized unless they are the first or last word of the title.
% Linebreaks \\ can be used within to get better formatting as desired.
% Do not put math or special symbols in the title.
\title{Categorical Formalization of Program Modification}


% author names and affiliations
% use a multiple column layout for up to three different
% affiliations
\author{
\IEEEauthorblockN{Yasutaka HIGA}
\IEEEauthorblockA{University of the Ryukyus \\ Email: atton@cr.ie.u-ryukyu.ac.jp}
\and
\IEEEauthorblockN{Shinji KONO}
\IEEEauthorblockA{University of the Ryukyus \\ Email: kono@ie.u-ryukyu.ac.jp}
}

% make the title area
\maketitle

% As a general rule, do not put math, special symbols or citations
% in the abstract
\begin{abstract}
We proposed programming units called code segments and data segments.
These are parts of code and data. It is designed to be work with
meta computation. To represent meta computation, Monad is used.
As an example, we define multi versions of programs
as a Monad.
\end{abstract}

% no keywords




% For peer review papers, you can put extra information on the cover
% page as needed:
% \ifCLASSOPTIONpeerreview
% \begin{center} \bfseries EDICS Category: 3-BBND \end{center}
% \fi
%
% For peerreview papers, this IEEEtran command inserts a page break and
% creates the second title. It will be ignored for other modes.
\IEEEpeerreviewmaketitle

\section{Continuation based C}
We proposed units of program named code segment and data segment.
Code segment is a unit of calculation which has no state.
Data segment is a set of typed data.
Code segments are connected to data segments with a context, which is a meta data segment.
After an execution of a code segment and its context, next code segments (Continuation) is executed.

We had developed a programming language ``Continuation based C`` \cite{DBLP:journals/corr/abs-1109-4048},
Hear after we call it CbC, which supports code segments.
CbC is compatible with C language and it has continuation as a goto statement.
Actually, goto statements are tail call of another a code segment and a code segment is a C function.
Tail call elimination is forced by our LLVM based compiler.
We are currently designing data segments part on CbC.

Code segments and data segments are low level enough to represent computation details,
and it is architecture independent.
It can be used as an architecture independent assembler.

In this paper, meta computation of CbC is discussed.
We introduce meta computation as a Monad.
As an example, versioning of functions are represented as a Monad.
Reliability of a program strongly depends on a method of modification.
Program modifications are defined as Monad which contains previous versions of the functions.
In this way, program modifications are represented as a meta computation.
For example, We can execute multi versions simultaneously using this Monad.

\section{Meta computation and a Monad}
Meta computations in CbC are formalized by Monad.
At first, we review meta computation and Monad.

Monad is a notion of Category Theory.

A category contains arrows and objects.
Arrow in a category is function.
Objects in a category is types.
A function has its input type and its output type,
so an arrow in a category has domain object and codomain object.
Composition of arrows and its association laws are provided.


If you have a function f which domain is A and codomain is B,
    $ f :: A \rightarrow B $
Then, there are meta function $ f^* $ which codomain is T B.
In this way, normal computation and meta computation as one to one correspondence\cite{Moggi:1991:NCM:116981.116984}.
Various computations such as partiality, nondeterminism, side-effects, exceptions and continuations are represented as Monads.

We use typed lambda calculus as a representation of function and Haskell syntax is used.
Programs notated typed lambda calculus constructed values and functions.
Value x has a type A is notated as $ x :: A $.
An application of a function f to value x is notated as $ f x $.

\begin{align*}
    x :: A \\
    f :: A \rightarrow B \\
    f x :: B \\
\end{align*}


Function composition operator is ``.`` .
As usual order of composition are associative.

\begin{align*}
    f :: A \rightarrow B \\
    g :: B \rightarrow C \\
    g . f :: A \rightarrow C \\
    \\
    h :: C \rightarrow D \\
    (h . g) . f = h . (g . f) :: A \rightarrow D
\end{align*}

Sum type is introduced using Haskel syntax(Table \ref{src:delta_data_definition}).

\begin{table}[html]
\begin{lstlisting}
data Delta a = Mono a
             | Delta a (Delta a)
\end{lstlisting}
\caption{Definition of data type ``Delta`` in Haskell}
\label{src:delta_data_definition}
\end{table}

This is data type definition of sum type delta which has type variable {\tt a}.
{\tt Mono a} and {\tt Delta a} is a constructor of data type {\tt Delta}, which maps object a in a category to object {\tt Delta a} in the same category.
Functor is a mapping from category A to B, which has two mappings, one for object mapping and one for arrow mapping(Table \ref{src:delta_fmap}).

\begin{table}[html]
\begin{lstlisting}
deltaFmap :: (a -> b) -> Delta a -> Delta b
deltaFmap f (Mono x)    = Mono (f x)
deltaFmap f (Delta x d) = Delta (f x) (deltaFmap f d)
\end{lstlisting}
\caption{Arrow mapping for data type ``Delta``}
\label{src:delta_fmap}
\end{table}

Arrow mapping in a functor satisfies identity law and distribution law.
Data type can be accessed by pattern matching(Table \ref{src:head_delta}).

\begin{table}[html]
\begin{lstlisting}
headDelta :: Delta a -> a
headDelta (Mono  x)   = x
headDelta (Delta x d) = x
\end{lstlisting}
\caption{Define function to Delta using pattern matching}
\label{src:head_delta}
\end{table}

This is a natural transformation from functor Delta to identity functor.
Natural transformation is a set of arrow between two functors, which satisfies commutative law.
%   f (headDelta x) = headDelta (delta-fmap f x)

Monad in category A is $ triple (T, \eta, \mu) $.
T is a functor from A to A.
$ \eta $ is a natural transformation from identity functor to T.
$ \mu $ is a natural transformation from TT to T.
TT is a nested data structure of T.

Monad also satisfies to laws below:

\begin{itemize}
    \item association law : $ {\mu}_{A}  . {\mu}_{T A} = {\mu}_{A} . T {\mu}_{A} $
    \item unity law : $ {\mu}_{A} . \eta_{T A} = \mu_{A} . T \eta_{A} = id_{T A} $
\end{itemize}

Various meta computations represents by definition of triple.
For each function $ f :: A \rightarrow B $ , there is a meta computation $ f^* :: A \rightarrow T B $.
Combination of $ f^* $ $ g^* $ $ h^* $ is defined as follows:

\begin{align*}
    (h^* . g^*) . f^* = h^* . (g^* . f^*)
\end{align*}

Association law of $ f^* $ is derived from Monad laws.
In this way, for each Monad there is a new category of $ f^* $ which is a well known Kleisli Category.

Normal function f has a meta function $ f^* $ which returns Monad T.

% Remove description Kleisli category

% Monad has another description Kleisli Triple $ (T, \eta, \_^{*}) $.
%
% Kleisli triple are following equations hold:
%
% \begin{itemize}
%     \item $ \eta^{*}_A    = id_{T A} $
%     \item $ \eta;f^{*}    = f \mbox{ for } f : A \rightarrow T B $
%     \item $ f^{*} ; g^{*} = (f; g^{*})^{*} \mbox{ for } f : A \rightarrow T B \mbox{ and } g : B \rightarrow T C $
% \end{itemize}
%
% $ id $ is abstraction that identity mapping for any typed values ($ id x = x $).
% $ id $ was exists any typed values.
% Notation $ id_{X} x $ is application $ id $ to a value x typed X.
% Then, $ T $ is functor that pair of structure and a map that abstraction for non-structured values to abstraction for structured values.
% If applied functor T to type A notated $ T A $.
% For example, list of any types is functor.
% List can be constructed to any typed values (list of characters, list of integers, etc) and can be apply abstraction for stored elements.
%
% \begin{eqnarray*}
%     xs = \verb/[10 , 20 , 30]/ \\
%     xs : \verb/List Int/ \\
%     f  : \verb/Int/ \rightarrow \verb/String/ \\
%     \verb/[f 10 , f 20 , f 30]/ : \verb/List String/
% \end{eqnarray*}
%
% It's summarized informal definition of functor for explain Monad.
% Values extended using property of functor T extend abstraction to normal values to structured values.
% Kleisli triple $ (T, \eta, \_^{*}) $ are a triple of functor T and $ \eta $ extension of normal values to meta one and $ \_^{*} $ extension of abstraction.
% Kleisli triple are derivable from Monad $ (T, \eta, \mu) $
%
% Definition of diverging computation as extend normal computations using Monad are shown.
%
% \begin{itemize}
%     \item $ T A = A_{\bot} (= A + \{\bot\}) $
%     \item $ \eta_A $ is the inclusion of A into $ A_{\bot} $
%     \item if $ f : A \rightarrow T B $, then $ f^{*} (\bot) = \bot $ and $ f^{*}(a) = f (a) $ when $ a $  has type A.
% \end{itemize}

\section{Modification of Program using Monad}
A program is set of function.
Modifications of a program are set of mapping from old version of functions to new functions.
These versions may have different types or same types and each version have correct type matchings.

% Definition of modifications named 'Delta Monad' are shown:
% \begin{itemize}
%     \item $ T A = A_0 \times A_1 \times \dots \times A_n $
%     \item $ \eta_A $ is map to values accumulated modification.
%     \item if $ f : A \rightarrow T B $ and $ x : T A  $ then \\
%         $ f^{*}(x) = \langle f_0(x_0) , f_1(x_1), \dots, f_n(x_n) \rangle$
% \end{itemize}



In case of modification with no type changes, Delta Monad is defined as a program modification as follows:

\begin{table}[html]
\begin{lstlisting}
data Delta a = Mono a
             | Delta a (Delta a) deriving Show

headDelta :: Delta a -> a
headDelta (Mono  x)   = x
headDelta (Delta x d) = x

tailDelta :: Delta a -> Delta a
tailDelta (Mono x)     =  Mono x
tailDelta (Delta d ds) = ds

instance Monad Delta where
  return x           = Mono x
  (Mono x) >>= f     = f x
  (Delta x d) >>= f  = Delta (headDelta (f x))
                             (d >>= (tailDelta . f))
\end{lstlisting}
    \caption{Definition of Delta Monad in Haskell}
    \label{src:delta_monad}
\end{table}

Modifications of values are stored as a list like structure.
Delta contains two constructor {\tt Mono} and {\tt Delta}, {\tt Mono} represents first version, {\tt Delta} represents modification.
Infix operator \verb/>>=/ handles meta functions has typed $ A \rightarrow Delta B $ recursive applies to each original versions.
This definition represents simple modification only monotonic increase versioning (exclude branching and merging) and program has consistent type in all versions.
We proved satisfying Monad laws by proof assistant language Agda\cite{agda}.
This monad can be combined with other Monad such as Writer.

\section{Example}
We show an example using Delta Monad(Table \ref{src:example_of_delta}).
A program contains only a function which calculate integer.
In first version, function f is adding 2 to argument.
In second version, modified function f multiplying 3 to argument.
We can define {\tt f'} as a meta function contains both version.
Meta function {\tt f'} outputs two results for value 100.

\begin{table}[html]
\begin{lstlisting}
-- functiion version one. add 2 to integer.
f :: Int -> Int
f x = x + 2

-- function version two. multiply 3 to integer.
f2 :: Int -> Int
f2 x = x * 3

-- meta function contains two version.
f' :: Int -> Delta Int
f' x = Delta (x + 2) (Mono (x * 3))

-- We can execute multi versions simultaneously.
-- *Main> Mono 100 >>= f'
-- Delta 102 (Mono 300)
\end{lstlisting}
\caption{An Example using Delta}
\label{src:example_of_delta}
\end{table}

\section{Conclusion and Future Works}
Program modification is defined as a Monad.
Modifications as meta computations makes various checking methods possible.
These checking methods are also some kind of Monads.
In this way, we can provide program development tool based on categorical formulation.
We are implementing various methods in CbC.
In this paper, we only handles modification on the same types.
Formulation of Modifications on the different types will be proposed in future.
Only linear version structure handled here.
We hope that more complex structure such as branching or merging can be handle in the same way.


% An example of a floating figure using the graphicx package.
% Note that \label must occur AFTER (or within) \caption.
% For figures, \caption should occur after the \includegraphics.
% Note that IEEEtran v1.7 and later has special internal code that
% is designed to preserve the operation of \label within \caption
% even when the captionsoff option is in effect. However, because
% of issues like this, it may be the safest practice to put all your
% \label just after \caption rather than within \caption{}.
%
% Reminder: the "draftcls" or "draftclsnofoot", not "draft", class
% option should be used if it is desired that the figures are to be
% displayed while in draft mode.
%
%\begin{figure}[!t]
%\centering
%\includegraphics[width=2.5in]{myfigure}
% where an .eps filename suffix will be assumed under latex,
% and a .pdf suffix will be assumed for pdflatex; or what has been declared
% via \DeclareGraphicsExtensions.
%\caption{Simulation results for the network.}
%\label{fig_sim}
%\end{figure}

% Note that IEEE typically puts floats only at the top, even when this
% results in a large percentage of a column being occupied by floats.


% An example of a double column floating figure using two subfigures.
% (The subfig.sty package must be loaded for this to work.)
% The subfigure \label commands are set within each subfloat command,
% and the \label for the overall figure must come after \caption.
% \hfil is used as a separator to get equal spacing.
% Watch out that the combined width of all the subfigures on a
% line do not exceed the text width or a line break will occur.
%
%\begin{figure*}[!t]
%\centering
%\subfloat[Case I]{\includegraphics[width=2.5in]{box}%
%\label{fig_first_case}}
%\hfil
%\subfloat[Case II]{\includegraphics[width=2.5in]{box}%
%\label{fig_second_case}}
%\caption{Simulation results for the network.}
%\label{fig_sim}
%\end{figure*}
%
% Note that often IEEE papers with subfigures do not employ subfigure
% captions (using the optional argument to \subfloat[]), but instead will
% reference/describe all of them (a), (b), etc., within the main caption.
% Be aware that for subfig.sty to generate the (a), (b), etc., subfigure
% labels, the optional argument to \subfloat must be present. If a
% subcaption is not desired, just leave its contents blank,
% e.g., \subfloat[].


% An example of a floating table. Note that, for IEEE style tables, the
% \caption command should come BEFORE the table and, given that table
% captions serve much like titles, are usually capitalized except for words
% such as a, an, and, as, at, but, by, for, in, nor, of, on, or, the, to
% and up, which are usually not capitalized unless they are the first or
% last word of the caption. Table text will default to \footnotesize as
% IEEE normally uses this smaller font for tables.
% The \label must come after \caption as always.
%
%\begin{table}[!t]
%% increase table row spacing, adjust to taste
%\renewcommand{\arraystretch}{1.3}
% if using array.sty, it might be a good idea to tweak the value of
% \extrarowheight as needed to properly center the text within the cells
%\caption{An Example of a Table}
%\label{table_example}
%\centering
%% Some packages, such as MDW tools, offer better commands for making tables
%% than the plain LaTeX2e tabular which is used here.
%\begin{tabular}{|c||c|}
%\hline
%One & Two\\
%\hline
%Three & Four\\
%\hline
%\end{tabular}
%\end{table}


% Note that the IEEE does not put floats in the very first column
% - or typically anywhere on the first page for that matter. Also,
% in-text middle ("here") positioning is typically not used, but it
% is allowed and encouraged for Computer Society conferences (but
% not Computer Society journals). Most IEEE journals/conferences use
% top floats exclusively.
% Note that, LaTeX2e, unlike IEEE journals/conferences, places
% footnotes above bottom floats. This can be corrected via the
% \fnbelowfloat command of the stfloats package.







% conference papers do not normally have an appendix





% trigger a \newpage just before the given reference
% number - used to balance the columns on the last page
% adjust value as needed - may need to be readjusted if
% the document is modified later
%\IEEEtriggeratref{8}
% The "triggered" command can be changed if desired:
%\IEEEtriggercmd{\enlargethispage{-5in}}

% references section

% can use a bibliography generated by BibTeX as a .bbl file
% BibTeX documentation can be easily obtained at:
% http://www.ctan.org/tex-archive/biblio/bibtex/contrib/doc/
% The IEEEtran BibTeX style support page is at:
% http://www.michaelshell.org/tex/ieeetran/bibtex/
%\bibliographystyle{IEEEtran}
% argument is your BibTeX string definitions and bibliography database(s)
%\bibliography{IEEEabrv,../bib/paper}
%
% <OR> manually copy in the resultant .bbl file
% set second argument of \begin to the number of references
% (used to reserve space for the reference number labels box)

\nocite{opac-b1092711, BarrM:cattcs, Girard:1989:PT:64805, JonesDuponcheel93}
\bibliographystyle{IEEEtran}
\bibliography{IEEEabrv,reference}



% that's all folks
\end{document}