\documentclass{llncs}

% DAMP'08 parameters
%   page limit: 15 pages
%   final version: 14 Dec 2008

\usepackage{amsmath}
\usepackage{version}
\usepackage{alltt}
\usepackage{url}
\usepackage{graphicx}
\usepackage{epsfig}
\usepackage{pifont}
%\usepackage{pgf,pgfarrows,pgfnodes}
\usepackage{stmaryrd}

% version control
%
\includeversion{DRAFT}
\excludeversion{DRAFT}

\def\Version{\relax}
\begin{DRAFT}%
  {
    \gdef\Version{%
      \\
      \textbf{--- DRAFT ---}\\[1ex]
      \ignorespaces}
  }
\end{DRAFT}

\renewcommand{\textfraction}{0}
\renewcommand{\topfraction}{1}
%\renewcommand{\bottomfraction}{1}
\renewcommand{\dbltopfraction}{1}
\renewcommand{\floatpagefraction}{.9}
\renewcommand{\dblfloatpagefraction}{1}

% Misc macros
%
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\comm}[1]{\textrm{--- {#1}}}
\newcommand{\inform}[1]{\ensuremath{\langle\textrm{#1}\rangle}}
\newcommand{\var}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\sub}[1]{_{\mathnormal{#1}}}
\newcommand{\lift}[1]{#1$^\uparrow$}
\newcommand{\V}[1]{#1$_{\mathrm{V}}$}
\newcommand{\SE}[1]{#1$_{\mathrm{S}}$}
\newcommand{\Arr}[1]{#1$_{\code{\pacon}}$}

\newcommand{\TT}[1]{\(\mathcal{T}\llbracket\)#1\(\rrbracket\)}
\newcommand{\VT}[1]{\(\mathcal{V}\llbracket\)#1\(\rrbracket\)}
\newcommand{\ST}[1]{\(\mathcal{S}\llbracket\)#1\(\rrbracket\)}
\newcommand{\SV}[1]{\(\mathcal{SV}\llbracket\)#1\(\rrbracket\)}
\newcommand{\SVB}[1]{\(\mathcal{SV}_B\llbracket\)#1\(\rrbracket\)}
\newcommand{\meta}[1]{\ensuremath{\llbracket\text{#1}\rrbracket}}

% Notation for type-indexed parallel arrays
%                                     This     or    this
\newcommand{\pacon}{\code{PA}}      % PA             [::]
\newcommand{\pa}[1]{\pacon\;#1}     % PA t           [:t:]
\newcommand{\paparen}[1]{(\pa{#1})} % (PA t)         [:t:]

%  pgf stuff
%
\newcommand{\mpgfrect}[4]{%
  \pgfrect[stroke]{\pgfpoint{#1}{#2}}{\pgfpoint{#3}{#4}}}
\newcommand{\mpgfline}[4]{\pgfline{\pgfpoint{#1}{#2}}{\pgfpoint{#3}{#4}}}
\newcommand{\mpgfbox}[2]{\mpgfrect{#1}{#2}{0.2cm}{0.2cm}}    

% end pgf


% TODO's
%
\newcommand{\todo}[2]{\emph{\textbf{Review #1}: #2}}
\newcommand{\TODO}[1]{\emph{\textbf{TODO:} #1}}

\begin{document}

\title{Partial Vectorisation of Haskell Programs%
  \Version}
\author{%
  Manuel M. T. Chakravarty\inst{1}\and
  Roman Leshchinskiy\inst{1}\and
  Simon Peyton Jones\inst{2}\and
  Gabriele Keller\inst{1}
}
\institute{%
  Programming Languages and Systems,
  School of Computer Science and Engineering,
  University of New South Wales,
  \email{\{chak,rl,keller\}@cse.unsw.edu.au}
  \and
  Microsoft Research Ltd,
  Cambridge, England,
  \email{simonpj@microsoft.com}
}  
\maketitle

\setcounter{footnote}{0}

\begin{abstract}
  Vectorisation for functional programs, also called the flattening
  transformation, relies on drastically reordering computations and
  restructuring the representation of data types.  As a result, it only
  applies to the purely functional core of a fully-fledged functional
  language, such as Haskell or ML.  A concrete implementation needs to apply
  vectorisation selectively and integrate vectorised with unvectorised code.
  This is challenging, as vectorisation alters the data representation, which
  must be suitably converted between vectorised and unvectorised code.  In
  this paper, we present an approach to partial vectorisation that selectively
  vectorises sub-expressions and data types, and also, enables linking
  vectorised with unvectorised modules.
\end{abstract}

\noindent\emph{Keywords:} Vectorisation; flattening; program transformation;
Haskell

\section{Introduction}
\label{sec:intro}

The idea of implementing \emph{nested data parallelism}~\cite{blelloch:ppa} in
functional programs by a vectorising program transformation is at least as old
as Blelloch \& Sabot's seminal
work~\cite{blelloch-sabot:compiling-collection,blelloch:diss} on the
\emph{flattening transformation.}  We have since generalised the basic idea
to cover the central features of modern functional languages, such as
algebraic data types, parametric polymorphism, and higher-order
functions~\cite{keller-chak:tflat,chak-keller:more-types,leshchinskiy-etal:ho-flattening}.
However, apart from a prototype that compiled a subset of Paralation Lisp, the
only complete implementation of vectorisation by flattening was, to the best
of our knowledge, the experimental NESL
system~\cite{blelloch-etal:impl-nested-parallel}.  Due to its experimental
nature, NESL was a rather limited functional language; for example, it did not
admit user-defined algebraic data types and higher-order
functions, had only rudimentary I/O, and did not have a module system or
support separate compilation.  In fact, NESL was implemented as a
whole program compiler that vectorised the entire program.

In our implementation of vectorisation in the Glasgow Haskell Compiler (GHC)
as part of the \emph{Data Parallel Haskell project}~\cite{chak-etal:DPH}, we
cannot follow NESL's approach.  We expect that a real application will consist
of a computationally-intensive core that must be vectorised, embedded
in a larger program that parses its command line, reads configuration files, 
drives a GUI, outputs Postscript, and so on.  None of this surrounding code
can or should be vectorised.  

% Haskell is equipped with a module system, and
% GHC supports separate compilation and binary-only libraries.  Hence, we cannot
% reasonably expect that all modules of a program have been compiled with
% vectorisation.  What is worse, even for a single module we may not be able to
% vectorise all code.  Vectorisation relies on drastically reordering
% computations and restructuring the representation of data types.  This is fine
% for Haskell's purely functional core, but it is not suitable for impure
% language features, such as monadic I/O and mutable variables, exceptions,
% thread-based concurrency, and calls to external C code.  
Consequently, we need
a form of \emph{selective} vectorisation that vectorises as much as possible,
but leaves sub-expressions that depend on impure features, or unvectorised
external code as is.  Moreover, we must integrate vectorised with
unvectorised code, which is challenging because vectorisation alters the 
representation of data structures and functional values; hence, values need
to be suitably converted when passed between vectorised and unvectorised code.

This paper makes the following technical contributions:
%
\begin{itemize}
\item We give the first presentation of a \emph{selective vectorisation transformation}
  that only vectorises
  sub-expressions that do not rely on impure or otherwise non-vectorisable
  features and in particular on external, unvectorised data structures and
  code (Section~\ref{sec:precisely}).
\item We describe the integration of vectorised and unvectorised modules and
  the additional information that vectorisation requires to be maintained
  across separately compiled modules (Section~\ref{sec:modules}).
\end{itemize}
%
Before we dive into these technical details, Section~\ref{sec:vectorisation}
summarises the main ideas of vectorisation and introduces our approach by
example.  We cover related work in Section~\ref{sec:related}.


\section{Vectorisation in a nutshell}
\label{sec:vectorisation}

The various aspects of vectorising purely functional programs including
algebraic data types, parametric polymorphism, and higher-order functions were
described in detail in previous
work~\cite{keller-chak:tflat,chak-keller:more-types,leshchinskiy-etal:ho-flattening,chak-etal:DPH}.
In the following, we summarise the core ideas with a concrete example.
Afterwards, we motivate and informally illustrate the main ideas of the
present paper by extending our example to include I/O.

\subsection{Data Parallel Haskell}

\begin{figure}[tbp]
  \centering
\begin{alltt}
type Vector   = (Float, Float)
type Area     = (Vector, Vector)

data MassPnt  = MassPnt \{ mass :: Float, location :: Vector \}
data Particle = Particle \{ center :: MassPnt, velocity :: Vector \}

data Tree = Node MassPnt [:Tree:]   \comm{Rose tree for spatial decomposition}

\comm{Perform spatial decomposition and build the quadtree}
buildTree :: [:MassPnt:] -> Tree

\comm{Change velocity of each particle in \code{ps} according to force affected by masses in tree}
accelerate :: Tree -> [:Particle:] -> [:Particle:]

\comm{Move a mass center according to the given velocity}
movePnt :: MassPnt -> Vector -> MassPnt

\comm{Move a particle according to its velocity}
moveParticle :: Particle -> Particle
moveParticle p = let v = velocity p
                 in Particle (movePnt (center p) v) v

\comm{Compute one step of the n-body simulation}
oneStep :: Float -> [:Particle:] -> [:Particle:]
oneStep ps
  = [: moveParticle p | p <- accelerate tree ps :]
  where
    mps   = [:mp | Particle mp v <- ps:]
    tree  = buildTree mps
\end{alltt}  
  \caption{Excerpt of 2-D Barnes-Hut $n$-body code}
  \label{fig:bh}
\end{figure}
%
Data Parallel Haskell (DPH) introduces a type of \emph{parallel arrays},
denoted \code{[:e:]} for arrays of type \code{e}, together with a large number
of parallel collective operations.  As far as possible, these
operations have the same names as Haskell's standard list functions, but with a
\code{P} suffix added---i.e., \code{mapP}, \code{filterP}, \code{unzipP}, and
so forth. The language also includes parallel array comprehensions
which are similar to list comprehensions but operate on parallel arrays. Details
of the language extension and examples are in~\cite{chak-etal:haskell-ndp}.

The crucial difference between Haskell lists and parallel arrays is that the
latter have a parallel evaluation semantics.  More precisely, demand for any
element of a parallel array results in the evaluation of all elements---in
particular, on a parallel machine, we expect the evaluation of these elements
to happen in parallel.  Figure~\ref{fig:bh} gives an excerpt from a
two-dimensional Barnes-Hut $n$-body simulator, an example that we chose
because it is both computationally intensive and very hard to express using
flat data parallelism.  The parallelism happens inside \code{oneStep}, where
all particles are processed in a single parallel step and where the main
workhorses \code{buildTree} and \code{accelerate} (which, in turn, contain
parallel computations) are invoked.  The function \code{buildTree} constructs
a quad-tree and \code{accelerate} uses it to compute the acceleration of a set
of particles in \(O(n \log n)\) work complexity.  All this needs to be
vectorised for parallel execution.  More precisely, we need to ensure that we
call the fully vectorised variants of the functions \code{\V{buildTree}},
\code{\V{accelerate}}, and \code{\V{moveParticle}}, to achieve \(O(\log^2 n)\)
parallel step complexity; details are
in~\cite{barnes-hut:nbody,keller-chak:tflat,chak-etal:haskell-ndp}.




% \begin{verbatim}
% accels :: Tree MassPnt -> Float -> [:MassPnt:] -> [:Accel:]
% accels (Node crd ts) len mps  = 
%   let 
%     farAcs     = [accel crd mp | mp <- mps, isFar len crd mp]
%     closeMps   = [mp | mp <- mps, not (isFar len crd mp)]
%     closeAcss  = [accels t (len / 2) closeMps | t <- ts]
%     closeAcs   = [superimp oneMpAcs | oneMpAcs <- transpose closeAcss]
%   in
%   combine direct farAcs closeAcs
% \end{verbatim}

% \begin{alltt}
% iter :: Int -> [Particle] -> IO [Particle]
% iter 0 ps = return ps
% iter n ps = 
%   do
%     ps' <- oneStep dt ps
%     iter (n - 1) ps'
% \end{alltt}


\subsection{Full vectorisation and why it may fail}
\label{sec:full-vect}

Consider a top-level function definition \code{\var f::\var t = \var e},
where \code{\var t} is the (monomorphic) type of \code{\var f}.  
The \emph{full vectorisation} transformation generates a new variant of
\code{\var f}, thus:
%
\begin{quote}
\begin{alltt}
\V{\var{f}} :: \TT{\var{t}} = \VT{\var{e}}   \comm{If \code{\var{e}} is vectorisable}
\end{alltt}
\end{quote}
%
Here, \code{\V{\var f}} is the \emph{fully vectorised} variant of \code{\var
  f}, whose right-hand side is generated by the \emph{full vectorisation
  transform} \VT{\(\cdot\)}.  Full vectorisation returns an expression of a
different type to the input, so the type of \code{\V{\var f}} is obtained by
vectorising the type \code{\var t}, thus \code{\TT{\var t}}.  In general, if
\code{\var e::\var t} then \code{\VT{\var e}::\TT{\var t}}.

Full vectorisation is the flattening transformation of Blelloch and Sabot,
subsequently elaborated by ourselves to handle polymorphism, user-defined algebraic
data types, and higher-order functions~\cite{keller-chak:tflat,chak-keller:more-types,leshchinskiy-etal:ho-flattening}.  It is, however, not the subject
of this paper, so we will keep details of full vectorisation to a minimum.


% 
% 
% Vectorisation affects both data structure declarations and function
% definitions.  Foremost, vectorisation generates for every function of type
% \code{f :: a -> b}, a \emph{lifted variant} of type \code{\lift f ::
%   [:a:] -> [:b:]}. 
% %
% % Ignoring currying for the
% % moment, the data parallel variant of addition \code{(+) :: Num a => a -> a -> a}
% % is elementwise addition of arrays \code{(\lift+) :: Num a => [:a:] -> [:a:] ->
% % [:a:]}.  
% % 
% % We call the data parallel variant of a function also
% % \emph{lifted} and the process of generating it \emph{lifting}. 
% In the first-order case, we can lift a function definition \code{f = e} 
% simply by replacing all functions in \code{e} with their lifted
% variants. For instance, \code{moveParticle} from Figure~\ref{fig:bh} is lifted
% to
% %
% \begin{quote}
% \begin{alltt}
% \lift{moveParticle} :: [:Particle:] -> [:Particle:]
% \lift{moveParticle} ps
%   = let vs = \lift{velocity} ps
%     in \lift{Particle} (\lift{movePnt} (\lift{center} ps) vs) vs
% \end{alltt}
% \end{quote}
% %
% In addition, all uses of a function in a parallel context --- that is, in an
% array comprehension --- are replaced by calls to its
% lifted variant, making use of the fact the \code{mapP f = \lift{f}}. For
% example, the main expression of \code{oneStep} essentially becomes
% \code{\lift{moveParticle} (accelerate tree ps)}.
% 
% For the purposes of the rest of
% the paper, it is sufficient to know that the \emph{fully-vectorised} form of a function \code{f}
% is a pair of the regular and lifted variant of \code{f}.  We use a
% subscript ``V'' to indicate the fully-vectorised version of a function,
% so that the fully vectorised version of \code{moveParticle} looks like this:
% %
% \begin{quote}
% \begin{alltt}
% \V{moveParticle} :: (Particle->Particle, [:Particle:]->[:Particle:])
% \V{moveParticle} = (moveParticle, \lift{moveParticle})
% \end{alltt}
% \end{quote}
% %
% We extend the subscript notation to expressions 
% \code{e}, whose fully-vectorised version is denoted by \code{\V e}. 
% 
% \subsection{Transforming data structures}
% \label{sec:trans-dt}
% 
% \begin{figure}[tbp]
%   \begin{pgfpicture}{0cm}{0cm}{12cm}{3cm}
% %     \mpgfline{0cm}{1cm}{12cm}{1cm}
% %     \mpgfline{0cm}{2cm}{12cm}{2cm}
% %     \mpgfrect{0cm}{0cm}{12cm}{3cm}
% 
% %     \mpgfline{1cm}{0cm}{1cm}{3cm}
% %     \mpgfline{2cm}{0cm}{2cm}{3cm}
% %     \mpgfline{3cm}{0cm}{3cm}{3cm}
% %     \mpgfline{4cm}{0cm}{4cm}{3cm}
% %     \mpgfline{5cm}{0cm}{5cm}{3cm}
% 
%     % boxes 
% 
%     \mpgfbox{1cm}{2.5cm}
%     \mpgfbox{1.6cm}{2.5cm}
%     \mpgfbox{2.3cm}{2.5cm}
%     \mpgfbox{3.1cm}{2.5cm}
% 
%     % arrows 
%     \pgfsetendarrow{\pgfarrowsingle}
% 
%     \mpgfline{1cm}{2.5cm}{0.9cm}{2cm}
%     \mpgfline{1.2cm}{2.5cm}{1.3cm}{2cm}
% 
%     \mpgfline{1.7cm}{2.5cm}{1.7cm}{2cm}
% 
%     \mpgfline{2.3cm}{2.5cm}{2.1cm}{2cm}
%     \mpgfline{2.4cm}{2.5cm}{2.4cm}{2cm}
%     \mpgfline{2.5cm}{2.5cm}{2.7cm}{2cm}
%     
%     \mpgfline{3.1cm}{2.5cm}{3.0cm}{2cm}
%     \mpgfline{3.3cm}{2.5cm}{3.4cm}{2cm}
% 
%     % boxes
% 
%     \mpgfbox{0.8cm}{1.8cm}
%     \mpgfbox{1.2cm}{1.8cm}
%     \mpgfbox{1.6cm}{1.8cm}
%     \mpgfbox{2.0cm}{1.8cm}
%     \mpgfbox{2.3cm}{1.8cm}
%     \mpgfbox{2.6cm}{1.8cm}
%     \mpgfbox{2.9cm}{1.8cm}
%     \mpgfbox{3.3cm}{1.8cm}
% 
%     % arrows
% 
%     \mpgfline{0.9cm}{1.8cm}{0.9cm}{1.3cm}    
%     \mpgfline{1.6cm}{1.8cm}{1.5cm}{1.3cm}    
%     \mpgfline{1.8cm}{1.8cm}{1.9cm}{1.3cm}    
%     \mpgfline{2.4cm}{1.8cm}{2.4cm}{1.3cm}    
%     \mpgfline{2.7cm}{1.8cm}{2.7cm}{1.3cm}    
%     \mpgfline{3.4cm}{1.8cm}{3.4cm}{1.3cm}    
% 
%     % boxes
%     \mpgfbox{0.8cm}{1.1cm}
%     \mpgfbox{1.4cm}{1.1cm}
%     \mpgfbox{1.8cm}{1.1cm}
%     \mpgfbox{2.3cm}{1.1cm}
%     \mpgfbox{2.6cm}{1.1cm}
%     \mpgfbox{3.3cm}{1.1cm}
% 
% 
%     \pgfputat{\pgfxy(0.7,2.5)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(1.3,2.5)}{\pgfbox[center,base]{\texttt{,}}}
%     \pgfputat{\pgfxy(2.0,2.5)}{\pgfbox[center,base]{\texttt{,}}}
%     \pgfputat{\pgfxy(2.8,2.5)}{\pgfbox[center,base]{\texttt{,}}}
%     \pgfputat{\pgfxy(3.6,2.5)}{\pgfbox[center,base]{\texttt{]}}}
% 
%     % end tree 
% 
% 
% 
%     % flat structure
%     % l1
%     \mpgfbox{6.5cm}{2.5cm}
%     \mpgfbox{7.4cm}{2.5cm}
%     \mpgfbox{8.3cm}{2.5cm}
%     \mpgfbox{9.2cm}{2.5cm}
% 
%     \pgfputat{\pgfxy(6.3,2.5)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(7.1,2.5)}{\pgfbox[center,base]{\texttt{,}}}
%     \pgfputat{\pgfxy(8.0,2.5)}{\pgfbox[center,base]{\texttt{,}}}
%     \pgfputat{\pgfxy(8.9,2.5)}{\pgfbox[center,base]{\texttt{,}}}
%     \pgfputat{\pgfxy(9.7,2.5)}{\pgfbox[center,base]{\texttt{]}}}
% 
%     %l2
%     \pgfputat{\pgfxy(6.15,1.8)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(6.25,1.8)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(6.95,1.8)}{\pgfbox[center,base]{\texttt{]}}}
%     \pgfputat{\pgfxy(7.1,1.8)}{\pgfbox[center,base]{\texttt{,}}}
% 
%     \mpgfbox{6.35cm}{1.8cm}
%     \mpgfbox{6.65cm}{1.8cm}
%         
%     \pgfputat{\pgfxy(7.3,1.8)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(7.7,1.8)}{\pgfbox[center,base]{\texttt{]}}}
%     \pgfputat{\pgfxy(7.8,1.8)}{\pgfbox[center,base]{\texttt{,}}}
% 
%     \mpgfbox{7.4cm}{1.8cm}
% 
%     \pgfputat{\pgfxy(7.9,1.8)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(8.9,1.8)}{\pgfbox[center,base]{\texttt{]}}}
%     \pgfputat{\pgfxy(8.975,1.8)}{\pgfbox[center,base]{\texttt{,}}}
%     \mpgfbox{8cm}{1.8cm}
%     \mpgfbox{8.3cm}{1.8cm}
%     \mpgfbox{8.6cm}{1.8cm}
% 
%     \pgfputat{\pgfxy(9.05,1.8)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(9.75,1.8)}{\pgfbox[center,base]{\texttt{]}}}
%     \pgfputat{\pgfxy(9.85,1.8)}{\pgfbox[center,base]{\texttt{]}}}
%     \mpgfbox{9.15cm}{1.8cm}
%     \mpgfbox{9.45cm}{1.8cm}
% 
%     %l3
%     \pgfputat{\pgfxy(-0.4,0)}{
%     \pgfputat{\pgfxy(6.15,1.1)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(6.25,1.1)}{\pgfbox[center,base]{\texttt{[}}}
%     
%     \mpgfbox{6.35cm}{1.1cm}
%      \pgfputat{\pgfxy(6.65,1.1)}{\pgfbox[center,base]{\texttt{]}}}
%      \pgfputat{\pgfxy(6.75,1.1)}{\pgfbox[center,base] {\texttt{,}}}
%      \pgfputat{\pgfxy(6.85,1.1)}{\pgfbox[center,base]{\texttt{[}}}
%      \pgfputat{\pgfxy(7.05,1.1)}{\pgfbox[center,base]{\texttt{]}}}
%      \pgfputat{\pgfxy(7.15,1.1)}{\pgfbox[center,base] {\texttt{,}}}
%      \pgfputat{\pgfxy(7.25,1.1)}{\pgfbox[center,base] {\texttt{[}}}
%     \mpgfbox{7.35cm}{1.1cm}    
%      \pgfputat{\pgfxy(7.65,1.1)}{\pgfbox[center,base] {\texttt{,}}}
%     \mpgfbox{7.75cm}{1.1cm}    
%      \pgfputat{\pgfxy(8.05,1.1)}{\pgfbox[center,base] {\texttt{]}}}
%      \pgfputat{\pgfxy(8.15,1.1)}{\pgfbox[center,base] {\texttt{,}}}
% 
%      \pgfputat{\pgfxy(8.25,1.1)}{\pgfbox[center,base]{\texttt{[}}}
%      \pgfputat{\pgfxy(8.45,1.1)}{\pgfbox[center,base]{\texttt{]}}}
% 
%      \pgfputat{\pgfxy(8.55,1.1)}{\pgfbox[center,base] {\texttt{,}}}
%      \pgfputat{\pgfxy(8.65,1.1)}{\pgfbox[center,base] {\texttt{[}}}
%     \mpgfbox{8.75cm}{1.1cm}    
%      \pgfputat{\pgfxy(9.05,1.1)}{\pgfbox[center,base] {\texttt{]}}}
% 
% 
%      \pgfputat{\pgfxy(9.15,1.1)}{\pgfbox[center,base] {\texttt{,}}}
%      \pgfputat{\pgfxy(9.25,1.1)}{\pgfbox[center,base] {\texttt{[}}}
%     \mpgfbox{9.35cm}{1.1cm}    
%      \pgfputat{\pgfxy(9.65,1.1)}{\pgfbox[center,base] {\texttt{]}}}
%      \pgfputat{\pgfxy(9.75,1.1)}{\pgfbox[center,base] {\texttt{,}}}
% 
%      \pgfputat{\pgfxy(9.85,1.1)}{\pgfbox[center,base]{\texttt{[}}}
%      \pgfputat{\pgfxy(10.05,1.1)}{\pgfbox[center,base]{\texttt{]}}}
% 
%      \pgfputat{\pgfxy(10.15,1.1)}{\pgfbox[center,base] {\texttt{,}}}
%      \pgfputat{\pgfxy(10.25,1.1)}{\pgfbox[center,base] {\texttt{[}}}
%     \mpgfbox{10.35cm}{1.1cm}    
%      \pgfputat{\pgfxy(10.65,1.1)}{\pgfbox[center,base] {\texttt{]}}}
%      \pgfputat{\pgfxy(10.75,1.1)}{\pgfbox[center,base] {\texttt{]}}}}
% 
%     %l4
%     \pgfputat{\pgfxy(0.5,0)}{
%     \pgfputat{\pgfxy(6.15,0.4)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(6.25,0.4)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(6.45,0.4)}{\pgfbox[center,base]{\texttt{]}}}
%     \pgfputat{\pgfxy(6.55,0.4)}{\pgfbox[center,base]{\texttt{,}}}
% 
%     \pgfputat{\pgfxy(6.65,0.4)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(6.85,0.4)}{\pgfbox[center,base]{\texttt{]}}}
%     \pgfputat{\pgfxy(6.95,0.4)}{\pgfbox[center,base]{\texttt{,}}}
% 
%     \pgfputat{\pgfxy(7.05,0.4)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(7.25,0.4)}{\pgfbox[center,base]{\texttt{]}}}
%     \pgfputat{\pgfxy(7.35,0.4)}{\pgfbox[center,base]{\texttt{,}}}
% 
%     \pgfputat{\pgfxy(0.4,0)}{
%     \pgfputat{\pgfxy(7.05,0.4)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(7.25,0.4)}{\pgfbox[center,base]{\texttt{]}}}
%     \pgfputat{\pgfxy(7.35,0.4)}{\pgfbox[center,base]{\texttt{,}}}
% }
% 
%     \pgfputat{\pgfxy(0.8,0)}{
%     \pgfputat{\pgfxy(7.05,0.4)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(7.25,0.4)}{\pgfbox[center,base]{\texttt{]}}}
%     \pgfputat{\pgfxy(7.35,0.4)}{\pgfbox[center,base]{\texttt{,}}}
%   }
%     \pgfputat{\pgfxy(1.2,0)}{
%     \pgfputat{\pgfxy(7.05,0.4)}{\pgfbox[center,base]{\texttt{[}}}
%     \pgfputat{\pgfxy(7.25,0.4)}{\pgfbox[center,base]{\texttt{]}}}
%     \pgfputat{\pgfxy(7.35,0.4)}{\pgfbox[center,base]{\texttt{]}}}
%   }}
% 
% \pgfsetlinewidth{0.8pt}
% \mpgfline{4cm}{1.75cm}{5.5cm}{1.75cm}    
%   \end{pgfpicture}
%   \caption{Value of type \code{[:Tree:]} and its vectorised representation}
%   \label{fig:tree-vect}
% \end{figure}
% %
% \TODO{This subsection is entirely opaque!  It needs examples. 
% Can we simply write down the type transformation}
% 
% It should be clear that the vectorisation of a typed
% expression \code{e} of type \code{t}, gives us a vectorised expression \code{\V e} 
% with a transformed type, which we write \code{\V t}.  
% This transformation of types is not
% only due to the change of \emph{function} representation, but also caused by
% the vectorisation of \emph{data structures}
% whenever parallel arrays are involved.  This is to improve locality of
% memory access during array traversals and to facilitate load balancing on parallel
% systems~\cite{keller-chak:dtypes,chak-keller:afp-arrays,chak-etal:DPH}.
% 
% To get an intuition of the data structure transformation, consider the
% definition of rose trees \code{Tree} in Figure~\ref{fig:bh}.  The
% children of a tree node are stored in a parallel array to enable
% parallel tree traversals.  However, it is challenging to ensure load
% balancing in highly irregular trees, and Barnes-Hut trees are usually
% irregular.  Vectorisation transforms an array of irregular trees into
% a flat array containing the root nodes of the original trees, and a
% sequence of nested arrays as illustrated in
% Figure~\ref{fig:tree-vect}, where the $n$th segment contains all the
% child nodes of the $n$th element of the previous level.  Tree
% construction by the functions \code{buildTree} and tree traversal by
% \code{accelerate} then proceed level by level with all nodes on one
% level being processed in parallel.
% 
% In the same way as the vectorisation of expressions includes the generation of
% a vectorised version \code{\V f} of a function \code{f}, the vectorisation of
% types includes the generation of a vectorised version \code{\V{Tree}} of
% \code{Tree}. 

\begin{figure}[tbp]
  \centering
\begin{alltt}
oneStepIO :: [:Particle:] -> IO [:Particle:]
oneStepIO ps
  = do \{ print qs; return qs \}        \comm{Side effecting I/O computation}
  where
    mps  = [:mp | Particle mp v <- ps:]  \comm{purely functional code\ldots}
    tree = buildTree mps                 \comm{\ldots{}that must be\ldots}
    qs   = [: moveParticle p             \comm{\ldots{} vectorised and\ldots}
            | p <- accelerate tree ps:]  \comm{\ldots{} run in parallel}
\end{alltt}  
  \caption{Parallel code mixed with I/O}
  \label{fig:bh-oneStep}
\end{figure}
%
In real programs, however, full vectorisation of the entire program may be neither
possible, nor even desirable.
Haskell\footnote{Here we mean the extension of Haskell 98 implemented
  by GHC, which has many additional features that will be in the next
  standard.  Nevertheless, already Haskell 98 supports a range of I/O
  operations.} supports a significant number of impure features, including
monadic I/O and mutable variables, exceptions, thread-based concurrency, and
calls to external C code.  Code using these impure features resists
vectorisation due to such code's dependence on a particular evaluation order.

As an example, consider the code in Figure~\ref{fig:bh-oneStep} which extends
the original \code{oneStep} with a call to the I/O function
%
\begin{quote}
\begin{verbatim}
print :: Show a => a -> IO ()
\end{verbatim}
\end{quote}
%
which prints values to the standard output. Its purpose here is to output the
state of simulated particles after
each time step, for example, to drive an animation.
We cannot vectorise the entire body of \code{oneStepIO} \emph{because we do
not have a vectorised version of \code{\upshape print}}.  In all
likelihood, the module \code{System.IO}, which exports \code{print}, will not
have been compiled with vectorisation in the first place, since
vectorising it would be pointless. But even if we tried to vectorise
\code{System.IO}, we would still not get \code{\V{print}} 
because of this function's dependence on sequential C procedures.  
In short, the full vectorisation transform \code{\VT{\var e}} may \emph{fail}.
It may fail because it encounters some
impure feature in \code{\var e} that prevents vectorisation; or because
\code{\var e} mentions some imported function \code{\var f} that was compiled
without vectorisation, or for which vectorisation failed. In the latter case,
no binding for \code{\V{\var f}} would have been created.
%The binding for \code{\V{\var f}} is created only if \code{\VT{\var e}} succeeds.
%    SLPJ: adds little
% In our example, the absence of \code{\V{print}} is crucial to
% determining that the subexpression \code{print qs} of
% \code{oneStepIO}'s body will not be vectorised.

\subsection{Selective vectorisation}
\label{sec:sel-vect}

We cannot vectorise the whole of \code{oneStep}, but we still want to
selectively vectorise \emph{as much of it as possible}, so that the code
computing the new particles is evaluated in parallel (the \code{where} clause
in Figure~\ref{fig:bh-oneStep}).  In general, for each top-level binding
\code{\var f::\var t = \var e} we apply the \emph{selective vectorisation
  transform} \ST{\(\cdot\)} to \code{\var e}, thus:
%
\begin{quote}
\begin{alltt}
\var{f} :: \var{t} = \ST{\var{e}}
\end{alltt}
\end{quote}
%
In contrast to full vectorisation, selective vectorisation keeps the result
type the same---if necessary by introducing suitable conversions.  This is
exactly what happens with \code{oneStepIO}, for example.

In fact, even if we \emph{are} able to fully vectorise \code{\var f}, we must
still retain a binding of name and type \code{\var f::\var t}.  After all,
\code{\var f} might be exported and used by a module not compiled with
vectorisation or used in a context that we cannot vectorise.
%or \code{\var f} might be used in a context that we cannot
% vectorise and where we also do not have \code{fromV} at type \code{\var t}.
To keep matters simple and predictable, we therefore generate the binding
\code{\var f::\var t = \ST{\var e}} regardless of whether or not full
vectorisation succeeds.

\subsubsection{Conversions.}
%
The selective vectorisation transform should vectorise the pure,
performance-critical part of \code{oneStepIO} and get \code{\V{qs} ::
  \TT{[:Particle:]}}. This means that although we cannot vectorise \code{print
  qs}, we still want to use \code{\V{qs}} as the argument to \code{print}.
But the types do not match!  So we must convert from \code{\TT{[:Particle:]}}
to \code{[:Particle:]} using the (overloaded) function \code{fromV}.  Thus,
selective vectorisation of \code{oneStepIO} should turn \code{print qs} into
\code{print (fromV \V{qs})}.

The functions \code{fromV} and \code{toV} marshal arguments and results ``across
the border'' between un-vectorised and vectorised code.
The selective vectorisation transform generates suitable \code{fromV} and
\code{toV} functions, based on the types to be marshaled.
However, this is neither
possible nor desirable for all types---for complicated types it is simply too
expensive.  Hence, selective vectorisation decides which sub-expressions to
vectorise, using both
\begin{itemize}
\item the
presence or absence of vectorised versions \code{\V{f}} of the free
variables \code{f} of the expression, and
\item the presence or absence of conversion functions \code{fromV} and
\code{toV} at the required types (i.e., the types of the free variables and
result).
\end{itemize}
We formalise this idea in Section~\ref{sec:expressions}.

\subsubsection{Optimality.}
%
In general, there is more than one way to selectively vectorise a given
expression.  This raise the question of which of multiple translations to
choose, and especially, whether one translation is ``better'' than the others.
Unfortunately, these questions are not easy to answer as we have two
potentially opposing requirements.  On one hand, we want to vectorise as much
code as possible---after all, only vectorised code will make good use of
parallelism.  On the other hand, the use of the conversion functions
\code{fromV} and \code{toV} can be expensive if large data structures are
converted, especially if that happens repeatedly in a recursive function.  We
leave a detailed analysis of this trade off and the development of a cost
model or a heuristic approach to decide on which sub-expression to vectorise
for future work.  The transformation formalised in the next section simply
attempts to vectorise as many sub-expression as possible.  However, some
guidance by the programmer is possible as the transformation does not assume
that conversions are available for all types; i.e., by not having conversions
for types inhabited by values that may be costly to convert (e.g., complex
tree structures), programmers can indirectly guide selective vectorisation.


% ---------------------------------------------------------------------
\section{Selective vectorisation precisely}
\label{sec:precisely}

% \TODO{What can we do about the following referee comment:
% Also, I found some of the formalisations provided in the paper not overly
% satisfying.  Some notation is used with very little explanation. When paired
% with unusual extensions such as you syntactic categories in Fig.3  and other
% oddities of it such as the introduction of $f$ and $v$ without further use,
% or the different notations for non-terminals, readability does suffer a lot.
% Another example is the formalisation of the key contribution itself, i.e.,
% the partial vectorisation. It appears to be a bit ad-hoc. The naming of the
% schemes is less then intuitive and some of the textual as well as some of the
% formal omissions make it difficult to follow the details.  I am sure that
% some more brushing on these parts would improve the readability of it a lot.}

Our description of selective vectorisation has been entirely informal
thus far.  In the rest of the paper we give a more precise description.  The
presentation is based on our earlier
work~\cite{leshchinskiy:diss,leshchinskiy-etal:ho-flattening}, where
we introduced vectorisation as a \emph{total} transformation on a
source language that included only vectorisable constructs, types, 
and primitive functions.  
In what follows we show how to extend this work to a source language
that does not have this convenient property.
We do this by
specifying a \emph{partial} transformation that may fail for some
expressions, and by precisely characterising which parts of an
expression are vectorised, and which are not.  Our implementation
uses a particular source language 
--- namely, GHC's Core
language~\cite{peyton-jones-santos:trafo-optim} --  
but our method will work for \emph{any} language.

In the following, we use double square brackets \(\llbracket\cdot\rrbracket\)
not only to denote source code fragments that are transformed by one of our
transformation functions (i.e., to denote source code ``arguments''), but also
for the source code ``results'' of these transformation functions.  In other
words, we use \(\llbracket\cdot\rrbracket\) much like quasi-quotes in 
meta-programming systems, such as Template Haskell.

We will consider only \emph{monomorphic} programs.  Our system
is quite capable of handling polymorphism (and must do so for Haskell), but
polymorphism adds complications that distract from the main point of this
paper, which is partial vectorisation.

\begin{figure}[tbp]
  \centering
  \[
  \begin{array}[t]{lclcll}
    \code{Binding} &{}\ni{}&\mathit{bnd}&{}\to{}& x~\code{::}~t~\code=~e \\
     \code{Type} &{}\ni{} & t & {}\to{} & 
        T \;\mid\; t_1 \; t_2 \\
%     \\
    \code{Expr} &{}\ni{}&e&{}\to{}& v \\
                &       & &{}\mid{}& \char"5C v~\code{->}~e \\
                &       & &{}\mid{}& e_1~e_2 \\
                &       & &{}\mid{}& \code{let}~\mathit{bnd}~\code{in}~e \\
                &       & &{}\vdots{}&  \\
%     \\
%     \code{Var} &{}\ni{}&x,v&{}\to{}& \inform{variable} \\
  \end{array}
  \qquad
  \begin{array}[t]{lclll}
    f,x,v&{}\to{}& \inform{variable} \\
    T&{}\to{}&  \code{(->)}~\mid~\code{[::]}&~\text{--- built in}\\
     &\mid   & \inform{type constructor} &~\text{--- defined}
  \end{array}
  \]
  \vspace*{-1\bigskipamount}
  \caption{Fragment of GHC's Core intermediate language}
  \label{fig:syntax}
\end{figure}
%
Figure~\ref{fig:syntax} displays the fragment of Core that is relevant for the
present paper.  The left-hand side column gives the names for the syntactic
categories that we use in the following to give type signatures to translation
schemes.

\subsection{Vectorising types} \label{sec:vec-arr-ty}

In general, if \code{\var e::\var t} then \code{\VT{\var e}::\TT{\var t}}.  In
such situations it is usually illuminating to look at the type transform
first. There is one case for each form of type in Figure~\ref{fig:syntax}\footnote{
We use Haskell's guard notation here.  The guard ``{\tt | \inform{\code{\V{T}} exists}}''
means ``this equation applies only if \code{\V{T}} exists''.}:
%
\begin{quote}
\begin{alltt}
\TT{\(\cdot\)} :: Type -> Type
\TT{(->)}          = (:->)
\TT{[::]}          = PA
\TT{T} | \inform{\code{\V{T}} exists} = \V{T}
\TT{\var{t\sub1} \var{t\sub2}}          = \TT{\var{t\sub1}} \TT{\var{t\sub2}}
\end{alltt}
\end{quote}
%
The type transform simply replaces functions (\code{->}) with
vectorised functions (\code{:->}), and arrays (\code{[::]}) with vectorised
arrays (\code{\pacon}), and other data types \code{T} with a vectorised
version of that type, \code{\V{T}}. 

In general, like the term transform, the type transform is \emph{partial}: given a
type constructor \code{T}, \code{\TT{T}} fails if \code{\V T} does not exist.
There are two cases to consider: either \code{T} is a \emph{primitve} type, or it is 
an \emph{algebraic data type}, which we consider next in turn.

% Unlike the term transform, we don't wrap the result of
% the transform in a \code{Maybe}.  This keeps the rest of the presentation
% slightly simpler and it is an invariant of the overall transformation that we
% use \code{\TT{T}} only if it is defined.

\paragraph{Primitive types.}  For some primitive
types, such as \code{Int}, the vectorised version is the same as the ordinary
version; that is, \code{\V{Int}} = \code{Int}.  But for other primitive types,
there might \emph{be} no vectorised version; for example \code{\TT{IO}} fails,
because there is no vectorised version \code{\V{IO}} of Haskell's IO monad.


\paragraph{User-defined algebraic data types.}
Suppose \code{T} is a user-defined algebraic data type \code{T}.  In order to
vectorise code involving \code{T} we need its vectorised version \code{\V T}.
We can generate \code{\V T} from \code{T} by 
by vectorising its component types in the obvious way.  Thus, for example,
%
\begin{quote}
\begin{alltt}
data T  = C t1 t2 | D
\end{alltt}
\end{quote}
%
generates the new data type declaration:
%
\begin{quote}
\begin{alltt}
data \V{T} = \V{C} \TT{t1} \TT{t2} | \V{D}
\end{alltt}
\end{quote}
%
If any of the argument types cannot be vectorised, then neither can \code{T}.
In the special (but very common) case where \code{\TT{t1}} = \code{t1} and
\code{\TT{t2}} = \code{t2}, we can avoid creating a fresh data type, instead
simply setting \code{\V{T}} = \code{T}, just as we do for \code{Int}.  So,
returning to Figure~\ref{fig:bh}, we have \code{\V{MassPnt} $=$ MassPnt} and
\code{\V{Particle} $=$ Particle}.  In contrast, for \code{Tree} we get
%
\begin{quote}
\begin{alltt}
data \V{Tree} = \V{Node} MassPnt \paparen{\V{Tree}}
\end{alltt}
\end{quote}
%

\paragraph{Functions.}
The vectorised version of function arrow \code{(->)} is the type of
vectorised functions \code{(:->)}, but how is \code{(:->)} defined?
Consider the following (contrived) example:
%
\begin{quote}
\begin{alltt}
app :: (Int -> Int) -> (Int, [:Int:])
app f = (f 1, [:f x | x <- [:1, 2, 3:]:])
\end{alltt}
\end{quote}
%
Here we apply \code{f} outside and inside an array comprehension; 
in the former case we must run \code{f} sequentially, but in the latter
it should be evaluated in parallel.  To support parallel application of \code{f},
vectorisation generates a data-parallel, or \emph{lifted} version of \code{f},
denoted by \code{\lift{f}}, such that if \code{f :: t -> u}, then
\code{\lift{f} :: PA \TT{t} -> PA \TT{u}} (for full details of lifting,
see~\cite{leshchinskiy:diss}). In
the fully-vectorised version of \code{app}, we therefore need \code{f}'s
regular as well as its lifted variant, so we must pass \emph{both} versions of
\code{f} to \code{\V{app}}.  To a first approximation, therefore, the type
\code{(:->)} is defined thus:
\begin{quote}
\begin{alltt}
data a :-> b = MkFun (a -> b) (\pa{a} -> \pa{b})
\end{alltt}
\end{quote}
That is, vectorisation replaces a function of type \code{t -> u} by
a \emph{pair} of functions, of type \code{(\TT{t} -> \TT{u}, \pa{\TT{t}} ->
\pa{\TT{u}})}.
This definition is not quite right, because of nested functions and partial applications
\cite{leshchinskiy-etal:ho-flattening}, but 
the details are not important for this paper.  All that we need is the existence of
the vectorised function constructor \code{(:->)}, and its apply operator
\begin{quote}
\begin{alltt}
($:) :: (a :-> b) -> a -> b
\end{alltt}
\end{quote}

\paragraph{Vectorised arrays.}

Under selective vectorisation, the non-vectorised (and hence sequential) part
of the program may still manipulate ``parallel'' arrays.  For example, we
might read a file to create a parallel array of type \code{[:Int:]}, that is
then passed to a vectorised computation.  Conversely, in the function
\code{oneStepIO} in Figure~\ref{fig:bh-oneStep}, we consume a parallel array
produced by a vectorised computation in sequential I/O code.

While the type of parallel arrays \code{[:a:]} in the source language
is parametric, the representation of arrays and array operations after
vectorisation depends on the element type.  For example, an array of
pairs is represented as a pair of arrays.  The reasons for this
requirement, and a sketch of how we realise this in our implementation
using \emph{type families}, are provided in previous
work~\cite{keller-chak:tflat,chak-etal:DPH}.

Concretely, \code{PA} is a type-indexed data type family representing vectorised
arrays.  In GHC's type-family notation \cite{ghc:type-families} we write
\begin{quote}
\begin{alltt}
data family \pa{(a::*)}
\end{alltt}
\end{quote}
Then we give a \code{data instance} declaration for each type that we want to
store in a vectorised array. For example:
\begin{quote}
\begin{alltt}
data instance \pa{(a,b)} = PAPair \paparen{a} \paparen{b}
\end{alltt}
\end{quote}
Hence, for each user-defined algebraic data type, we must generate a \code{data instance}
declaration that describes how a vectorised array of such values is
represented.  For example, the \code{Tree} type in Figure~\ref{fig:bh}
generates the following declaration:
%
\begin{quote}
\begin{alltt}
data instance \pa{Tree} = \Arr{Node} \paparen{MassPnt} (Segd, \pa{Tree})
\end{alltt}
\end{quote}
%
\code{Segd} is a \emph{segment descriptor} encoding the structure of nested
arrays; c.f., for example~\cite{chak-etal:DPH} for more details of our use of
type-indexed data types.

\subsection{Vectorising expressions}
\label{sec:expressions}

Now we are ready to consider the selective vectorisation of expressions.
Our approach relies on three mutually recursive transformation schemes defined
in Figure~\ref{fig:trafo}:
%
\begin{quote}
\begin{alltt}
\VT{\(\cdot\)}  \,:: Expr \var{t} -> Env -> Maybe (Expr \TT{\var{t}})
\ST{\(\cdot\)}  \,:: Expr \var{t} -> Env -> Expr \var{t}
\SV{\(\cdot\)} :: Expr \var{t} -> Env -> (Maybe (Expr \TT{\var{t}}), Expr \var{t})
\end{alltt}
\end{quote}
%
Full vectorisation \VT{\(\cdot\)}, and selective vectorisation \ST{\(\cdot\)}, 
have already been introduced, although here we give them types that
(a) express partiality by returning a \code{Maybe}, and (b) 
express the type transformation by parameterising \code{Expr}.

% Crucially, \ST{\(\cdot\)} never changes the type of the transformed expression, so that 
% the result of selective vectorisation can be transparently used in
% place of the original expression without having to modify the surrounding
% code. In contrast, \VT{\(\cdot\)} will in general change the type of the
% expression such that it can only be used by vectorised code.  We have made
% this explicit in the signatures by parametrising \code{Expr} with the type of
% the represented expression.

The definitions of \VT{\(\cdot\)} and \ST{\(\cdot\)} do not directly depend on
each other. Instead, the recursive knot is tied by \SV{\(\cdot\)} which uses both
transformations to transform sub-expressions. \SV{\(\cdot\)} acts
as a mediator between selective and partial vectorisation. Its main task is to
intertwine vectorised and unvectorised code by introducing appropriate
conversions.

The transformations are parametrised with an environment which maps variables
to their vectorised versions if available. This information is required by
partial vectorisation to transform variables, as apparent in the
corresponding rule taken from Figure~\ref{fig:trafo}:
%
\begin{quote}
\begin{alltt}
\VT{\var{x}} env
  | (\var{x} \(\mapsto\) \V{\var{x}}) \(\in\) env = Just \meta{\V{\var{x}}}
  | otherwise       \,\,= Nothing
\end{alltt}
\end{quote}
%
In the following, we look at the transformations in more detail
and explain what happens at the interfaces between vectorised and unvectorised
code.

\begin{figure}[tp]
%\begin{quote}
\begin{alltt}
\ST{\(\cdot\)} :: Expr \var{t} -> Env -> Expr \var{t}
\ST{\var{x}} env    \;= \meta{\var{x}}
\ST{\var{e\sub1} \var{e\sub2}} env = \meta{\SE{\var{e\sub1}} \SE{\var{e\sub2}}}
  where
    (\_, \SE{\var{e\sub1}}) = \SV{\var{e\sub1}} env
    (\_, \SE{\var{e\sub2}}) = \SV{\var{e\sub2}} env

\ldots\inform{similar for other cases of \ST{\(\cdot\)}}\ldots

\ST{let \var{x} :: \var{t} = \var{e\sub1} in \var{e\sub2}} env
  = \meta{let \var{bs} in \SE{\var{e\sub2}}}
  where
    (\var{bs}, env') = \SVB{\var{x} :: \var{t} = \var{e\sub1}} env
    \SE{\var{e\sub2}} = \ST{\var{e\sub2}} env'

\VT{\(\cdot\)} :: Expr \var{t} -> Env -> Maybe (Expr \TT{\var{t}})
\VT{\var{x}} env
  | (\var{x} \(\mapsto\) \V{\var{x}}) \(\in\) env = Just \meta{\V{\var{x}}}
  | otherwise       \,\,= Nothing
\VT{\var{e\sub1} \var{e\sub2}} env 
  | (Just \V{\var{e\sub1}}, \_) <- \SV{\var{e\sub1}} env
  , (Just \V{\var{e\sub2}}, \_) <- \SV{\var{e\sub2}} env = Just \meta{\V{\var{e\sub1}} $: \V{\var{e\sub2}}}
  | otherwise                  \,\,= Nothing
\VT{let \var{x} :: \var{t} = \var{e\sub1} in \var{e\sub2}} env
  | (Just \V{\var{e\sub2}}, \_) <- \SV{\var{e\sub2}} env' = Just \meta{let \var{bs} in \var{e\sub2}}
  | otherwise                   \,\,= Nothing
  where
    (\var{bs}, env') = \SVB{\var{x} :: \var{t} = \var{e\sub1}} env

\ldots\inform{similar for other cases of \VT{\(\cdot\)}}\ldots

\SV{\(\cdot\)} :: Expr \var{t} -> Env -> (Maybe (Expr \TT{\var{t}}), Expr \var{t})
\SV{\var{e}} env = case \VT{\var{e}} env of
              Just \V{\var{e}}
                | \inform{\code{fromV \V{\var{e}}} exists} -> (Just \V{\var{e}}, \meta{fromV \V{\var{e}}})
                | otherwise         -> (Just \V{\var{e}}, \SE{\var{e}})
              Nothing
                | \inform{\code{toV \SE{\var{e}}} exists}   -> (Just \meta{toV \SE{\var{e}}}, \SE{\var{e}})
                | otherwise         -> (Nothing, \SE{\var{e}})
  where
    \SE{\var{e}} = \ST{\var{e}} env

\SVB{\(\cdot\)} :: Binding -> Env -> ([Binding], Env)
\SVB{\var{x} :: \var{t} = \var{e}} env
  | \inform{\var{t} is vectorisable}
  , (Just \V{\var{e}}, \SE{\var{e}}) <- \SV{\var{e}} env' = ([\var{x}::\var{t} = \SE{\var{e}}, \V{\var{x}}::\V{\var{t}} = \V{\var{e}}], env')
  | otherwise                   \,\,= ([\var{x}::\var{t} = \ST{\var{e}} env], env)
  where
    env'  = env \(\cup\) \{\var{x} \(\mapsto\) \V{\var{x}}\}
\end{alltt}
%
% \VT{\(\cdot\)} :: Expr \var{t} -> Env -> Maybe (Expr \V{\var{t}})
% \VT{\var{e\sub1} \var{e\sub2}} env = case (\SV{\var{e\sub1}} env, \SV{\var{e\sub2}} env) of
%                  ((Just \V{\var{e\sub1}}, \_), (Just \V{\var{e\sub2}}, \_)) -> Just (\V{\var{e\sub1}} \V{\var{e\sub2}})
%                  \_ -> Nothing
%\end{quote}
\caption{Selective vectorisation}
\label{fig:trafo}
\end{figure}

\subsection{Embedding unvectorised sub-expressions}

To see how the transformations defined in Figure~\ref{fig:trafo} allow for
mixing vectorised and unvectorised code, let us consider an example that
demonstrates how vectorised code may depend on unvectorised code.  Assume a
variable \code{M.constTable :: [:Int:]} defined in a module \code{M} that was
not compiled with vectorisation; i.e., \code{\V{M.constTable}} does not exist.
In a naive implementation, we might abandon the vectorisation of an expression
such as \code{sumP M.constTable} altogether and evaluate it
sequentially. However, this is clearly suboptimal; instead, we would like to
convert \code{M.constTable} to a vectorised representation (this is easily
possible for arrays of primitive types) and pass it to the vectorised, i.e.,
parallel implementation of \code{sumP}.  Ultimately, we would like to
have
%
\begin{quote}
\begin{alltt}
\VT{sumP M.constTable} env = Just \meta{\V{sumP} $: (toV M.constTable)}
\end{alltt}
\end{quote}
%
In other words, we would like vectorisation to succeed for the entire
expression even though it fails for one of the sub-expressions. That is
why \VT{\(\cdot\)} uses \SV{\(\cdot\)} to vectorise
sub-expressions as it is the latter that can introduce the necessary conversions.
For example, the rule for vectorising application given in
Figure~\ref{fig:trafo} passes the two sub-expressions on to \SV{\(\cdot\)}
which tries to transform them such that they can be used in a vectorised
context. In our example, vectorisation immediately succeeds for \code{sumP}
which has a vectorised version:
%
\begin{quote}
\begin{alltt}
\SV{sumP} env = (Just \meta{\V{sumP}}, \meta{\SE{sumP}})
\end{alltt}
\end{quote}
%
but fails for \code{M.constTable} which has no vectorised
variant. Fortunately, \SV{\(\cdot\)} is able to rectify this by introducing a
conversion:
%
\begin{quote}
\begin{alltt}
\SV{M.constTable} env 
  = (Just \meta{toV \SE{M.constTable}}), \meta{\SE{M.constTable}})
\end{alltt}
\end{quote}
%
This enables the application rule of \VT{\(\cdot\)} to succeed, producing the
desired result.  Note that the definition of \VT{\(\cdot\)} does not contain
any interfacing logic---interfacing is delegated entirely to
\SV{\(\cdot\)}. This is also the reason why we only included three example rules
in the definition of \VT{\(\cdot\)}---the complete definition can be obtained
by using \SV{\(\cdot\)} in place of direct recursion in the definition of
vectorisation given in~\cite{leshchinskiy:diss} and by accounting for
partiality in the exact same manner as we demonstrated for application.

\subsection{Vectorising as much as possible}

Using unvectorised in vectorised code is only half of the story, however.
Arguably much more important is the ability to pass results of parallel
computations to inherently unvectorisable tasks such as I/O. In fact, we have
already seen an example where this is absolutely essential: the statement
\code{print qs} in Figure~\ref{fig:bh-oneStep} outputs the result of a
computation which we expect to be executed in parallel and which, therefore,
must be vectorised. Again, it is the task of \SV{\(\cdot\)} to introduce the
necessary conversion before passing the computed value to the unvectorisable
\code{print}.

The mechanism employed here is quite similar to the one discussed in the
previous section.
%The rule for selectively vectorising applications is
%
%\begin{quote}
%\begin{alltt}
%\ST{\(\cdot\)} :: Expr \var{t} -> Env -> Expr \var{t}
%\ST{\var{e\sub1} \var{e\sub2}} env = \meta{\SE{\var{e\sub1}} \SE{\var{e\sub2}}}
%  where
%    (\_, \SE{\var{e\sub1}}) = \SV{\var{e\sub1}} env
%    (\_, \SE{\var{e\sub2}}) = \SV{\var{e\sub2}} env
%\end{alltt}
%\end{quote}
%
Since we cannot vectorise \code{print}, we have:
%
\begin{quote}
\begin{alltt}
\SV{print} env = (Nothing, \meta{\SE{print}})
\end{alltt}
\end{quote}
%
The situation is quite different for \code{qs}, however. Not only can it be
fully vectorised to \code{\V{qs}}, the latter can also be converted to an
unvectorised representation. In such a case, \SV{\(\cdot\)} will throw away the
result of selectively vectorising the sub-expression and simply suitably
convert the fully vectorised version. In our example, this amounts to:
%
\begin{quote}
\begin{alltt}
\SV{qs} env = (Just \meta{\V{qs}}, \meta{fromV \V{qs}})
\end{alltt}
\end{quote}
%
For the overall expression, the transformation rule for selectively
vectorising applications then generates
%
\begin{quote}
\begin{alltt}
\ST{print qs} env = \meta{\SE{print} (fromV \V{qs})}
\end{alltt}
\end{quote}
%
This is optimal in the sense that we evaluate as much as possible in parallel
(namely all of \code{qs}) before passing the result to the inherently
sequential code. The definitions of \ST{\(\cdot\)} and \SV{\(\cdot\)} ensure
that the transformation always prefers fully vectorised expression
to using selectively vectorised ones, thereby preserving the maximum
degree of parallelism while still allowing for partiality of vectorisation.

\subsection{Vectorising \code{let}}

During selective vectorisation, \code{let} bindings are handled in just the
same way as that described in Sections~\ref{sec:full-vect} and
\ref{sec:sel-vect}.  Given a single\footnote{%
  Both in the definition of the transformation and in the subsequent
  discussion, we restrict ourselves to a single, possibly recursive binding of
  the form \code{let \var{x} :: \var{t} = \var{e\sub1} in \var{e\sub2}}.  Our
  method easily generalises to multiple mutually-recursive bindings.}  binding
\code{\var{x}::\var{t} = \var{e}}, we always produce the selectively
vectorised binding \code{\var{x}::\var{t} = \ST{\var{e}}}.  Additionally, if
\code{\var{e}} can be fully vectorised, we generate the fully vectorised
binding \code{\V{\var{x}}::\TT{\var{t}} = \VT{\var{e}}}. In this case, we also
extend the environment to account for the newly introduced vectorised version
of \code{\var x} such that it is visible during the vectorisation of the
body. This is described by the \code{let} cases of \code{\VT{\(\cdot\)}} and
\code{\ST{\(\cdot\)}}, which invoke the transformation scheme \SVB{\(\cdot\)}
to deal with the binding.
%
%\begin{quote}
%\begin{alltt}
%\VT{let \var{x} :: \var{t} = \var{e\sub1} in \var{e\sub2}} env
%  | (Just \V{\var{e\sub2}}, \_) <- \SV{\var{e\sub2}} env' = Just \meta{let \var{bs} in \var{e\sub2}}
%  | otherwise                   \,\,= Nothing
%  where
%    (\var{bs}, env') = \SVB{\var{x} :: \var{t} = \var{e\sub1}} env
%\end{alltt}
%\end{quote}
%
%The \code{let} case of \code{\ST{\(\cdot\)}} is analogous. Moreover, 
The same transformation is used to handle top-level bindings.

As an example, the body of
\code{moveParticle} from Figure~\ref{fig:bh} is vectorised as follows:
%
\begin{quote}
\begin{alltt}
\VT{let v = velocity p in Particle (movePnt (center p) v) v} env
  = Just \(\llbracket\)let \V{v} = \V{velocity} $: \V{p}
              v  = fromV (\V{velocity} $: \V{p})
          in \V{Particle} $: 
               (\V{movePnt} $: (\V{center} $: \V{p}) $: \V{v}) $: \V{v}\(\rrbracket\)
\end{alltt}
\end{quote}
%
% \begin{quote}
% \begin{alltt}
% \V{let d = distance x y in d > epsilon && len / d < theta}
%   = let \V{d} = \V{distance} \V{x} \V{y}
%         d  = fromV (\V{distance} \V{x} \V{y})
%     in
%     \V{d} \V{>} \V{epsilon} \V{&&} \V{len} \V{/} \V{d} \V{<} \V{theta}
% \end{alltt}
% \end{quote}
%
%\begin{quote}
%\begin{alltt}
%\VT{let x :: Int = sumP xs in x+x} = let \V{x} :: Int = \V{sumP} \V{xs}
%                                         x :: Int = fromV (\V{sumP} \V{xs})
%                                     in \V{x} \V{+} \V{x}
%\end{alltt}
%\end{quote}
%
Obviously, there is ample room for optimisation here.
For example, when \code{\SVB{\(\cdot\)}} generates two
bindings in a local \code{let}, only one of them may be used in the \code{let} body,
but simple dead-code elimination will excise the unused binding.
% 
% It may seem overly complicated to generate
% both the binding for \code{v} and \V{v} here.  However, consider that
% \SVB{\(\cdot\)} is also used for top-level bindings, which may be exported and
% where we cannot statically determine which of the bindings is subsequently
% used.

What about recursion?\footnote{NB: Haskell does not distinguish between value
  and function bindings.  Any \code{let} binding can be recusive.}  Whether
the right-hand side of a recursive binding such as
%
\code{r :: \var{t} = f r}
%
can be vectorised depends, among other things, on whether a fully vectorised
version of \code{r} is available. Of course, we cannot know if \code{\V{r}} is
available until we have tried to vectorise the right-hand side.  Obviously,
this is a classical case of circular dependency which our transformation must
resolve.

Our solution to this problem is somewhat simple-minded, but effective. First,
we attempt to vectorise the right-hand side assuming that \code{\V{r}} exists.
If it can be fully vectorised, we generate two bindings as described above
using the two expressions produced by \SV{\(\cdot\)}. If partial vectorisation
fails, however, we are faced with an additional complication. We cannot use
the selectively vectorised expression that was produced by \SV{\(\cdot\)}
under the assumption that \code{\V{x}} exists; after all, it may contain
references to the latter. The following example demonstrates this. Suppose we
have the following functions:
%
\begin{quote}
\begin{alltt}
f  :: Int -> T
g  :: T -> Int
\V{g} :: \V{T} :-> Int
\end{alltt}
\end{quote}
%
Here, \code{g} has a vectorised version but \code{f} does not. Moreover, we
assume that the type \code{T} is vectorisable but does not support conversion
to and from \code{\V{T}}. Then, for the binding \code{x :: T = f (g x)}
partial vectorisation would fail but selective
vectorisation, if performed under the assumption that \code{\V{x}} exists,
would yield \code{x :: T = f (toV (\V{g} \$: \V{x}))}. This definition is
unusable, however, as we have no binding for \code{\V{x}} after all. We have
to selectively vectorise the binding once more, this time omitting
\code{\V{x}} from the environment. In our example, this would leave the
original binding unchanged which is, indeed, the only possible solution.



\section{Selective vectorisation of modules}
\label{sec:modules}

Between all the modules forming a program, some modules will be compiled with
vectorisation and some will not.  In the following, we discuss how these two
types of modules fit together and what extra information vectorisation
requires to be communicated between separately compiled modules.

\subsection{Modules compiled without vectorisation}

The scheme for vectorising expressions, and in particular bindings, presented
before is designed such that modules compiled without vectorisation
%
\begin{enumerate}
\item do not have to be aware of vectorisation at all and
\item are just a special case of those compiled with vectorisation.
\end{enumerate}
%
Concerning Point~(1), vectorised modules still contain all the original type
definitions of the source and, although bindings of the form \code{\var
  v::\var t = \var e} are transformed into \code{\var v::\var t = \SE{\var e}},
their interface remains the same.  Concerning Point~(2), even if a module is
compiled with vectorisation, it is conceivable that none of its functions or
type declarations is actually vectorisable under partial vectorisation.  In
this case, the interface of the module remains as if it hadn't been compiled
with vectorisation at all.  (Nevertheless, some expression bodies may have
been selectively vectorised.)

\subsection{Interface files}

GHC uses \emph{interface files} to communicate exported type declarations and
function signatures between separately compiled modules.  Whenever a module
\code{A} is compiled, an interface file \code{A.hi} is generated from its type
information.  Whenever a module \code{B} imports \code{A}, the compiler reads
\code{A.hi} to obtain type information for all imported entities.  

If optimisation is enabled (and vectorisation is a form of optimisation), GHC
emits further information into interface files.  This additional information
includes information computed by code analysis (such as strictness
information) as well as the right-hand sides of function definitions that are
considered for cross-module inlining.

When a module is compiled with vectorisation, GHC includes the following
additional information in the interface file:
%
\begin{itemize}
\item For each value or function binding \code{x}, GHC indicates whether
  \code{\V x} exists.
\item For each type constructor \code{T}, GHC indicates whether \code{\V T}
  exists, and if so, whether \code{T} itself serves as \code{\V T}.  If
  \code{\V T} exists, we may also have the type-specific
  conversion functions \code{toV} and \code{fromV}.
\item For each type constructor \code{T}, we have a type family instance
  defining the representation of the non-parametric array representation
  described in Section~\ref{sec:vec-arr-ty}.  This always exists as we use
  parametric, boxed arrays as a fallback for types where we cannot derive an
  optimised representation.
\end{itemize}


\section{Related work}
\label{sec:related}

There is a long list of work concerning vectorisation, some of which we have
mentioned throughout this paper.  We have discussed much of this previous work
in~\cite{chak-etal:DPH} and will refrain from repeating this discussion.  To the
best of our knowledge, none of this previous work has mentioned partial
vectorisation.  In particular,
NESL~\cite{blelloch:diss,blelloch-etal:impl-nested-parallel} was implemented
as a whole program compiler performing wholesale vectorisation.

The Proteus system~\cite{mills-etal:proteus} promised a combination of data
and control parallelism, but Proteus had a particular focus on manual
refinement of algorithms and where data parallel components were automatically
vectorised, this again was a complete whole-program transformation.  Moreover,
the system was never fully implemented.

Manticore~\cite{fluet-etal:manticore-status} supports a range of forms of
parallelism including nested data parallelism.  Manticore employs some of the
same techniques as we do, but it does not seem to use vectorisation in the same
form.  The Manticore implementation is, at the time of writing, work in
progress.


\section{Conclusion}
\label{sec:conclusion}

We argued that vectorisation for a fully fledged functional language needs to
be partial; i.e., only part of a program is vectorised.  We presented and
in part formalised a partial vectorisation transformation that vectorises
sub-expressions selectively and uses conversions where necessary to integrate
vectorised and unvectorised code.  At the time of writing, we are working on
completing a first version of vectorisation for GHC, which includes our
partial vectorisation strategy.  All code is publicly accessible from the GHC
HEAD repository at \url{http://darcs.haskell.org/ghc/}.

\bibliographystyle{splncs}
\bibliography{slpj-author,simon,vect-for-real}

\end{document}

% Local 

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% IspellDict: british
%%% End: 
