From: Roman Leshchinskiy Date: Tue, 3 Jul 2007 06:37:38 +0000 (+0000) Subject: Add ndp docs X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=f35b69cf2ab808f9ec4e93d54b9f41ca4a51c8e0 Add ndp docs --- diff --git a/docs/ndp/haskell.sty b/docs/ndp/haskell.sty new file mode 100644 index 0000000..969ad67 --- /dev/null +++ b/docs/ndp/haskell.sty @@ -0,0 +1,496 @@ +%%% This is a LaTeX2e style file. +%%% +%%% It supports setting functional languages, such as Haskell. +%%% +%%% Manuel M. T. Chakravarty [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 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 and Bernard J. Pope +%%% for feedback and suggestions, and to Conal Elliott +%%% and Marc van Dongen 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 +%%% +%%% \ +%%% +%%% 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}\\ + }% + } + + diff --git a/docs/ndp/vect.tex b/docs/ndp/vect.tex new file mode 100644 index 0000000..06d8537 --- /dev/null +++ b/docs/ndp/vect.tex @@ -0,0 +1,363 @@ +\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*{\ 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 \ +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 \ 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 \ we +automatically define its dictionary \. Moreover, for every +in-scope type variable \<\alpha\> we have its dictionary +\. 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 \, there exists a vectorised +version \ (which can be the same as \). 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 (\) and global variables and +literals \. 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 \, there exists a +vectorised version \, 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 \. 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 +\ 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 \. 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 \. Unfortunately, this means that +\ 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 \ in \) +\\ +\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 \ 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 \, i.e., the vectoriser +returned \textbf{Maybe}, we leave the definition of \ 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 +\, we change the definition of \ to +\begin{haskell} +f :: \sigma = unconv_\sigma f_v +\end{haskell} + +\item Otherwise (the vectoriser said \textbf{Yes} but we do not have +\ or if \ couldn't be fully vectorised), we change the +definition of \ to +\begin{haskell} +f :: \sigma = e' +\end{haskell} +where \ is obtaining by vectorising \ 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., +\). +\end{itemize} + +\end{document} +