--- /dev/null
+%%% This is a LaTeX2e style file.
+%%%
+%%% It supports setting functional languages, such as Haskell.
+%%%
+%%% Manuel M. T. Chakravarty <chak@cse.unsw.edu.au> [1998..2002]
+%%%
+%%% $Id: haskell.sty,v 1.2 2004/04/02 08:47:53 simonmar Exp $
+%%%
+%%% This file is free software; you can redistribute it and/or modify
+%%% it under the terms of the GNU General Public License as published by
+%%% the Free Software Foundation; either version 2 of the License, or
+%%% (at your option) any later version.
+%%%
+%%% This file is distributed in the hope that it will be useful,
+%%% but WITHOUT ANY WARRANTY; without even the implied warranty of
+%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+%%% GNU General Public License for more details.
+%%%
+%%% Acknowledegments ==========================================================
+%%%
+%%% Thanks to Gabriele Keller <keller@it.uts.edu.au> for beta testing and
+%%% code contributions. Thanks to the LaTeX3 project for improving the LaTeX
+%%% sources (which helped me writing this code). Furthermore, I am grateful
+%%% to Martin Erwig <Martin.Erwig@FernUni-Hagen.de> and Bernard J. Pope
+%%% <bjpop@cs.mu.OZ.AU> for feedback and suggestions, and to Conal Elliott
+%%% <conal@MICROSOFT.com> and Marc van Dongen <dongen@cs.ucc.ie> for pointing
+%%% out a tricky bug.
+%%%
+%%% TODO ======================================================================
+%%%
+%%% B ~ bug; F ~ feature
+%%%
+%%% * B: Consider to use the following alternative definition for \<..\>:
+%%%
+%%% \def\<{\bgroup\@hsSpaceToApp\endhs}
+%%% \def\endhs#1\>{\(\mathit{#1}\)\egroup}
+%%%
+%%% It completely avoids the problem that \mathit\bgroup..\egroup isn't
+%%% guaranteed to work and seems more elegant, anyway.
+%%%
+%%% * F: Along the lines of the discussion with Martin Erwig add support for
+%%% keywords etc (see the emails)
+%%%
+%%% * B: If we have as input
+%%%
+%%% \<map
+%%% g\>
+%%%
+%%% there won't be a `\hsap' inserted!! (Can this be solved by using
+%%% \obeylines in \<...\>?)
+%%%
+%%% * B: A \relax is needed after a & if it immediately followed by a \hsbody{}
+%%% (See TeXbook, S.240)
+%%%
+%%% * F: Implement a \hstext{...} as \(\text{...}\).
+%%%
+%%% * F: Star-form of \hscom that uses "---" instead of "-\hskip0pt-"
+%%%
+%%% * We would like hswhere* etc that are like haskell* (\hsalign already
+%%% supports this, ie, there is a \hsalign*).
+%%%
+%%% * Star-Versions of if, let etc that use a single line layout (maybe not
+%%% with star, because of the above).
+%%%
+%%% * Support for enforcing and prohibiting breaks in `haskell' displays.
+%%%
+%%% * Comments in a let-in should be aligned in the same way for the bindings
+%%% and the body.
+%%%
+%%% * It would be nice to have different styles (indentation after in of
+%%% let-in or not) etc; either to be set with a package option or in the
+%%% preamble (the latter probably makes more sense).
+%%%
+%%% * Literate programming facility: Variant of the `haskell' env (maybe
+%%% `hschunk', which is named and can be used in other chunks). But maybe
+%%% it is not necessary to provide a chunk-based reordering mechanism,
+%%% because most of the Haskell stuff can be in any order anyway...
+%%% Important is to provide a way to define visually pleasing layout
+%%% together with the raw Haskell form for program output. (Maybe `haskell*'
+%%% as Haskell env that outputs its contents?)
+%%%
+
+%% Initialization
+%% ==============
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{haskell}[2002/02/08 v1.1a Chilli's Haskell Style]
+
+% NOTE: The sole purpose of the following is to work around what I believe is
+% a bug in LaTeX. If the first occurence of \mathit in a document uses
+% \bgroup and \egroup to enclose the argument (instead of { and }),
+% \mathit does *not* apply to the argument. (I guess, some font
+% initialisation stuff is getting in the way of parsing the argument.)
+%
+% The following forces a \mathit right after \begin{document}.
+%
+% UPDATE: The LaTeX project people say that it isn't really a bug; more
+% like a not supported form. See alternative definition in the
+% bug list above.
+%
+\AtBeginDocument{\setbox0=\hbox{\(\mathit\relax\)}}
+
+
+%% Parameters
+%% ==========
+
+\newskip\hsmargin
+\hsmargin\leftmargini
+
+
+%% Main macros and environments
+%% ============================
+
+% applications
+%
+\newcommand{\hsap}{% % application by juxtaposition
+ \unskip\mskip 4mu plus 1mu} % only the last \hsap counts
+
+% commands to start and stop setting spaces as \hsap
+%
+{\obeyspaces\gdef\@hsSpaceToApp{\obeyspaces\let =\hsap}} % spaces matter!!!
+{\obeyspaces\gdef\@hsNormalSpace{\let =\space}}
+
+% commands to start and stop treating numbers specially, ie, we don't want
+% them to be affected by font changing commands in Haskell contexts as this
+% would give italic numerals; the trick is to redefine their math code such
+% that they go into math class 0 and thus don't change families (cf. `The
+% TeXbook', Chapter 17, pp152)
+%
+\newcommand{\@hsRmNumbers}{%
+ \mathcode`0="0030
+ \mathcode`1="0031
+ \mathcode`2="0032
+ \mathcode`3="0033
+ \mathcode`4="0034
+ \mathcode`5="0035
+ \mathcode`6="0036
+ \mathcode`7="0037
+ \mathcode`8="0038
+ \mathcode`9="0039
+ }
+\newcommand{\@hsNormalNumbers}{%
+ \mathcode`0="7030
+ \mathcode`1="7031
+ \mathcode`2="7032
+ \mathcode`3="7033
+ \mathcode`4="7034
+ \mathcode`5="7035
+ \mathcode`6="7036
+ \mathcode`7="7037
+ \mathcode`8="7038
+ \mathcode`9="7039
+ }
+
+% Save the bindings of the standard math commands
+%
+% This is somewhat subtle as we want to able to enter the original math mode
+% within Haskell mode and we have to ensure that the different opening
+% commands are matched by the correct versions of the closing commands.
+%
+\let\@hsmathorg=\(
+\let\@hsmathendorg=\)
+\let\hs@crorg=\\
+\newcommand{\@hsmath}{%
+ \relax\hbox\bgroup
+ \@hsNormalSpace
+ \@hsNormalNumbers
+ \let\(=\@hsmathorgx
+ \let\)=\@hsmathend
+ \def\\{\hs@crorg}%
+ \@hsmathorg
+ }
+\newcommand{\@hsmathend}{%
+ \@hsmathendorg
+ \egroup
+ }
+\newcommand{\@hsmathorgx}{%
+ \relax\@hsmathorg
+ \let\)=\@hsmathendorg
+ }
+
+%% Typesetting of Haskell
+%% ======================
+
+% Inline Haskell phrases are delimited by `\<' and `\>'.
+%
+% Note: `\>' is only locally redefined.
+%
+\newcommand{\<}{%
+ \@hsmathorg
+ \mathit\bgroup
+ \@hsSpaceToApp
+ \@hsRmNumbers
+ \let\>=\@endhs
+ \let\(=\@hsmath
+ \def\\{\cr} % for Haskell alignments
+ }
+\newcommand{\@endhs}{%
+ \egroup
+ \@hsmathendorg
+ }
+
+% Displayed Haskell (environment `haskell' and `haskell*')
+%
+% There are two kind of preambles for \halign: \hs@preambleNorm is for
+% `amsmath' style alignments and \hs@preambleStar for `equation' style
+% alignments (but with an unbound number of columns to its right)
+%
+% We need #### to get a ## in the \edef building the \halign command.
+%
+% first the preambles (also used in \hs@align below):
+%
+\def\hs@preambleNorm{%
+ \noexpand\<####\unskip\noexpand\>\hfil&&\noexpand%
+ \<{}####\unskip\noexpand\>\hfil}
+\def\hs@preambleStar{%
+ \noexpand\<####\unskip\noexpand\>\hfil&\hfil\noexpand%
+ \<{}####\unskip{}\noexpand\>\hfil&&\noexpand\<{}####\noexpand\>\hfil}
+%
+% the environments:
+%
+\newenvironment{haskell}{%
+ \@haskell\hs@preambleNorm}{%
+ \@endhaskell
+ }
+\newenvironment{haskell*}{%
+ \@haskell\hs@preambleStar}{%
+ \@endhaskell
+ }
+%
+% auxiliary definition getting the preamble as its first argument and starting
+% the environment:
+%
+\def\@haskell#1{%
+ \bgroup
+ \vspace\abovedisplayskip
+ \let\(=\@hsmath % Important when `\(' occurs after `&'!
+ \edef\@preamble{%
+ \halign\bgroup\hskip\hsmargin#1\cr}
+ \@preamble
+ }
+%
+% Auxiliary definition ending environment:
+%
+\def\@endhaskell{%
+ \crcr\egroup
+% \vspace\belowdisplayskip
+ \egroup\noindent\ignorespaces\global\@ignoretrue%
+ }
+
+% single line comment and keyword style
+%
+\newcommand{\hscom}[1]{%
+ \relax\(\quad\textnormal{-\hskip0pt- #1}\)}
+% \relax\(\quad\textnormal{--- #1}\)}
+\newcommand{\hskwd}[1]{%
+ \mathbf{#1}}
+
+% informal description
+%
+\newcommand{\hsinf}[1]{%
+ \(\langle\textnormal{#1}\rangle\)}
+
+% literals and some special symbols
+%
+\newcommand{\hschar}[1]{\textrm{'#1'}} % character literals
+\newcommand{\hsstr}[1]{\textrm{``#1''}} % strings literals
+\newcommand{\hsfrom}{\leftarrow} % <-
+
+% aligned subphrases
+%
+% check for an optional star and combine prefix (in #1) with one of the two
+% preambles (with star means to center the material between the first and
+% second &)
+%
+\def\hs@align#1{%
+ \@ifstar
+ {\hs@align@pre{#1\hs@preambleStar}}%
+ {\hs@align@pre{#1\hs@preambleNorm}}%
+ }
+%
+% test for optional argument; #1: preamble
+%
+\def\hs@align@pre#1{%
+ \@testopt{\hs@align@prealign#1}t}
+%
+% got all arguments, now for the real code; #1: preamble; #2: alignment;
+% #3: body (the material set by the \halign)
+%
+\def\hs@align@prealign#1[#2]#3{%
+ \relax\(
+ \edef\@preamble{%
+ \halign\bgroup#1\cr}
+ \if #2t\vtop \else \if#2b\vbox \else \vcenter \fi\fi
+ \bgroup%
+ \@preamble
+ #3%
+ \crcr\egroup%
+ \egroup\)
+ }
+%
+% user-level command: alignment without a prefix
+%
+\newcommand{\hsalign}{%
+ \relax
+ \hs@align\relax%
+ }
+
+% subphrase breaking the surrounding alignment being flushed left
+%
+\newcommand{\hsnoalign}[1]{%
+ \noalign{%
+ \hs@align{\hskip\hsmargin}{#1}%
+ }%
+ }
+
+% body expression breaking the surrounding alignment
+%
+% * setting \hsmargin to 0pt within the preamble (and _after_ it is used in
+% the preamble) is crucial, as we want \hsmargin only to be applied in
+% _outermost_ alignments
+%
+\newcommand{\hsbody}[1]{%
+ {}\\
+ \noalign{%
+ \hs@align{\hskip\hsmargin\quad\hsmargin0pt}{#1}%
+ }%
+ }
+
+
+%% Defining commands for use in the Haskell mode
+%% =============================================
+%%
+%% We use some of the low-level machinery defined in LaTeX's source file
+%% `ltdefns.dtx'.
+%%
+%% \hscommand is similar to \newcommand, but there is no *-version.
+%%
+%% We use our own definitions here to insert a strategic `\relax' (see below)
+%% and to obey spaces within the bodies of Haskell definitions.
+
+\newcommand{\hscommand}[1]{\@testopt{\hs@newcommand#1}0}
+\def\hs@newcommand#1[#2]{%
+ \obeyspaces % spaces count in Haskell macros
+ \@ifnextchar [{\hs@xargdef#1[#2]}%
+ {\hs@argdef#1[#2]}}
+
+% All this trouble only to be able to add the `\relax' into the expansion
+% process. If we don't that, commands without optional arguments when
+% invoked after an alignment character & don't work properly (actually, the
+% \obeyspaces doesn't work). I am sure that has to do with the scanning for
+% \omit etc in \halign (TeXbook, p240), but I don't understand yet why it
+% is problematic in this case.
+%
+% Furthermore, we switch off \obeyspaces in the end.
+%
+\long\def\hs@argdef#1[#2]#3{%
+ \@ifdefinable#1{%
+ \expandafter\def\expandafter#1\expandafter{%
+ \relax % in order to stop token expansion after &
+ \csname\string#1\expandafter\endcsname}%
+ \expandafter\@yargdef
+ \csname\string#1\endcsname
+ \@ne
+ {#2}%
+ {#3}}%
+ \catcode`\ =10% % stop obeying spaces now
+ }
+
+% Switch off \obeyspaces in the end.
+%
+\long\def\hs@xargdef#1[#2][#3]#4{%
+ \@ifdefinable#1{%
+ \expandafter\def\expandafter#1\expandafter{%
+ \expandafter
+ \@protected@testopt
+ \expandafter
+ #1%
+ \csname\string#1\expandafter\endcsname
+ {#3}}%
+ \expandafter\@yargdef
+ \csname\string#1\endcsname
+ \tw@
+ {#2}%
+ {#4}}%
+ \catcode`\ =10% % stop obeying spaces now
+ }
+
+
+%% Abbreviations
+%% =============
+
+% infix operators
+%
+\newcommand{\hsapp}{\mathbin{+\mkern-7mu+}}
+\newcommand{\hsifix}[1]{\mathbin{\string`#1\string`}}
+
+% let expression
+%
+\hscommand{\hslet}[3][t]{%
+ \hsalign[#1]{%
+ \hskwd{let}\\
+ \quad\hsalign{#2}\\
+ \hskwd{in}\\
+ #3
+ }%
+ }
+
+% if expression
+%
+\hscommand{\hsif}[4][t]{%
+ \hsalign[#1]{%
+ \hskwd{if} #2 \hskwd{then}\\
+ \quad\hsalign{#3}\\
+ \hskwd{else}\\
+ \quad\hsalign{#4}%
+ }%
+ }
+
+% case expression
+%
+\hscommand{\hscase}[3][t]{%
+ \hsalign[#1]{%
+ \hskwd{case} #2 \hskwd{of}\\
+ \quad\hsalign{#3}%
+ }%
+ }
+
+% where clause
+%
+% * it is important to take the \quad into the preamble, so that nested
+% \noaligns can break it
+%
+\hscommand{\hswhere}[1]{%
+ \hsbody{%
+ \hskwd{where}\\
+ \hs@align{\quad}{#1}%
+ }%
+ }
+
+% do expression
+%
+\hscommand{\hsdo}[2][t]{%
+ \hsalign[#1]{%
+ \hskwd{do}\\
+ \quad\hsalign{#2}\\
+ }%
+}
+
+% class declaration
+%
+\hscommand{\hsclass}[2]{%
+ \hskwd{class} #1 \hskwd{where}
+ \hsbody{%
+ #2
+ }%
+}
+
+% instance declaration
+%
+\hscommand{\hsinstance}[2]{%
+ \hskwd{instance} #1 \hskwd{where}
+ \hsbody{%
+ #2
+ }%
+}
+
+
+%% Extensions for Distributed Haskell (Goffin)
+%% ===========================================
+%%
+%% These definitions may change in the future.
+
+\hscommand{\hsunif}{\mathbin{:=:}}
+\hscommand{\hsalias}{\mathrel{\sim}}
+\hscommand{\hsoutof}{\twoheadleftarrow}
+\hscommand{\hsinto}{\twoheadrightarrow}
+\hscommand{\hsparc}{\binampersand}
+\hscommand{\hsseq}{\Longrightarrow}
+\hscommand{\hsex}[2]{{\hskwd{ex} #1 \hskwd{in} #2}}
+
+\hscommand{\hsexin}[3][t]{%
+ \hsalign[#1]{%
+ \hskwd{ex} #2 \hskwd{in}\\
+ \quad\hsalign{#3}\\
+ }%
+ }
+
+\hscommand{\hschoice}[2][t]{%
+ \hsalign[#1]{%
+ \hskwd{choice}\\
+ \quad\hsalign{#2}\\
+ }%
+ }
+
+
--- /dev/null
+\documentclass{article}
+\usepackage{haskell}
+
+\hscommand{\vect}[1]{(#1)_v}
+\hscommand{\lift}[2]{(#1)^{\uparrow#2}}
+\hscommand{\liftn}[1]{(#1)^{\uparrow{n}}}
+
+\hscommand{\patype}[1]{\mathsf{patype}\langle#1\rangle}
+\hscommand{\pa}[1]{\mathsf{pa}\langle#1\rangle}
+
+\hscommand{\capp}{\mathbin{{\$}{:}}}
+\hscommand{\cappP}{\mathbin{{\$}{:}^\uparrow}}
+
+\hscommand{\parr}[1]{[{:}{:}#1{:}{:}]}
+\hscommand{\pparr}[1]{[{:}#1{:}]}
+
+\hscommand{\Data}{\hskwd{data}}
+\hscommand{\DataF}{\hskwd{data~family}}
+\hscommand{\DataI}{\hskwd{data~instance}}
+\hscommand{\NewtypeI}{\hskwd{newtype~instance}}
+
+\setlength{\parindent}{0cm}
+
+\begin{document}
+
+\section*{Library}
+
+\subsection*{Parallel arrays}
+
+We distinguish between user-visible, parametric arrays (\<\pparr{\cdot}\>) and
+flattened parallel arrays (\<\parr{\cdot}\>) which are internal to our
+implementation. Operations on the former have purely sequential semantics.
+During vectorisation, they are replaced by parallel arrays and operations.
+
+\begin{haskell}
+\Data \pparr{\alpha} = Array Int \alpha \hscom{or similar} \\
+\DataF \parr{\alpha}
+\end{haskell}
+
+\subsection*{\<PA\> dictionaries}
+
+To avoid problems with using typeclasses in Core, we use explicit records for
+representing dictionaries of type-dependent operations on parallel arrays:
+
+\begin{haskell}
+\Data PA \alpha = & PA \{
+ \hsbody{lengthP & :: \parr{\alpha}\to{Int} \\
+ replicateP & :: Int\to\alpha\to\parr{\alpha} \\
+ \ldots \\ \}}
+\end{haskell}
+
+In vectorised code, polymorphic functions must be supplied with a \<PA\>
+dictionary for each type varialbe. For instance, \<\Lambda\alpha.e\> turns
+into \<\Lambda\alpha.\lambda{dPA_\alpha}::PA \alpha.e'\>.
+
+For higher-kinded type variables, we expect a function of appropriate type
+which computes the dictionary for a saturated application of the type
+variable from the dictionaries of the arguments. For instance,
+\<\Lambda{m}::{*}\to{*}.e\> turns into
+\<\Lambda{m}::{*}\to{*}.\lambda{dPA_m}::(\forall\alpha::{*}.PA \alpha\to{PA}
+(m a)).e'\>.
+In general, the type of the \<dPA\> argument for a type \<\sigma::\kappa\> is
+given by
+
+\begin{haskell}
+\patype{\sigma:{*}} & = PA \sigma \\
+\patype{\sigma:\kappa_1\to\kappa_2} & =
+\forall\alpha:\kappa_1.\patype{\alpha:\kappa_1}\to\patype{\sigma \alpha:\kappa_2}
+\end{haskell}
+
+For each user-defined or built-in type constructor \<T\> we
+automatically define its dictionary \<dPA_T::\patype{T}\>. Moreover, for every
+in-scope type variable \<\alpha\> we have its dictionary
+\<dPA_\alpha::\patype{\alpha}\>. This allows us to compute the dictionary for
+an arbitrary type as follows:
+
+\begin{haskell}
+\pa{T} & = dPA_T \\
+\pa{\alpha} & = dPA_{\alpha} \\
+\pa{\sigma \phi} & = \pa{\sigma}[\phi] \pa{\phi} \\
+\pa{\forall\alpha::\kappa.\sigma} & =
+\Lambda\alpha::\kappa.\lambda{dPA_{\alpha}}::\patype{\alpha::\kappa}.\pa{\sigma}
+\end{haskell}
+
+\subsection*{Closures}
+
+Closures are represented as follows:
+
+\begin{haskell}
+\Data & Clo \alpha \beta & = \exists\gamma. Clo & (PA \gamma) \gamma
+ & (\gamma\to\alpha\to\beta) (\parr{\gamma}\to\parr{\alpha}\to\parr{\beta}) \\
+\DataI & \parr{Clo \alpha \beta} & = \exists\gamma. AClo & (PA \gamma)
+ \parr{\gamma}
+ & (\gamma\to\alpha\to\beta) (\parr{\gamma}\to\parr{\alpha}\to\parr{\beta})
+\end{haskell}
+
+Closure application is implemented by the following two operators:
+
+\begin{haskell}
+({\capp}) & :: Clo \alpha \beta \to \alpha \to \beta \\
+({\cappP}) & :: \parr{Clo \alpha \beta} \to \parr{\alpha} \to \parr{\beta}
+\end{haskell}
+
+Note that \<({\cappP})\> is effectively the lifted version of \<({\capp})\>.
+
+\subsection*{Flat array representation}
+
+Some important instances of the \<\parr{\cdot}\> family:
+
+\begin{haskell}
+\hskwd{data} & \hskwd{instance} \parr{(\alpha_1,\ldots,\alpha_n)}
+ & = ATup_n !Int \parr{\alpha_1} \ldots \parr{\alpha_n} \\
+\hskwd{newtype}~ & \hskwd{instance} \parr{\alpha\to\beta}
+ & = AFn (\parr{\alpha}\to\parr{\beta}) \\
+\hskwd{newtype} & \hskwd{instance} \parr{PA \alpha}
+ & = APA (PA \alpha)
+\end{haskell}
+
+The last two definitions are discussed later.
+
+\section*{Vectorisation}
+
+\subsection*{Types}
+
+We assume that for each type constructor \<T\>, there exists a vectorised
+version \<T_v\> (which can be the same as \<T\>). In particular, we have
+\begin{haskell}
+({\to}_v) & = Clo \\
+\pparr{\cdot}_v & = \parr{\cdot}
+\end{haskell}
+
+Vectorisation of types is defined as follows:
+
+\begin{haskell}
+\vect{T} & = T_v \\
+\vect{\alpha} & = \alpha \\
+\vect{\sigma \phi} & = \vect{\sigma} \vect{\phi} \\
+\vect{\forall\alpha:\kappa.\sigma} & = \forall\alpha:\kappa.\patype{\alpha:\kappa}\to\vect{\sigma}
+\end{haskell}
+
+\subsection*{Data type declarations}
+
+\begin{haskell}
+\vect{\hskwd{data} T = \overline{C t_1 \ldots t_n}} = \hskwd{data} T_v =
+\overline{C_v \vect{t_1} \ldots \vect{t_n}}
+\end{haskell}
+
+\subsection*{Terms}
+
+We distinguish between local variables (\<x\>) and global variables and
+literals \<c\>. We assume that we have the following typing judgement:
+
+\begin{haskell}
+\Delta,\Gamma\vdash{e}:\sigma
+\end{haskell}
+
+Here, \<\Delta\> assigns types to globals and \<\Gamma\> to locals. Moreover,
+we assume that for each global variable \<c\>, there exists a
+vectorised version \<c_v\>, i.e.,
+
+\begin{haskell}
+c:\sigma\in\Delta \Longrightarrow c_v:\vect{\sigma}\in\Delta
+\end{haskell}
+
+\subsubsection*{Vectorisation}
+
+\begin{haskell}
+\vect{c} & = c_v & c is global \\
+\vect{x} & = x & x is local \\
+\vect{\Lambda\alpha:\kappa.e} & =
+\Lambda\alpha:\kappa.\lambda{dPA_{\alpha}}:\patype{\alpha:\kappa}.\vect{e} \\
+\vect{e[\sigma]} & = \vect{e}[\vect{\sigma}] \\
+\vect{e_1 e_2} & = \vect{e_1}\capp\vect{e_2} \\
+\vect{\lambda{x}:\sigma.e} & = Clo \vect{\sigma} \vect{\phi} \tau \pa{\tau}
+ (y_1,\dots,y_n) \\
+ &
+\quad\quad(\lambda{ys}:\tau.
+ \lambda{x}:\vect{\sigma}.
+ \hskwd{case} ys \hskwd{of} (y_1,\dots,y_n) \to \vect{e}) \\
+ &
+\quad\quad(\lambda{ys}:\parr{\tau}.
+ \lambda{x}:\parr{\vect{\sigma}}.
+ \hskwd{case} ys \hskwd{of} ATup_n l y_1 \dots y_n \to \lift{e}{l})
+\\
+ \hswhere{e has type \phi \\
+ \{y_1:\tau_1,\dots,y_n:\tau_n\} & = FVS(e)\setminus{x} \\
+ \tau & = (\vect{\tau_1},\dots,\vect{\tau_n})}
+% \\
+% e has type \phi}
+\end{haskell}
+
+Vectorisation maintains the following invariant:
+
+\begin{haskell}
+\Delta,\Gamma\vdash{e}:\sigma \Longrightarrow
+ \Delta,\Gamma_v\vdash\vect{e}:\vect{\sigma}
+\end{haskell}
+
+where \<\Gamma_v\> is defined by
+
+\begin{haskell}
+x:\sigma\in\Gamma \Longleftrightarrow x:\vect{\sigma}\in\Gamma_v
+\end{haskell}
+
+\subsubsection*{Lifting}
+\begin{haskell}
+\liftn{c:\sigma} & = replicateP \pa{\vect{\sigma}} n c_v \\
+\liftn{x} & = x \\
+\liftn{\Lambda\alpha:\kappa.e} & =
+\Lambda\alpha:\kappa.\lambda{dPA_{\alpha}}:\patype{\alpha:\kappa}.\liftn{e} \\
+\liftn{e[\sigma]} & = \liftn{e}[\vect{\sigma}] \pa{\vect{\sigma}} \\
+\liftn{e_1 e_2} & = \liftn{e_1} \cappP \liftn{e_2} \\
+\liftn{\lambda{x}:\sigma.e} & = AClo \vect{\sigma} \vect{\phi} \vect{\tau}
+ \pa{\vect{\tau}}
+ (ATup_n y_1 \dots y_n) \\
+ &
+\quad\quad(\lambda{ys}:\vect{\tau}.
+ \lambda{x}:\vect{\sigma}.
+ \hskwd{case} ys \hskwd{of} (y_1,\dots,y_n) \to \vect{e}) \\
+ &
+\quad\quad(\lambda{ys}:\parr{\vect{\tau}}.
+ \lambda{x}:\parr{\vect{\sigma}}.
+ \hskwd{case} ys \hskwd{of} ATup_n l y_1 \dots y_n \to \lift{e}{l})
+ \hswhere{e has type \phi \\
+ \{y_1:\tau_1,\dots,y_n:\tau_n\} & = FVS(e)\setminus{x} \\
+ \tau & = (\tau_1,\dots,\tau_n)}
+\end{haskell}
+
+Lifting maintains the following invariant:
+
+\begin{haskell}
+\Delta,\Gamma\vdash{e}:\sigma \Longrightarrow
+ \Delta,\Gamma^\uparrow\vdash\liftn{e} : \parr{\sigma_v}
+\end{haskell}
+
+where
+
+\begin{haskell}
+x:\sigma\in\Gamma \Longleftrightarrow x:\parr{\vect{\sigma}}\in\Gamma^\uparrow
+\end{haskell}
+
+Note that this is precisely the reason for the \<\parr{\cdot}\> instances for
+\<\alpha\to\beta\> and \<PA \alpha\>. A term of type \<\forall\alpha.\sigma\>
+will be lifted to a term of type
+\<\parr{\forall\alpha.PA \alpha\to\vect{\sigma}}\> which requires the
+instances. Apart from closures, these are the only occurences of \<({\to})\> in
+the transformed program, however.
+
+
+\section*{What to vectorise?}
+
+An expression is vectorisable if it only mentions globals and type constructors
+which have a vectorised form. When vectorising, we look for maximal
+vectorisable subexpressions and transform those. For instance, assuming that
+\<print\> hasn't been vectorised, in
+
+\begin{haskell}
+main = \hsdo{
+ print (sumP \pparr{\ldots}) \\
+ print (mapP \ldots \pparr{\ldots})}
+\end{haskell}
+
+we would vectorise the arguments to \<print\>. Note that this implies that we
+never call non-vectorised code from vectorised code (is that a problem?).
+
+Whenever we come out of a vectorised ``bubble'', we have to convert between
+vectorised and unvectorised data types. The examples above would roughly
+translate to
+
+\begin{haskell}
+main = \hsdo{
+ print (unvect (sumP_v \parr{\ldots})) \\
+ print (unvect (mapP_v \ldots \parr{\ldots}))}
+\end{haskell}
+
+For this, we have to have the following functions:
+
+\begin{haskell}
+vect_\sigma & :: \sigma\to\vect{\sigma} \\
+unvect_\sigma & :: \vect{\sigma}\to\sigma
+\end{haskell}
+
+It is sufficient to have these functions only for a restricted set of types as
+we can always vectorise less if the conversions becomes too complex.
+
+Sometimes, it doesn't make sense to vectorise things. For instance, in
+
+\begin{haskell}
+foo f xs = print (f xs)
+\end{haskell}
+
+we wouldn't vectorise \<f xs\>. Unfortunately, this means that
+\<foo (mapP f) xs\> will be purely sequential.
+
+For each expression, the vectoriser gives one of the following answers.
+
+\begin{tabular}{lp{10cm}}
+\textbf{Yes} &
+the expression can be (and has been) vectorised \\
+\textbf{Maybe} &
+the expression can be vectorised but it doesn't make sense to do so
+unless it is used in a vectrorisable context (e.g., for \<f xs\> in \<foo\>)
+\\
+\textbf{No} &
+the expression can't be vectorised (although parts of it can, so we
+still get back a transformed expression)
+\end{tabular}
+
+\subsection*{Top-level definitions}
+
+For a top-level definition of the form
+
+\begin{haskell}
+f :: \sigma = e
+\end{haskell}
+
+vectorisation proceeds as follows.
+
+\begin{itemize}
+\item If \<e\> can be fully vectorised, we generate
+\begin{haskell}
+f_v :: \vect{\sigma} = \vect{e}
+\end{haskell}
+
+\item If it doesn't always make sense to vectorise \<e\>, i.e., the vectoriser
+returned \textbf{Maybe}, we leave the definition of \<f\> unchanged. Thus, we
+would not change
+\begin{haskell}
+({\$}) = \lambda{f}.\lambda{x}.f x
+\end{haskell}
+but would additionaly generate
+\begin{haskell}
+({\$}_v) = Clo \ldots
+\end{haskell}
+
+\item Otherwise (if the vectoriser said \textbf{Yes}) and we have
+\<unconv_\sigma\>, we change the definition of \<f\> to
+\begin{haskell}
+f :: \sigma = unconv_\sigma f_v
+\end{haskell}
+
+\item Otherwise (the vectoriser said \textbf{Yes} but we do not have
+\<unconv_\sigma\> or if \<e\> couldn't be fully vectorised), we change the
+definition of \<f\> to
+\begin{haskell}
+f :: \sigma = e'
+\end{haskell}
+where \<e'\> is obtaining by vectorising \<e\> as much as possible without
+changing its type. For instance, for
+\begin{haskell}
+f = \lambda{g}.\lambda{x}.mapP (\ldots) (g x)
+\end{haskell}
+we would generate
+\begin{haskell}
+f & = \lambda{g}.\lambda{x}.unvect (mapP_v (\ldots) (vect (g x))) \\
+f_v & = Clo \ldots
+\end{haskell}
+assuming we have the necessary conversions but cannot convert functions (i.e.,
+\<g\>).
+\end{itemize}
+
+\end{document}
+
projects / ghc-hetmet.git / commitdiff