\documentclass{beamer}

%\usepackage{beamerthemesplit}
\usetheme{Frankfurt}

\input{mathlig}

\title{Implementing the darcs patch formalism}
\subtitle{...and verifying it}
\logo{\includegraphics[width=1.0cm]{circle_logo}}

\author{David Roundy}
\date{February 2006}
\institute{Cornell University}

\begin{document}

\mathlig{<->}{\leftrightarrow}
\mathlig{|/}{\vee}
\mathlig{/|}{\wedge}

\frame{\titlepage}

\begin{frame}
  \frametitle{The subject of this talk}
  \begin{block}{}
    Darcs a revision control system based on a formalism for manipulating
    changes, which allows for a system that is \emph{change-based} rather
    than \emph{version-based}.  This talk will describe this formalism.
  \end{block}
  \begin{block}{}
    I will also describe a new trick using ``Generalized Algebraic Data
    Types'' (GADTs) to statically check the correctness of
    change-manipulation code.
  \end{block}
\end{frame}

%\section*{Outline}
\begin{frame}
  \frametitle{Outline}
  \tableofcontents
\end{frame}

\input{intro}

\begin{frame}
  \frametitle{Darcs terminology}
  \begin{block}{}
    \begin{itemize}
    \item A \structure{change} is a logical entity.
    \item A \structure{patch} is a description of a change.
    \item The state of a repository is defined by its \structure{set} of
      changes.
    \item A set of changes is stored as a \structure{sequence} of patches.
    \end{itemize}
  \end{block}
  \begin{block}{Notation}
    \begin{itemize}
    \item A \structure{change} is represented as a capital letter:  $A$
    \item A \structure{patch} is represented by a capital letter with
      possibly primes and/or a subscript:  $A$, $A'$, $A_1$
    \item Sometimes the \structure{state} (or \structure{context}) before
      and after a patch is represented by lowercase superscripts:  $^oA^a$
    \end{itemize}
  \end{block}
\end{frame}

\frame{\Huge \center The state of a repository is defined by a
  \structure{set} of changes.}

\section{Patch relationships}

\subsection{Sequence}

\begin{frame}[fragile]
  Patches are normally stored in sequence.  For a sequential pair of
  patches, the final state of the first patch is identical to the initial
  state of the second patch.

  \begin{block}{Mathematical notation}
  \begin{columns}
    \begin{column}{1.5cm}
      \begin{equation*}
        ABC
      \end{equation*}
    \end{column}
    \begin{column}{.5cm}
      or
    \end{column}
    \begin{column}{1.5cm}
      \begin{equation*}
        ^oA^aB^bC^c
      \end{equation*}
    \end{column}
  \end{columns}

  .
  \end{block}

  \begin{block}{Haskell notation}
  \begin{columns}
    \begin{column}{2cm}
\begin{verbatim}
  A :. B
\end{verbatim}
    \end{column}
    \begin{column}{1cm}
      or
    \end{column}
    \begin{column}{2cm}
\begin{verbatim}
A :- B :- C
\end{verbatim}
    \end{column}
  \end{columns}

  .
  \end{block}
\end{frame}

\subsection{Parallel and antiparallel}

\begin{frame}[fragile]
  \frametitle{Parallel and antiparallel}

  Parallel patches begin at the same state, and diverge to two different
  states, while antiparallel patches begin at different states and end at
  the same state.  e.g. for the two patches:
  \begin{equation*}
    ^oA^a \quad \text{and} \quad ^oB^b
  \end{equation*}
  $A$ is parallel to $B$ and $A^{-1}$ is antiparallel to $B^{-1}$.
  \begin{block}{Mathematical notation}
  \begin{columns}
    \begin{column}{2cm}
      \begin{equation*}
        A |/ B
      \end{equation*}
    \end{column}
    \begin{column}{1cm}
      and
    \end{column}
    \begin{column}{2cm}
      \begin{equation*}
        A^{-1} /| B^{-1}
      \end{equation*}
    \end{column}
  \end{columns}

  .
  \end{block}

  \begin{block}{Haskell notation}
  \begin{columns}
    \begin{column}{1.0cm}
\begin{verbatim}
A :\/: B
\end{verbatim}
    \end{column}
    \begin{column}{0.2cm}
      and
    \end{column}
    \begin{column}{3.5cm}
\begin{verbatim}
invert A :/\: invert B
\end{verbatim}
    \end{column}
  \end{columns}

  .
  \end{block}
\end{frame}

\section{Enforcing patch relationships}

\subsection{Introduction to GADTs}

\begin{frame}
  \frametitle{Generalized Algebraic Data Types (GADTs)}
  \emph{``The solution to every problem is to create a new GADT.''}
  \vfill

  \begin{block}{``Generalized Algebraic Data Type''}
    \begin{itemize}
    \item Also known as ``guarded recursive data types'' or ``first-class
      phantom types''
    \item The common use example (which I won't give here) is to allow
      statically typesafe abstract syntax trees.
    \item Allow runtime behavior to statically restrict a subtype.
    \end{itemize}
  \end{block}
\end{frame}

\begin{frame}[fragile]
  \frametitle{A \emph{very} quick glance at Haskell syntax}

  \begin{itemize}
  \item Types are capitalized, as in \texttt{Int}
  \item Functions are lowercase
  \end{itemize}

  \begin{block}{}
  \begin{verbatim}
foo :: Int -> Char -> Bool
\end{verbatim}
  \texttt{foo} is a function that accepts an \texttt{Int} and a \texttt{Char}
  as arguments, and returns a \texttt{Bool}
  \end{block}
  \begin{itemize}
  \item Type \emph{variables} are lowercase
  \end{itemize}
  \begin{block}{}
  \begin{verbatim}
bar :: a -> a -> a
\end{verbatim}
  \texttt{bar} is a function that accepts two arguments of any type, and
  returns a value of the same type.
  \end{block}

\end{frame}

\begin{frame}[fragile]
  \frametitle{Algebraic Data Types}
  \begin{block}{}
  \begin{verbatim}
data Bool where
  True :: Bool
  False :: Bool
\end{verbatim}
  \end{block}
  \begin{block}{}
  \begin{semiverbatim}
data Complex where
  Cartesian :: Double -> Double -> Complex
  Polar :: Double -> Double -> Complex
  PureReal :: Double -> Complex
\end{semiverbatim}
  \end{block}
  \begin{block}{}
  \begin{semiverbatim}
data Maybe a where
  Just :: a -> Maybe a
  Nothing :: Maybe a
\end{semiverbatim}
  \end{block}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Generalized Algebraic Data Types (GADTs)}
  \begin{verbatim}
data Pair a b where
  Pair :: a -> b -> Foo a b
  SymmetricPair :: a -> a -> Foo a a
\end{verbatim}
The latter constructor restricts the type, which allows us to write
typesafe code that wouldn't be possible with the more general type of a
``\verb!Pair a b!''.
  \begin{semiverbatim}
foo :: Pair a b -> b
foo (Pair x y) = y
foo (SymmetricPair x y) = x {\color{red}-- Note the oddness!}
  \end{semiverbatim}
\end{frame}

\subsection{Phantom existential witness types}

\begin{frame}
  \frametitle{Phantom existential witness types}
  \begin{block}{Phantom type}
    A type for which no data member is ever created.  Most common example
    is the use in the ST monad to statically ensure that distinct states
    cannot be mixed.
  \end{block}
  \begin{block}{Existential type}
    A type whose identity cannot be determined.  The type is, however,
    known to exist, and may be known to have certain properties (e.g. be in
    a typeclass).
  \end{block}
  \begin{block}{Witness type}
    A type whose existence is used to prove (``stand as witness'') that
    something is true.  Must be phantom.
  \end{block}
\end{frame}

\section{Patch properties}

\begin{frame}{}
  \begin{center}
    \Huge
    Patch Properties
  \end{center}
\end{frame}

\subsection{Inversion}

\begin{frame}
  \frametitle{Inversion}
  \begin{block}{}
    Every darcs patch must be invertible.
  \end{block}
  \begin{block}{Repercussions:}
    \begin{itemize}
    \item A ``remove file'' patch must either contain the entire contents
      of the file, or one must only be able to remove a file after its
      contents have been removed.  (darcs chooses the latter)
    \item A patch such as ``copy file'' is extra-complicated, since its
      inverse, a ``merge two identical files'' patch has confusing
      semantics (and thus the ``copy file'' patch would as well).
    \item We can apply patches either forwards or backwards to reach a
      particular version.
    \item Other benefits to be seen later when merging...
    \end{itemize}
  \end{block}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Inversion with phantom types as witnesses}
  \begin{block}{The Haskell ``Patch'' type}
\begin{verbatim}
data Patch a b where
    ...
\end{verbatim}
    This says that the \verb!Patch! type is parametrized by two phantom
    types.
  \end{block}

  No GADTs yet, but we gain some expressiveness in function definitions:
  \begin{block}{}
    Compare the Haskell code
\begin{verbatim}
invert :: Patch o a -> Patch a o
\end{verbatim}
    with the mathematical notation $^oA^a$ and $^a\left(A^{-1}\right)^o$.
  \end{block}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Inverse of a sequence}
  \begin{block}{}
    The inverse of a sequence of patches is the sequence of their inverses,
    in reverse order.
  \end{block}
  \begin{align*}
    (ABC)^{-1} = C^{-1}B^{-1}A^{-1}
  \end{align*}
  \begin{block}{}
\begin{semiverbatim}
x = invert (a :- b :- c)
y = invert c :- invert b :- invert a
\alert{-- x and y are the same...}
\end{semiverbatim}
  \end{block}
\end{frame}

\subsection{Equality}

\begin{frame}[fragile]
  \frametitle{Patch equality}
  \begin{block}{}
    \begin{itemize}
    \item If two patches are \structure{equal}, then both their
      representation, initial and final states are equal.
    \item Conversely, if two of these three are true, then the third must
      be also.
    \end{itemize}
  \end{block}
  \begin{block}{We need:}
    \begin{itemize}
    \item A function that accepts two parallel patches and determines if
      they are equal by comparing their representation.
    \item A function that accepts two anti-parallel patches and determines
      if they are equal by comparing their representation.
    \end{itemize}
    \structure{Note:} Checking the representation \emph{alone} is not
    enough to guarantee equality, since non-equal patches may have the same
    representation when expressed in different contexts (e.g. ``remove the
    first line of a file'').
  \end{block}
\end{frame}

\begin{frame}[fragile]
  \frametitle{GADT witnesses and patch equality}
  \begin{block}{GADT as witness of type equality}
\begin{verbatim}
data EqCheck a b where
    NotEq :: EqCheck a b
    IsEq :: EqCheck a a
\end{verbatim}
  \end{block}
  \begin{block}{Two equality check operators}
\begin{semiverbatim}
(=\\/=) :: Patch a b -> Patch a c -> EqCheck b c
(=/\\=) :: Patch a c -> Patch b c -> EqCheck a b
    \alert{-- Implemented using unsafeCoerce# }
\end{semiverbatim}
  \end{block}
  \begin{columns}
  \begin{column}{7cm}
  \begin{block}{}
    \small
\begin{verbatim}
example ((a :- b) :\/: (a' :- c)) =
     case a =\/= a' of
     IsEq -> example2 (b :\/: c)
     ...
\end{verbatim}
  \end{block}
  \end{column}
  \begin{column}{3cm}
    \begin{block}{}
      \small \begin{equation*}
      (AB) |/ (A'C)
    \end{equation*}
    \begin{equation*}
      A = A'
    \end{equation*}
    \begin{equation*}
      B |/ C
    \end{equation*}
    \end{block}
  \end{column}
  \end{columns}
\end{frame}

\subsection{Commutation properties}

\begin{frame}[fragile]
  \frametitle{Commutation}
  \begin{block}{}
    \structure{Commutation} is both a relationship and a function, which
    reorders a pair of sequential patches.  Commutation may fail.
  \end{block}

  \begin{block}{Mathematical notation}
  \begin{columns}
    \begin{column}{2cm}
      \begin{equation*}
        A B <-> B' A'
      \end{equation*}
    \end{column}
    \begin{column}{1cm}
      or
    \end{column}
    \begin{column}{2cm}
      \begin{equation*}
        ^oA^aB^b <-> ^oB'^xA'^b
      \end{equation*}
    \end{column}
  \end{columns}
  \end{block}
  \begin{block}{Haskell notation}
\begin{verbatim}
commute :: Sequential o b -> Maybe (Sequential o b)

... do (a :- b :- c) <- abc
       b' :. a' <- commute (a :. b)
       c' :. a'' <- commute (a' :. c)
\end{verbatim}
  \end{block}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Commutation is self-inverting}
  \begin{block}{}
    Commutation---when successful---is self-inverting. 
  \end{block}
  \begin{block}{}
\begin{semiverbatim}
verify_commute (a :. b) | isJust (commute (a :. b)) =
  isJust $ do b1 :. a1 <- commute (a :. b)
              a' :. b' <- commute (b1 :. a1)
              IsEq <- a' =\\/= a
              IsEq <- b' =/\\= b \alert{-- could use =\\/=} 
\end{semiverbatim}%$
  \end{block}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Commutation of an inverse sequential pair}
  \begin{block}{}
    Commutation with the inverse of a sequential pair gives the same result
    as the inverse of the commutation of the pair.
  \end{block}
  \begin{align*}
    A B &<-> B_1 A_1\\
    B^{-1} A^{-1} &<-> A_1^{-1} B_1^{-1}
  \end{align*}
  \begin{block}{}
\begin{verbatim}
verify_commute (a :. b) | isJust (commute (a :. b)) =
    isJust $
    do b1 :. a1 <- commute (a :. b)
       ia1 :. ib1 <- commute (invert b :. invert a)
       IsEq <- b1 =\/= invert ib1
       IsEq <- a1 =\/= invert ia1
\end{verbatim}%$
  \end{block}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Commutation with patch and its inverse}
  \begin{block}{}
    Commutation with a patch and its inverse, if successful, does not alter
    a patch.  If the first commute is successful, then the other must be
    also.
  \end{block}
  \begin{align*}
    A B &<-> B_1 A_1\\
    A^{-1} B_1 &<-> B A_1^{-1}
  \end{align*}
  \begin{block}{}
\begin{verbatim}
verify_commute (a :. b) | isJust (commute (a :. b)) =
    isJust $ do b1 :. a1 <- commute (a :. b)
                b' :. ia1 <- commute (invert a :. b1)
                IsEq <- b' =\/= b
                IsEq <- invert ia1 =\/= a1
\end{verbatim}%$
  \end{block}
\end{frame}

\begin{frame}
  \frametitle{Permutivity}
  \begin{block}{}
    Permutivity is the property of the commute that means that any commuted
    permutation is uniquely defined, regardless of the order of
    commutation.
  \end{block}
  \begin{align*}
    ABC <-> A C_1 B_1 <-> C_2 A_1 B_1 <-> C_2 B_2 A_2 <-> B_3 C_3 A_2
    <-> B_3 A_3 C
  \end{align*}
  \begin{block}{}
    \begin{itemize}
    \item Ganesh has proven that if permutivity holds for \emph{any} set of
      sequence of three patches, then it holds for any sequence of $N$
      patches.
    \item Only applies to permutations that exist
    \end{itemize}
  \end{block}
\end{frame}

\section{Application:  a merge}
\subsection{ }

\begin{frame}
  \frametitle{Application:  a merge}
  \begin{block}{}
    A \structure{merge} is an operation that takes two parallel patches,
    and converts them into a pair of sequential patches.

    Commutation of the sequential pair must allow recovery of both original
    patches.
  \end{block}
  \begin{block}{}
    The merge of $A |/ B$ is
    \begin{equation*}
      AB_1 <-> BA_1
    \end{equation*}
    Using the property of commutation with a patch and its inverse:
    \begin{equation*}
      B^{-1}A <-> A_1B_1^{-1}
    \end{equation*}
    which allows us to compute the merged result using only the merge and
    invert functions.
  \end{block}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Application:  a merge}
  \begin{block}{}
    The merge of $A |/ B$ is
    \begin{equation*}
      AB_1 <-> BA_1
    \end{equation*}
    Using the property of commutation with a patch and its inverse:
    \begin{equation*}
      B^{-1}A <-> A_1B_1^{-1}
    \end{equation*}
    which allows us to compute the merged result using only the merge and
    invert functions.
  \end{block}
  \begin{block}{}
\begin{semiverbatim}
merge :: Parallel a b -> Maybe (AntiParallel b a)
\alert{-- Input is A and B, output is A_1 and B_1}
merge (a :\\/: b) =
    do a1 :. ib1 <- commute (invert b :. a)
       return (a1 :/\\: invert ib1)
\end{semiverbatim}
  \end{block}
\end{frame}

\section*{ }

\begin{frame}
  \frametitle{Conclusions}
  \emph{``The solution to every problem is to create a new GADT.''}
  \vfill
  \begin{block}{}
    \begin{itemize}
    \item Patch manipulation is lots of fun.
    \item GADTs are also lots of fun.
    \item Witness types allow us to prevent large classes of bugs.
    \end{itemize}
  \end{block}
  \vfill
  \begin{block}{Interested darcs users:}
  Meet at 1:00 outside this building for a brainstorming discussion of what
  features really ought to be added to darcs.
  \end{block}
\end{frame}

\end{document}
