Commit f35b69cf authored by rl@cse.unsw.edu.au's avatar rl@cse.unsw.edu.au
Browse files

Add ndp docs

parent f071ec88
%%% 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}\\
}%
}
\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}