negatives.tex

\documentclass[authoryear,preprint]{sigplanconf}
\usepackage{amsmath}
\usepackage{listings} 
\usepackage{stmaryrd}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{xcolor}
\usepackage{courier}
\usepackage{thmtools}
\usepackage{bbold}

%%

\newcommand{\geqz}{\geq\zerog}
\newcommand{\leqz}{\leq\zerog}
\newcommand{\zerog}{\mathbb{0}}
\newcommand{\oneg}{\mathbb{1}}
\newcommand{\twog}{\mathbb{2}}
\newcommand{\threeg}{\mathbb{3}}
\newcommand{\fourg}{\mathbb{4}}
\newcommand{\fiveg}{\mathbb{5}}
\newcommand{\bck}{\triangleleft}
\newcommand{\fwd}{\triangleright}

%%

\begin{document}
\special{papersize=8.5in,11in}
\setlength{\pdfpageheight}{\paperheight}
\setlength{\pdfpagewidth}{\paperwidth}

\newcommand{\alt}{~|~}
\lstnewenvironment{code}{\lstset{basicstyle={\sffamily\footnotesize}}}{}

\lstset{frame=none,
         language=Haskell,
         basicstyle=\sffamily, 
         numberstyle=\tiny,
         numbersep=5pt,
         tabsize=2,    
         extendedchars=true,
         breaklines=true,   
         breakautoindent=true,
         keywordstyle=\color{black},
         captionpos=b,
         stringstyle=\color{black}\ttfamily,
         showspaces=false,  
         showtabs=false,    
         framexleftmargin=2em,
         framexbottommargin=1ex,
         showstringspaces=false
         basicstyle=\sffamily,
         columns=[l]flexible,
         flexiblecolumns=true,
         aboveskip=\smallskipamount,
         belowskip=\smallskipamount,
         lineskip=-1pt,
         xleftmargin=1em,
         escapeinside={/+}{+/},
         keywords=[1]{Monad,Just,Nothing,type,data,right,left,id,where,do,
                     if,then,else,let,in},
         literate=
           {+}{{$\;+\;$}}1 
           {/}{{$/$}}1 
           {*}{{$\;*\;$}}1
           {=}{{$=\ $}}1 
           {/=}{{$\not=$}}1
           {[]}{$[\;]$}2
           {<}{{$<$}}1 
           {>}{{$>$}}1 
           {++}{{$+\!\!\!+\;$}}1 
           {::}{{$:\mkern -2.5mu:\;$}}1
           {&&}{{$\&\!\!\!\&$}}2
           {:=:}{{$:\mkern -2mu=\mkern -2mu:\;$}}3
           {:+:}{{$:\mkern -5mu+\mkern -5mu:\;$}}3
           {:-:}{{$:\mkern -5mu-\mkern -5mu:\;$}}3
           {:*:}{{$:\mkern -5mu*\mkern -5mu:\;$}}3
           {$}{{\texttt{\$}\hspace{0.5em}}}1
           {`}{$^\backprime$}1
           {==}{{$=\!=\;$}}2
           {===}{{$\equiv\;$}}2
           {->}{{$\rightarrow\;$}}2 
           {>=}{{$\geq$}}2 
           {<=}{{$\leq$}}2 
           {>=0}{{$\geq_\zerog\;$}}2 
           {<=0}{{$\leq_\zerog\;$}}2 
           {==0}{{$=_\zerog\;$}}2 
           {>0}{{$>_\zerog\;$}}2 
           {<0}{{$<_\zerog\;$}}2 
           {<-}{{$\leftarrow$}}2
           {=>}{{$\Rightarrow\;$}}2
           {<<}{{$\ll$}}2 
           {>>}{{$\gg\;$}}2
           {>>>}{{$\ggg\;$}}3 
           {<<<}{{$\lll\;$}}3
           {>>=}{{$\gg\mkern -2.5mu=\;$}}3
           {=<<}{{$=\mkern -2.5mu\ll\;$}}3
           {<|}{$\lhd\;$}2
           {<||}{$\unlhd\;$}2
           {\ ||\ }{$\|$}1
           {\\}{$\lambda$}1
           {:>}{{$\rhd$}}2
           {||>}{{$\unrhd$}}2
           {_}{{$\_$}}1
           {_B}{{$_b$}}2
           {forall}{{$\forall$}}1
}

\lstset{postbreak=\raisebox{0ex}[0ex][0ex]
        {\ensuremath{\hookrightarrow}}}
\lstset{breaklines=true, breakatwhitespace=true}
\lstset{numbers=none, numbersep=5pt, stepnumber=2, numberstyle=\scriptsize}
\lstset{rangeprefix=/*!\ , rangesuffix=\ !*\/, includerangemarker=false}

%% double-blind reviewing...
\title{Negative Types}
\authorinfo{}{}{}
\maketitle

\begin{abstract}
\ldots
\end{abstract}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{\textsc{LET}: Operational Semantics}

We introduce a toy functional language. Separate the first-order from the
higher-order component.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{$\Pi^{o}$: Operational and Denotational Semantics}

Present $\Pi^{o}$ with an interpreter specifying the operational
semantics. This is $\Pi$ with recursive types and a trace operator. (It might
be enough to have just one recursive type $\mathbb{N}$.) We know
\emph{first-order} \textsc{LET} can be translated to this language: we cannot
translate higher-order functions. That requires compact closure but we live a
plain symmetric bimonoidal category.

For a concrete model or denotational semantics that instantiates the
categorical framework, the minimum requirement is that every type maps to
some kind of space; a value $v : t$ maps to an element of that space; and a
combinator $c : t_1 \leftrightarrow t_2$ maps to a function between the
spaces denoting $t_1$ and $t_2$. The simplest model one can think of is to
map a type of size $n$ to a set of $n$ elements (including the infinite set
of $\omega$ elements; a value $v : t$ maps to an element in the set denoting
$t$; a combinator maps to a permutation on that set. One could also build
other models, e.g. vector spaces (infinite dimensional however) but that
model is fine. Perhaps show the details of the model and the correspondence
between operational and denotational semantics.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{$\Pi^{o-}$: Operational Semantics}

Extend $\Pi^{o}$ with negative types and $\eta$ and $\epsilon$. Present the
operational semantics that uses two interpreters forwards and backwards. Do
we have such a semantics that we like? 

The categorical model is now supposed to be a ring category. This is
complicated so we will work directly with a concrete model that gives us more
operational intuition. We need to map every type to some space. If type $t$
maps to space $S$, we need to have an operation that maps that space to
another space that acts like ``negative'' $S$ so that we can satisfy for
example that $S-S=0$. Using the cardinality of the set like we did for
$\Pi^{o}$ does not directly work (footnote on papers that describe sets with
negative cardinality). Another idea is to generalize spaces to have two
components (a producer and a consumer; a left player and a right player) and
to describe the space using the relative ``strength'' of the two
components. (This is the idea of the Int or G construction but that doesn't
directly work if we have two monoidal structures and needs a complicated
completion to ring categories.) A natural and beautiful theory is that of
Conway games which model two player games: left and right. In that setting we
can talk about games in which the left player has an $n$-move advantage
(summarized by the number $n$) and games in which the right player has an
$n$-move advantage (summarized by the number $-n$ which denotes that the left
player has an $n$-move disadvantage). It is therefore possible to map a type
of size $n$ where $n$ is an integer to the class Conway games where the left
player has an $n$-move (dis-)advantage; the negative of a space $S$ is the
space in which all the games are flipped with left and right players
exchanging positions; following common terminology, we call the target of the
type an \emph{arena}; a value $v : t$ maps to a \emph{strategy} for the left
player in the arena for type $t$. Combinators transform strategies. Note that
the space corresponds to type $0$ is an arena with no possible moves.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Operational Semantics}

Given that our language is reversible, a backward evaluator is relatively
straightforward to implement: using the backward evaluator to calculate
$c(v)$ is equivalent to $c^{\dagger}(v)$ in the forward evaluator.

\begin{figure*}
\[\begin{array}{rclr}
[\mathit{iso}, v, C, s]_{\bck} &\longmapsto& 
  \langle \mathit{iso}, v', C, s'\rangle_{\bck} 
  \quad\textrm{where}~\mathit{iso}^{\dagger}~s~v \longmapsto (v', s') \\
\langle c_1, v, \mathit{Fst}~C~c_2, s \rangle_{\bck} &\longmapsto& 
  \langle c_1 \fatsemi c_2, v, C, s \rangle_{\bck} \\
\langle c_2, v, \mathit{Snd}~c_1~C, s \rangle_{\bck} &\longmapsto& 
  [c_1, v, \mathit{Fst}~C~c_2, s]_{\bck} \\
[ c_1 \fatsemi c_2, v, C, s ]_{\bck} &\longmapsto& 
  [c_2, v, \mathit{Snd}~c_1~C, s]_{\bck} \\
\langle c_1, v, \mathit{LeftP}~C~c_2, s \rangle_{\bck} &\longmapsto& 
  \langle c_1 \oplus c_2, \mathit{left}~v, C \rangle_{\bck} \\
[c_1 \oplus c_2, v', C, s ]_{\bck} &\longmapsto& 
  [ c_1, v, \mathit{LeftP}~C~c_2, s[v' \approx left v] ]_{\bck} \\
\langle c_2, v, \mathit{RightP}~c_1~C, s\rangle_{\bck} &\longmapsto& 
  \langle c_1 \oplus c_2, \mathit{right}~v, C \rangle_{\bck} \\
[c_1 \oplus c_2, v', C,s ]_{\bck} &\longmapsto& 
  [ c_2, v, \mathit{RightP}~c_1~C, s[v' \approx right v] ]_{\bck} \\
\langle c_1, v_1, \mathit{LeftT}~C~c_2~v_2, s \rangle_{\bck} &\longmapsto& 
  \langle c_1 \otimes c_2, (v_1, v_2), C, s \rangle_{\bck} \\
\langle c_2, v_2, \mathit{RightT}~c_1~v_1~C, s \rangle_{\bck} &\longmapsto& 
  [ c_1, v_1, \mathit{LeftT}~C~c_2~v_2, s ]_{\bck} \\
[ c_1 \otimes c_2, v, C, s ]_{\bck} &\longmapsto& 
  [ c_2, v_2, \mathit{RightT}~c_1~v_1~C, S' ]_{\bck} 
  \quad\textrm{where}~ s' = s[v \approx (v_1, v_2)] \\
\\
\\
\langle \epsilon, v, C, s \rangle_{\fwd} &\longmapsto& 
  \langle \epsilon, \mathit{left}~(-v'), C, s[v \approx right v'] \rangle_{\bck} \\
\langle \epsilon, v, C, s \rangle_{\fwd} &\longmapsto& 
  \langle \epsilon, \mathit{right}~v', C, s[v \approx left (-v')] \rangle_{\bck} \\
\\
\\
\langle \eta, v, C, s \rangle_{\bck} &\longmapsto& 
  \langle \eta, \mathit{left}~(-v'), C, s[v \approx right v'] \rangle_{\fwd} \\
\langle \eta, v, C, s \rangle_{\bck} &\longmapsto& 
  \langle \eta, \mathit{right}~v', C, s[v \approx left (-v')] \rangle_{\fwd}
\end{array}\]
\end{figure*}

We add the following rules to the reductions above. 
\begin{enumerate}
\item The rules for $\epsilon$ essentially transfer control from the forward
  evaluator (whose states are tagged by $\triangleright$) to the backward
  evaluator (whose states are tagged by $\triangleleft$). In other words,
  after an $\epsilon$ the direction of the world is reversed. The pattern
  matching done by the unification ensures that a value on the right wire is
  tagged to be negative and transferred to the left wire, and vice versa.
  Note that there is no evaluation rule for $\eta$ in the forward
  evaluator. This corresponds to the fact that there is no value of type 0
  and hence the forward evaluator can never execute an $\eta$.

\item The rules for $eta$ are added to the backward evaluator. A program
  executing backwards starts executing forwards after the execution of the
  $\eta$. Dual to the previous case, there is no rule for $\epsilon$ in the
  backward evaluator since the output type of $\epsilon$ is 0.
\end{enumerate}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Conway Numbers: Arenas}

A Conway number is a game consisting of left and right options where each
option models a move to another game. There is another technical condition
given below that constrains every left option to be ``less than'' every right
option but that can be ignored for the moment. Players alternate taking
options and the player with no available options loses. In Haskell, ignoring
the additional technical condition, one might define the datatype of Conway
numbers as:
\begin{code}
data ConwayNumber = CN [ConwayNumber] [ConwayNumber]
\end{code}
The simplest Conway number is \lstinline|CN [] []| with empty left and right
options. We call this number $\zerog$: 
\begin{code}
/+ $\zerog$ +/  = CN  [] []
\end{code}
Once we have defined $\zerog$, we can also define the following:
\begin{code}
/+ $\oneg$ +/  = CN  [ /+ $\zerog$ +/ ]  []
/+ $\twog$ +/  = CN  [ /+ $\oneg$ +/ ]  []
/+ $\threeg$ +/  = CN  [ /+ $\twog$ +/ ]  []
\end{code}
and so on. Intuitively, the number $\mathbb{n}$ represents a game in which
the left player has an $n$-move advantage over the right player. Dually, we
can define the following numbers where the left player has $n$-move
\emph{disadvantage} over the right player:
\begin{code}
/+ -$\oneg$ +/  = CN  [] [ /+ $\zerog$ +/ ]
/+ -$\twog$ +/  = CN  [] [ /+ -$\oneg$ +/ ]
/+ -$\threeg$ +/  = CN  [] [ /+ -$\twog$ +/ ]
\end{code}
More generally, the \emph{unary negation} of a number or its \emph{dual} is
defined as follows:
\begin{code}
neg :: ConwayNumber -> ConwayNumber
neg (CN xls xrs) = 
  CN [ neg xr | xr <- xrs ] [ neg xl | xl <- xls ]
\end{code}

\smallskip\noindent\textbf{Comparing numbers.} There are three outcomes to
games represented by Conway numbers $\mathbb{n}$:
\begin{itemize}
\item $\mathbb{n} > \zerog$ which indicates that the \emph{left} player can
  enforce a win, no matter who starts;
\item $\mathbb{n} < \zerog$ which indicates that the \emph{right} player can
  enforce a win, no matter who starts;
\item $\mathbb{n} = \zerog$ which indicates that the \emph{second}
  player can enforce a win, no matter who.
\end{itemize}
For example, we have $\threeg > \zerog$ because the right player would have
no options (i.e., would lose) on the first or second turn depending on who
starts. Similarly, we have $-\threeg < \zerog$ because the left player would
have no options on on the first or second turn depending on who starts. For
$\zerog$, it is evident that the first player to take a turn must lose, i.e.,
that the second player wins. More interestingly, consider the game
$\textsf{CN}~[-\oneg]~[\oneg]$ which we claim is $= \zerog$. Indeed, if the
left player starts, the only option is to move to the game $-\oneg$ which the
right player wins. If however the right player moves first, the only option
is to move to the game $\oneg$ which the left player wins. In both cases, the
second player wins. To ensure that these three outcomes are the only possible
outcomes, Conway numbers have an additional restriction: for every left
option $x$ and right option $y$, we require that $x < y$. If that restriction
is lifted we could construct games such that $\textsf{CN}~[\zerog]~[\zerog]$
for which none of the relations $> \zerog$, $< \zerog$, or $= \zerog$
holds. Instead for this game, the first player always wins, which means that
the left player cannot enforce a win (in case the right player starts) and
vice-versa.

The formal definitions of the comparison operators are:
\begin{code}
>=0 (CN _ xrs)  = not $ or (map <=0 xrs)
<=0 (CN xls _)  = not $ or (map >=0 xls) 
==0 x           = >=0 x && <=0 x
<0 x            = <=0 x && not (>=0 x)
>0 x            = >=0 x && not (<=0 x)
\end{code}
Only $\geq_\zerog$ and $\leq_\zerog$ are fundamental. The predicate
$\geq_\zerog$ means that the left player can win as second player and
$\leq_\zerog$ means that the right player can win as second player. If the
left player can win as second player, it means that the right player has no
good opening move, i.e., that there is no right option that is $\leq_\zerog$.

Conway numbers also come equipped with addition, subtraction, and
multiplication operations defined as follows.

\smallskip\noindent\textbf{Addition and subtraction.} Addition of two games
intuitively gives each player the choice of selecting an option from either
game. Subtraction is simply the addition of the dual of a game. Formally:
\begin{code}
(:+:) :: ConwayNumber -> ConwayNumber -> ConwayNumber
x@(CN xls xrs) :+: y@(CN yls yrs) = 
  CN 
    ([ xl :+: y | xl <- xls ] `union`
     [ x :+: yl | yl <- yls ])
    ([ xr :+: y | xr <- xrs ] `union`
     [ x :+: yr | yr <- yrs ])

(:-:) :: ConwayNumber -> ConwayNumber -> ConwayNumber
x :-: y = x :+: (neg y) 
\end{code}
It is easy to check that $\zerog$ is the unit of addition and that addition
is commutative. Furthermore, adding two positive numbers like~$\twog$
and~$\threeg$ gives $\fiveg$ as desired, and similarly for two negative
numbers. When mixing positive and negative numbers, e.g., adding $\threeg$
and $-\twog$, the result appears much more complicated:
\begin{code}
CN [CN  [CN  [-/+ $\twog$ +/] 
             [CN [-/+ $\oneg$ +/] [/+ $\oneg$ +/]]]
        [CN  [CN [-/+ $\oneg$ +/] [/+ $\oneg$ +/]] 
             [/+ $\twog$ +/]]] 
   [CN  [CN  [CN [-/+ $\oneg$ +/] [/+ $\oneg$ +/]] 
             [/+ $\twog$ +/]] 
        [/+ $\threeg$ +/]]
\end{code}
We will formalize the sense in which the game above is equivalent to the game
$\oneg$, but for now we can intuitively reason as follows. We have already
seen that the game $\textsf{CN}~[-\oneg]~[\oneg]$ is equivalent to $\zerog$
which simplifies the above to:
\begin{code}
CN [CN  [CN  [-/+ $\twog$ +/] [/+ $\zerog$ +/]]
        [CN  [/+ $\zerog$ +/] [/+ $\twog$ +/]]]
   [CN  [CN  [/+ $\zerog$ +/] [/+ $\twog$ +/]]
        [/+ $\threeg$ +/]]
\end{code}
Now consider the game $\textsf{CN}~[\zerog]~[\twog]$. If the left player
starts, the game proceeds to $\zerog$ and the right player loses. If the
right player starts, the game proceeds to $\twog$ which is an even stronger
position for the left player. In other words, the right option is useless and
the right player always loses: the game is equivalent to
$\textsf{CN}~[\zerog]~[\;]$, i.e., to~$\oneg$. By a similar reasoning,
$\textsf{CN}~[-\twog]~[\zerog]$ simplifies to $-\oneg$, and the whole
expression becomes:
\begin{code}
CN [CN  [/+ -$\oneg$ +/] [/+ $\oneg$ +/]]
   [CN  [/+ $\oneg$ +/] [/+ $\threeg$ +/]]
\end{code}
The left option is equivalent to $\zerog$ and the right one is equivalent to
$\twog$, and the entire expression is equivalent to $\oneg$.

\smallskip\noindent\textbf{Multiplication.} The most complicated operation on
Conway numbers is multiplication. It is defined as follows:
\begin{code}
(:*:) :: ConwayNumber -> ConwayNumber -> ConwayNumber
x@(CN xls xrs) :*: y@(CN yls yrs) = 
  CN 
    ([ (xl :*: y) :+: (x :*: yl) :-: (xl :*: yl)
     | xl <- xls, yl <- yls] `union`
     [ (xr :*: y) :+: (x :*: yr) :-: (xr :*: yr)
     | xr <- xrs, yr <- yrs])
    ([ (xl :*: y) :+: (x :*: yr) :-: (xl :*: yr)
     | xl <- xls, yr <- yrs] `union`
     [ (xr :*: y) :+: (x :*: yl) :-: (xr :*: yl)
     | xr <- xrs, yl <- yls])
\end{code}

Conway numbers form a \emph{ring} under the semantic notion of equality
\lstinline$:=:$ defined below:
\begin{code}
(:=:) :: ConwayNumber -> ConwayNumber -> ConwayNumber
x :=: y = ==0 (x :-: y)
\end{code}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{$\Pi^{o-}$: Denotational Semantics} 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{$\Pi^{o-}$: Correspondence} 

Show correspondence between operational and denotational semantics for
$\Pi^{o-}$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Back to $\textsc{LET}$}

Now work out the full translation from \textsc{LET} to $\Pi^{o-}$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Conclusion}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\bibliographystyle{abbrvnat}
\softraggedright
\bibliography{cites}

\end{document}