diff options
Diffstat (limited to 'docs/ndp')
| -rw-r--r-- | docs/ndp/haskell.sty | 496 | ||||
| -rw-r--r-- | docs/ndp/vect.tex | 363 |
2 files changed, 0 insertions, 859 deletions
diff --git a/docs/ndp/haskell.sty b/docs/ndp/haskell.sty deleted file mode 100644 index 3e4d478b1e..0000000000 --- a/docs/ndp/haskell.sty +++ /dev/null @@ -1,496 +0,0 @@ -%%% 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 occurrence 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 deleted file mode 100644 index bf1e25842b..0000000000 --- a/docs/ndp/vect.tex +++ /dev/null @@ -1,363 +0,0 @@ -\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 variable. 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}] \pa{\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 occurrences 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 additionally 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} - |