# HG changeset patch # User atton # Date 1429443147 -32400 # Node ID 7b833cdd68a9e62d00d15847b2ad077ffbe6a5e0 # Parent d62cfdf464fec7674baa9a3ebc476921ed14e831 Improvements by kono teacher diff -r d62cfdf464fe -r 7b833cdd68a9 cfopm.tex --- a/cfopm.tex Sun Apr 19 17:17:16 2015 +0900 +++ b/cfopm.tex Sun Apr 19 20:32:27 2015 +0900 @@ -97,40 +97,69 @@ % creates the second title. It will be ignored for other modes. \IEEEpeerreviewmaketitle -\section{Continuation based C} % enough only describe code/data segment? -We proposed programming style using unit of program named code segment and data segment. -Code segment is a unit of calculation not dependents state. -Data segment contains values of calculation and calculation context called meta data segment. -Execution of program is represented by moves interconnected code segments. -Code/Data segment style programming was suitable to state based concurrent program. +\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 function. +In this way, program modifications are represented as a meta computation. +For example, We an execute multi versions simultaneously using this Monad. -Programming language 'Continuation based C' (CbC\cite{DBLP:journals/corr/abs-1109-4048}) supported code/data segment style programming. -CbC is lower language of C removed function call and loop-statements(for, while) and added continuation by goto and code segment. -Code segment of CbC is function without return values in C. -Interconnections of code segment represents goto with environment. -CbC can define meta calculation as calculation of calculation named meta code segment. -Meta computations contains various computations including partiality, nondeterminism, side-effects, exceptions and continuations. +\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. + -\section{Meta computation and Monads} -Meta computations in CbC formalized by Monads to prevent chaos by unlimited computations. -Monads are a notion of Category Theory, in programs Monad correspondence of normal/meta computations\cite{Moggi:1991:NCM:116981.116984}. -For example, diverging computation is represented direct sum of normal values and bottom. +Functor is a data type which has a type variable. +Monad is a functor which satisfies Monad laws. +Monad laws contains natural transformations, eta and mu. -We show formalization of programs for using Monads. -Programs notated typed lambda calculus constructed values and abstractions. -Abstraction f maps value to value, and applies to value x notated $ f x $. -Every lambda term has a type. -Value x has type A notated $ x : A $. -Abstraction f has a argument of type A and return value of type B notated $ f : A \rightarrow B $. +If you have a function f which domain is A and codomain is B, + f :: A -> 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{eqnarray*} - x : A \\ - f : A \rightarrow B \\ - f x : B \\ + x :: A \\ + f :: A \rightarrow B \\ + f x :: B \\ \end{eqnarray*} -Type matched abstractions can be composed by operator '$\circ$'. -Order of composition are commutative. +Function composition operator is '.'. +As usual order of composition are associative. \begin{eqnarray*} f : A \rightarrow B \\ @@ -141,10 +170,37 @@ (h \circ g) \circ f = h \circ (g \circ f) : A \rightarrow D \end{eqnarray*} -Abstractions has many arguments notated by abstraction took a argument, and returns a abstraction that argument numbers has decreased(Currying). +Sum type is introduced using Haskel syntax. + + data Delta a = Mono a + | Delta a (Delta a) + +This is data type definition of sum type delta which has type variable {\tt a}. +Mono a and Delta a is a constructor of data type Delta, which maps object a in a category to object 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. + + fmap-delta :: (a -> b) -> Delta a -> Delta b + fmap-delta f (Mono x) = Mono (f x) + fmap-delta f (Delta x d) = Delta (f x) (fmap-delta f d) + +Arrow mapping in a functor satisfies identity law and distribution law. +Data type can be accessed by pattern matching. -Abstractions can be extended using Monad. -Monad is $ triple (T, \eta, \mu) $ satisfies laws. + headDelta :: Delta a -> a + headDelta (Mono x) = x + headDelta (Delta x d) = x + +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} \circ {\mu}_{T A} = {\mu}_{A} \circ T {\mu}_{A} $ @@ -152,62 +208,72 @@ \end{itemize} Various meta computations represents by definition of triple. -Monad has another description Kleisli Triple $ (T, \eta, \_^{*}) $. - -Kleisli triple are following equations hold: +For each function f :: A -> B, there is a meta computation f* :: A -> T B. +Combination of f* g* is defined as follows: -\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} + f* . g* = mu (delta-fmap f* (mu (delta-fmap g*))) + +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. -$ 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. +Normal function f has a meta function f* which returns Monad T. + +% Remove description Kleisli category -\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} +% 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} -Reliability of a program dynamically changed in software development. -We propose handle modifications of a program as meta computations for improve reliability. -Modifications represents a set of program versions including values and abstraction with type consistency. -Execution of program including modification like concurrent execution of all versions. - -Definition of modifications named 'Delta Monad' are shown: +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. -\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} +% 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} -Versions of a program without branching represents finite direct product. + -We simulated Delta Monad in Haskell (Table\ref{src:delta_monad}). +In case of modification with no type changes, Delta Monad is defined as a program modification as follows: \begin{table}[html] \begin{lstlisting} @@ -231,18 +297,28 @@ \caption{Definition of Delta Monad in Haskell} \end{table} -We aim to prove Delta Monads satisfies Monad laws using Haskell has built-in Monad definition. -Modifications of values stored list like structure named Delta. +Modifications of values are stored as a list like structure. Delta contains two constructor Mono and Delta, Mono represents first version, Delta represents modification. -Infix operator \verb/>>=/ handles extended abstraction has typed $ \verb/A/ \rightarrow \verb/Delta B/ $ recursive applies to each original versions. +% FIXME +Infix operator \verb/>>=/ handles extended functions has typed $ \verb/A/ \rightarrow \verb/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 executed different versions in same time and proved satisfying Monad laws by proof assistant language Agda\cite{agda}. +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} + +% +2, *2 \section{Conclusion and Future Works} -Handleable modification by meta computations is proposed. -Using this Delta Monad, we can make reliable program development possible. -Especially, Automatically property comparison in development cycle is made possible by CbC also plans incorporate model checker as meta computations. -We aim to extend Delta Monad represents all possible modifications (branching, merging, and more) with proof and implement to CbC. +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.