compiler.lyx

#LyX 2.0 created this file. For more info see http://www.lyx.org/
\lyxformat 413
\begin_document
\begin_header
\textclass article
\begin_preamble
\usepackage{amsmath, amssymb, mathpartir, mathtools, minibox, plstx, stmaryrd}

\newcommand\llb{\left\llbracket}
\newcommand\rrb{\right\rrbracket}
\newcommand{\sequence}[1]{#1 \, \dots \,}

\newcommand{\arr}{\mathit{\alpha}}
\newcommand{\base}{\mathit{b}}
\newcommand{\basetype}{\mathit{B}}
\newcommand{\elt}{\mathit{l}}
\newcommand{\expr}{\mathit{e}}
\newcommand{\fun}{\mathit{f}}
\newcommand{\idx}{\mathit{\iota}}
 \newcommand{\altidx}{\mathit{\kappa}}
\newcommand{\integer}{\mathit{z}}
\newcommand{\nat}{\mathit{n}}
 \newcommand{\altnat}{\mathit{m}}
 \newcommand{\altaltnat}{\mathit{k}}
\newcommand{\op}{\mathit{\pi}}
\newcommand{\rank}{\mathit{\rho}}
\newcommand{\sort}{\mathit{\gamma}}
\newcommand{\type}{\mathit{\tau}}
\newcommand{\alttype}{\mathit{\sigma}}
\newcommand{\val}{\mathit{v}}
\newcommand{\var}{\mathit{x}}
\newcommand{\altvar}{\mathit{y}}


\newcommand{\annotate}[2][]{{#2}^{#1}}
\newcommand{\arrlit}[2]{\left[ #1 \right]_{#2}}
\newcommand{\app}[2]{\left( #1 \; #2 \right)}
\newcommand{\tlam}[2]{\left( {\tt T\lambda} \left[ #1 \right] #2 \right)}
\newcommand{\tapp}[2]{\left( \text{\tt T-APP} \; #1 \; #2 \right)}
\newcommand{\ilam}[2]{\left( {\tt I\lambda} \left[ #1 \right] #2 \right)}
\newcommand{\iapp}[2]{\left( \text{\tt I-APP} \; #1 \; #2 \right)}
\newcommand{\pack}[3]{\left( {\tt PACK} \; #1 #2 \;\; {\tt as} \; #3  \right)}
\newcommand{\unpack}[4]{\left( {\tt UNPACK} \; \left( \left\langle #1 | #2 \right\rangle = #3 \right) \; #4 \right)}
\newcommand{\tuple}[1]{\left \langle #1 \right \rangle}
\newcommand{\tfield}[2]{#1 \# #2  }
\newcommand{\letbind}[3]{ {\tt LET} \; #1 = #2 \; {\tt IN} \; #3 }
\newcommand{\lam}[2]{ \left( \lambda \; \left( #1 \right) \; #2  \right) }


\newcommand{\typearray}[2]{{\tt A}_{#1} #2}
\newcommand{\typefun}[2]{\left( #1 \rightarrow #2 \right)}
\newcommand{\typeclosure}[2]{\left( #1 \xrightarrow{Cls} #2 \right)}
\newcommand{\typeuniv}[2]{\left( \forall \left[ #1 \right] #2 \right)}
\newcommand{\typeprod}[2]{\left( \Pi \left[ #1 \right] #2 \right)}
\newcommand{\typesum}[2]{\left( \Sigma \left[ #1 \right] #2 \right)}
\newcommand{\typetuple}[2]{\left( #1 \, \times \, #2  \right)}

\newcommand{\idxshape}[1]{\left( {\tt S} #1 \right)}
\newcommand{\idxplus}[2]{\left( {\tt +} \; #1 \; #2 \right)}

\newcommand{\erasedapp}[3]{\left( #1 \; #2 \; | \; #3 \right)}
\newcommand{\erasedpack}[2]{\left( {\tt PACK} \; #1 #2  \right)}

\newcommand{\erasedbasetype}{\tt Base}
\newcommand{\erasedvartype}{\tt Var}

\newcommand{\mrtuple}[1]{\left \langle #1 \right \rangle}
\newcommand{\mrlet}[3]{\left( {\tt LET} \; \mrtuple{#1} \; {\tt =} \; #2 \; {\tt in} \; #3 \right)}
\newcommand{\mrletbr}[3]{\minibox {$ \left( {\tt LET} \; \mrtuple{#1} \; {\tt =} \; #2 \right. $ \\ $ \left. \qquad {\tt in} \; #3 \right) $}}
\newcommand{\mrvec}[2]{\left( {\tt VEC} \; #2 \; | \; #1 \right)}
\newcommand{\mrrep}[3]{\left( {\tt REP} \; #1 \; #2 \Rightarrow \; #3 \right)}
\newcommand{\mrmap}[4]{\left(  {\tt MAP} \; #1\; #2 \; #3 \; | \; #4 \right) }
\newcommand{\mrmapbr}[4]{\minibox{$\left( {\tt MAP} #1 \right. $ \\ $ \qquad #2 $ \\ $ \qquad #3 $ \\ $ \left. \qquad #4 \right)$}}
\newcommand{\applyfun}[2]{\lam{#1 \; #2}{\app{#1}{#2}}}

\newcommand{\eraseE}[1]{\llb #1 \rrb _E}
\newcommand{\eraseL}[1]{\llb #1 \rrb _L}
\newcommand{\eraseT}[1]{\llb #1 \rrb _T}
\newcommand{\eraseI}[1]{\llb #1 \rrb _I}
\newcommand{\eraseA}[1]{\llb #1 \rrb _A}

\newcommand{\mangle}[1]{\left( \mathit{Mangle}\llb #1 \rrb \right)}
\newcommand{\length}[1]{\left( \mathit{Length}\llb #1 \rrb \right)}
\newcommand{\appframe}[1]{\left( \mathit{AppFrame}\llb #1 \rrb \right)}
\newcommand{\argframe}[1]{\left( \mathit{ArgFrame}\llb #1 \rrb \right)}
\newcommand{\expansion}[1]{\left( \mathit{Expansion}\llb #1 \rrb \right)}
\end_preamble
\use_default_options true
\maintain_unincluded_children false
\language english
\language_package default
\inputencoding auto
\fontencoding global
\font_roman default
\font_sans default
\font_typewriter default
\font_default_family default
\use_non_tex_fonts false
\font_sc false
\font_osf false
\font_sf_scale 100
\font_tt_scale 100

\graphics default
\default_output_format default
\output_sync 0
\bibtex_command default
\index_command default
\paperfontsize default
\spacing single
\use_hyperref false
\papersize default
\use_geometry false
\use_amsmath 1
\use_esint 1
\use_mhchem 1
\use_mathdots 1
\cite_engine basic
\use_bibtopic false
\use_indices false
\paperorientation portrait
\suppress_date false
\use_refstyle 1
\index Index
\shortcut idx
\color #008000
\end_index
\secnumdepth 3
\tocdepth 3
\paragraph_separation indent
\paragraph_indentation default
\quotes_language english
\papercolumns 1
\papersides 1
\paperpagestyle default
\tracking_changes false
\output_changes false
\html_math_output 0
\html_css_as_file 0
\html_be_strict false
\end_header

\begin_body

\begin_layout Title
Remora Compiler Overview
\end_layout

\begin_layout Section
Introduction
\end_layout

\begin_layout Standard
- compiler for array-oriented language
\end_layout

\begin_layout Standard
-- high-level approach to data-parallelism
\end_layout

\begin_layout Standard
-- implicit iteration space
\end_layout

\begin_layout Standard
--- determined statically by types
\end_layout

\begin_layout Standard
- targeting GPU via NVJIT
\end_layout

\begin_layout Standard
-- builds on LLVM
\end_layout

\begin_layout Standard
-- JIT decides whether to parallelize a loop on GPU
\end_layout

\begin_layout Standard
- export Passes module for each 
\begin_inset Quotes eld
\end_inset

phase
\begin_inset Quotes erd
\end_inset

 of compilation
\end_layout

\begin_layout Standard
-- procedures which execute just this phase's passes
\end_layout

\begin_layout Standard
-- procedures which execute this and all previous phases' passes
\end_layout

\begin_layout Section
Remora Abstract Syntax
\end_layout

\begin_layout Standard
Expressions are meant to represent arrays.
 A separate syntax class is used to allow non-array terms (functions and
 base values) to appear as array elements.
 The compiler currently does not support empty array notation (it would
 require a type declaration on the array itself).
 In the following grammar, 
\begin_inset Formula $\base$
\end_inset

 stands for base values (such as floats and booleans) and 
\begin_inset Formula $\basetype$
\end_inset

 for base types.
\end_layout

\begin_layout Standard
\begin_inset Preview

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
begin{plstx}
\end_layout

\begin_layout Plain Layout

	(expressions): 
\backslash
expr
\end_layout

\begin_layout Plain Layout

	::= 
\backslash
arr
\end_layout

\begin_layout Plain Layout

	| 
\backslash
var
\end_layout

\begin_layout Plain Layout

	| 
\backslash
app{
\backslash
expr}{
\backslash
sequence{
\backslash
expr}}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
tlam{
\backslash
sequence{
\backslash
var}}{
\backslash
expr}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
tapp{
\backslash
expr}{
\backslash
sequence{
\backslash
type}}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
ilam{
\backslash
sequence{
\backslash
var}}{
\backslash
expr}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
iapp{
\backslash
expr}{
\backslash
sequence{
\backslash
idx}}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
pack{
\backslash
sequence{
\backslash
idx}}{
\backslash
expr}{
\backslash
type}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
unpack{
\backslash
sequence{
\backslash
var}}{
\backslash
altvar}{
\backslash
expr}{
\backslash
expr'}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
tuple{
\backslash
sequence{
\backslash
expr}}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
tfield{
\backslash
expr}{
\backslash
nat}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
letbind{
\backslash
tuple{
\backslash
sequence{
\backslash
var}}}{
\backslash
expr}{
\backslash
expr'}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
letbind{
\backslash
var}{
\backslash
expr}{
\backslash
expr'} 
\backslash

\backslash

\end_layout

\begin_layout Plain Layout

	(arrays): 
\backslash
arr
\end_layout

\begin_layout Plain Layout

	::= 
\backslash
arrlit{
\backslash
sequence{
\backslash
elt}}{
\backslash
sequence{
\backslash
nat}} 
\backslash

\backslash

\end_layout

\begin_layout Plain Layout

	(array elements): 
\backslash
elt
\end_layout

\begin_layout Plain Layout

	::= 
\backslash
base
\end_layout

\begin_layout Plain Layout

	| 
\backslash
lam{
\backslash
sequence{
\backslash
left(
\backslash
var 
\backslash
; 
\backslash
type 
\backslash
right)}}{
\backslash
expr}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
expr 
\backslash

\backslash

\end_layout

\begin_layout Plain Layout

	(types): 
\backslash
type, 
\backslash
alttype
\end_layout

\begin_layout Plain Layout

	::= 
\backslash
basetype
\end_layout

\begin_layout Plain Layout

	| 
\backslash
var
\end_layout

\begin_layout Plain Layout

	| 
\backslash
typearray{
\backslash
idx}{
\backslash
type}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
typefun{
\backslash
sequence{
\backslash
type}}{
\backslash
alttype}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
typeuniv{
\backslash
sequence{
\backslash
var}}{
\backslash
type}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
typeprod{
\backslash
sequence{
\backslash
left( 
\backslash
var 
\backslash
; 
\backslash
sort 
\backslash
right)}}{
\backslash
type}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
typesum{
\backslash
sequence{
\backslash
left( 
\backslash
var 
\backslash
; 
\backslash
sort 
\backslash
right)}}{
\backslash
type}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
typetuple{
\backslash
type}{
\backslash
sequence{
\backslash
alttype}} 
\backslash

\backslash

\end_layout

\begin_layout Plain Layout

	(type indices): 
\backslash
idx, 
\backslash
altidx
\end_layout

\begin_layout Plain Layout

	::= 
\backslash
nat
\end_layout

\begin_layout Plain Layout

	| 
\backslash
var
\end_layout

\begin_layout Plain Layout

	| 
\backslash
idxshape{
\backslash
;
\backslash
sequence{
\backslash
idx}}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
idxplus{
\backslash
idx}{
\backslash
altidx}
\end_layout

\begin_layout Plain Layout


\backslash

\backslash

\end_layout

\begin_layout Plain Layout


\backslash
end{plstx}
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
Within the compiler, types and type indices are defined as algebraic data
 types (with an optional sort tag on index variables):
\begin_inset listings
inline false
status collapsed

\begin_layout Plain Layout

type idx =
\end_layout

\begin_layout Plain Layout

| INat of int
\end_layout

\begin_layout Plain Layout

| IShape of idx list
\end_layout

\begin_layout Plain Layout

| ISum of idx * idx
\end_layout

\begin_layout Plain Layout

| IVar of var * srt option
\end_layout

\begin_layout Plain Layout

\end_layout

\begin_layout Plain Layout

type typ =
\end_layout

\begin_layout Plain Layout

| TFloat
\end_layout

\begin_layout Plain Layout

| TInt
\end_layout

\begin_layout Plain Layout

| TBool
\end_layout

\begin_layout Plain Layout

| TDProd of (var * srt) list * typ
\end_layout

\begin_layout Plain Layout

| TDSum of (var * srt) list * typ
\end_layout

\begin_layout Plain Layout

| TFun of typ list * typ
\end_layout

\begin_layout Plain Layout

| TArray of idx * typ
\end_layout

\begin_layout Plain Layout

| TProd of typ list
\end_layout

\begin_layout Plain Layout

| TAll of var list * typ
\end_layout

\begin_layout Plain Layout

| TVar of var 
\end_layout

\end_inset


\end_layout

\begin_layout Standard
The term-level pieces (
\begin_inset Formula $\expr$
\end_inset

 and 
\begin_inset Formula $\elt$
\end_inset

) are parameterized over the types of their subterms:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status collapsed

\begin_layout Plain Layout

type ('self_t, 'elt_t) expr_form =
\end_layout

\begin_layout Plain Layout

| App of 'self_t * 'self_t list
\end_layout

\begin_layout Plain Layout

| TApp of 'self_t * typ list
\end_layout

\begin_layout Plain Layout

| TLam of var list * 'self_t
\end_layout

\begin_layout Plain Layout

| IApp of 'self_t * idx list
\end_layout

\begin_layout Plain Layout

| ILam of (var * srt) list * 'self_t
\end_layout

\begin_layout Plain Layout

| Let of var * 'self_t * 'self_t
\end_layout

\begin_layout Plain Layout

| Arr of int list * 'elt_t list
\end_layout

\begin_layout Plain Layout

| Tuple of 'self_t list
\end_layout

\begin_layout Plain Layout

| Field of int * 'self_t
\end_layout

\begin_layout Plain Layout

| LetTup of var list * 'self_t * 'self_t
\end_layout

\begin_layout Plain Layout

| Var of var
\end_layout

\begin_layout Plain Layout

| Pack of idx list * 'self_t * typ
\end_layout

\begin_layout Plain Layout

| Unpack of var list * var * 'self_t * 'self_t
\end_layout

\begin_layout Plain Layout

and ('self_t, 'expr_t) elt_form =
\end_layout

\begin_layout Plain Layout

| Float of float
\end_layout

\begin_layout Plain Layout

| Int of int
\end_layout

\begin_layout Plain Layout

| Bool of bool
\end_layout

\begin_layout Plain Layout

| Lam of (var * typ) list * 'expr_t
\end_layout

\begin_layout Plain Layout

| Expr of 'expr_t
\end_layout

\end_inset


\end_layout

\begin_layout Standard
A pair of mapping functions 
\family typewriter
map_expr_form
\family default
 and 
\family typewriter
map_elt_form
\family default
 can be used to repeat some operation on every subterm.
 These are useful for AST traversals which only do nontrivial work at particular
 nodes -- the noninteresting cases (such as annotating the function application
 frame in a non-
\family typewriter
App
\family default
 node) can be skipped over.
\end_layout

\begin_layout Standard
Delaying the recursion makes it easy to create different versions of the
 AST.
 First, a simple version with ordinary expressions/elements as subterms
 can encode a source program:
\begin_inset listings
inline false
status collapsed

\begin_layout Plain Layout

type rem_expr = RExpr of (rem_expr, rem_elt) expr_form
\end_layout

\begin_layout Plain Layout

and rem_elt = RElt of (rem_elt, rem_expr) elt_form
\end_layout

\end_inset


\end_layout

\begin_layout Standard
Another version includes an annotation at each term node:
\begin_inset listings
inline false
status collapsed

\begin_layout Plain Layout

type 'annot ann_expr =
\end_layout

\begin_layout Plain Layout

  AnnRExpr of 'annot *
\end_layout

\begin_layout Plain Layout

              ('annot ann_expr, 'annot ann_elt) expr_form
\end_layout

\begin_layout Plain Layout

and 'annot ann_elt =
\end_layout

\begin_layout Plain Layout

  AnnRElt of 'annot *
\end_layout

\begin_layout Plain Layout

             ('annot ann_elt, 'annot ann_expr) elt_form 
\end_layout

\end_inset


\end_layout

\begin_layout Standard
The ASTs are treated as persistent data structures.
 When possible, functions which operate on them will reuse existing nodes
 rather than allocating new ones.
\end_layout

\begin_layout Standard
Functions are provided for converting between the two representations (either
 removing annotations or inserting caller-designated 
\begin_inset Quotes eld
\end_inset

blank
\begin_inset Quotes erd
\end_inset

 annotations).
 There are also functions which apply a given function to every annotation
 (treating the AST like a Functor instance).
 Another set of functions applies a specified operation to corresponding
 pairs of annotations in two ASTs of the same shape.
 These functions produce an 
\family typewriter
option
\family default
 AST in case the two argument ASTs do not match in shape.
\end_layout

\begin_layout Standard
A top-level definition has a bound name, a type declaration, and an expression
 (possibly annotated).
 A program consists of a list of top-level definitions (which are allowed
 to refer to each other) and an expression.
 An annotated program includes an annotation representing the entire program,
 but an annotated definition only has annotations within its body.
\begin_inset listings
inline false
status collapsed

\begin_layout Plain Layout

type rem_defn = RDefn of var * typ * rem_expr
\end_layout

\begin_layout Plain Layout

type rem_prog = RProg of rem_defn list * rem_expr
\end_layout

\begin_layout Plain Layout

type 'annot ann_defn =
\end_layout

\begin_layout Plain Layout

  AnnRDefn of var * typ * 'annot ann_expr
\end_layout

\begin_layout Plain Layout

type 'annot ann_prog =
\end_layout

\begin_layout Plain Layout

  AnnRProg of 'annot * 'annot ann_defn list * 'annot ann_expr 
\end_layout

\end_inset


\end_layout

\begin_layout Section
Type checking
\end_layout

\begin_layout Standard
The full typing rules for Remora (except for the let-binding and tuple-related
 forms added here) are given in the 
\begin_inset CommandInset href
LatexCommand href
name "ESOP 2014 paper"
target "http://www.ccs.neu.edu/home/jrslepak/esop14-full.pdf"

\end_inset

 and implemented in the 
\begin_inset CommandInset href
LatexCommand href
name "Redex model"
target "https://github.com/jrslepak/Remora/tree/master/semantics"

\end_inset

.
 The type checking pass generates 
\family typewriter
typ option
\family default
 annotations.
 Well-typed parts of an ill-typed program's AST will have types ascribed
 to them.
 For example, an array containing a 2-vector and a 3-vector cannot be given
 a type, but each of those two vectors may still be typable.
\end_layout

\begin_layout Standard
The environment structure consists of lists mapping the current in-scope
 index, type, and term variables to their respective sorts, kinds, and types.
 Remora currently does not include higher-order polymorphism, so there is
 only one kind (represented in code by the 
\family typewriter
unit
\family default
 type).
\end_layout

\begin_layout Standard
The code makes heavy use of OCaml Core's monadic interface for 
\family typewriter
option
\family default
s.
 This interface allows a sequence where each operation assumes all previous
 operations have succeeded.
 Once any operation in the sequence fails, the rest are skipped, and the
 result is automatically 
\family typewriter
None
\family default
.
 If all operations succeed, the final one will 
\family typewriter
return
\family default
 a value 
\family typewriter
v
\family default
, leaving 
\family typewriter
Some v
\family default
 as the result of the operation sequence.
\end_layout

\begin_layout Standard
Once an AST has 
\family typewriter
typ option
\family default
 annotations, it can be converted to either 
\family typewriter
Some
\family default
 AST with (non-option) 
\family typewriter
typ
\family default
 annotations if it is well-typed or 
\family typewriter
None
\family default
 if it is ill-typed.
 The rest of the compiler can then assume it is working with a fully well-typed
 program.
\end_layout

\begin_layout Standard
Each term node variant has a corresponding case in the type checker.
\end_layout

\begin_layout Subsection*

\family typewriter
App (fn, [arg ...])
\end_layout

\begin_layout Standard
Check the types of 
\family typewriter
fn
\family default
 and each 
\family typewriter
arg
\family default
.
 The type of 
\family typewriter
fn
\family default
 must be an array of
\family typewriter
 TFun ([cell_typ ...], ret_typ)
\family default
, or 
\begin_inset Formula $\typefun{\sequence{\tt cell\_typ}}{\tt ret\_typ}$
\end_inset

.
 Comparing each cell type 
\family typewriter
in
\family default
 to the type of the corresponding 
\family typewriter
arg
\family default
 gives that argument's 
\family typewriter
arg_frame_shape
\family default
.
 The shape of 
\family typewriter
fn
\family default
's type, 
\family typewriter
fun_shape
\family default
, is the frame shape for 
\family typewriter
fn
\family default
.
 Find the largest frame shape 
\family typewriter
prefix_max
\family default
 (according to prefix ordering).
 The result type for this application is an array with shape 
\family typewriter
prefix_max
\family default
 and element type 
\family typewriter
ret_typ
\family default
.
\end_layout

\begin_layout Subsection*

\family typewriter
TApp (fn, [typ_arg ...])
\end_layout

\begin_layout Standard
Check the type of fn (the arguments are types, which need no annotation).
 
\family typewriter
fn
\family default
's type must be of the form 
\family typewriter
TAll ([tvar...], tbody)
\family default
, or 
\begin_inset Formula $\typeuniv{\sequence{\tt tvar}}{\tt {tbody}}$
\end_inset

.
 There must be as many 
\family typewriter
typ_arg
\family default
s as there are 
\family typewriter
tvar
\family default
s, and every 
\family typewriter
typ_arg
\family default
 must be a non-array type.
 If these conditions are met, return 
\family typewriter
tbody
\family default
 with free occurrences of 
\family typewriter
tvars
\family default
 replaced with the corresponding 
\family typewriter
typ_arg
\family default
s.
\end_layout

\begin_layout Subsection*

\family typewriter
TLam (bindings, body)
\end_layout

\begin_layout Standard
Use an extended environment which marks the type variables in 
\family typewriter
bindings
\family default
 as in-scope to find the type 
\family typewriter
body_annot
\family default
 of 
\family typewriter
body
\family default
.
 If 
\family typewriter
body
\family default
 is well-typed, return 
\family typewriter
TAll (bindings, body_type)
\family default
.
\end_layout

\begin_layout Subsection*

\family typewriter
IApp (fn, [idx_arg ...])
\end_layout

\begin_layout Standard
Ensure 
\family typewriter
fn
\family default
's type has the form 
\family typewriter
TDProd ([(ivar, s) ...], tbody)
\family default
, or in abstract notation 
\begin_inset Formula $\typeprod{\sequence{({\tt ivar}\;{\tt s})}}{\tt tbody}$
\end_inset

.
 Each idx_arg must have the corresponding sort 
\family typewriter
s
\family default
.
 If the sorts all match, the type is 
\family typewriter
tbody
\family default
 with each 
\family typewriter
idx_arg
\family default
 substituted for its 
\family typewriter
ivar
\family default
.
 Index variable sort tags are updated as needed.
\end_layout

\begin_layout Subsection*

\family typewriter
ILam (bindings, body)
\end_layout

\begin_layout Standard
Find the type 
\family typewriter
body_type
\family default
 of 
\family typewriter
body
\family default
 using an environment extended according to 
\family typewriter
bindings
\family default
.
 Return 
\family typewriter
DProd (bindings, body_type)
\family default
.
\end_layout

\begin_layout Subsection*

\family typewriter
Let (var, bound, body)
\end_layout

\begin_layout Standard
Find the type 
\family typewriter
bound_type
\family default
 of 
\family typewriter
bound
\family default
.
 Construct a new environment entry binding 
\family typewriter
var
\family default
 at 
\family typewriter
bound_type
\family default
.
 Find the type 
\family typewriter
body_type
\family default
, by checking 
\family typewriter
body
\family default
 with an environment extended with that new entry.
 Return 
\family typewriter
body_type
\family default
.
\end_layout

\begin_layout Subsection*

\family typewriter
Arr ([dim ...], [elt ...])
\end_layout

\begin_layout Standard
Check the type of each 
\family typewriter
elt
\family default
.
 Find the product of the 
\family typewriter
dim
\family default
s, and make sure that it matches the number 
\family typewriter
elt
\family default
s.
 If the 
\family typewriter
elt
\family default
 types are all equivalent to the same type 
\family typewriter
uniq_elt_type
\family default
, then construct a shape index 
\family typewriter
ashp
\family default
 from the declared dimensions, and return 
\family typewriter
TArray (array_shape, uniqt)
\family default
, or 
\begin_inset Formula $\typearray{\tt ashp}{\tt uniqt}$
\end_inset

 in abstract notation.
\end_layout

\begin_layout Subsection*

\family typewriter
Tuple [elt ...]
\end_layout

\begin_layout Standard
Check the type 
\family typewriter
t
\family default
 of each 
\family typewriter
elt
\family default
.
 If all of the elts are well-typed, return 
\family typewriter
TProd [t ...]
\family default
.
\end_layout

\begin_layout Subsection*

\family typewriter
Field (num, tup)
\end_layout

\begin_layout Standard
Check the type of 
\family typewriter
tup
\family default
.
 It must have the form
\family typewriter
 TProd ft
\family default
, where 
\family typewriter
ft
\family default
 is a list of types with at least (
\family typewriter
num
\family default
 + 1) elements.
 If so, return the 
\family typewriter
num
\family default
th type.
\end_layout

\begin_layout Subsection*

\family typewriter
LetTup ([var ...], tup, body)
\end_layout

\begin_layout Standard
Again, begin by checking that the type of 
\family typewriter
tup
\family default
 has the form 
\family typewriter
TProd ft
\family default
, where the length of 
\family typewriter
ft
\family default
 is the same as the number of 
\family typewriter
var
\family default
s being bound.
 Construct new term environment entries binding each 
\family typewriter
var
\family default
 at the corresponding element of 
\family typewriter
ft
\family default
.
 Using an environment extended with these entries, find the of 
\family typewriter
body
\family default
 and return it.
 If we were unable to add any environment entries because 
\family typewriter
tup
\family default
 is ill-typed or does not have a tuple type, we still attempt to type check
 
\family typewriter
body
\family default
, but we mark this 
\family typewriter
LetTup
\family default
 form as ill-typed.
\end_layout

\begin_layout Subsection*

\family typewriter
Pack ([i ...], e, TDSum ([(ivar, s) ...], t))
\end_layout

\begin_layout Standard
Note that if the type declaration does not have this form, this expression
 is ill-typed.
 Otherwise, ensure each index 
\family typewriter
i
\family default
 has the corresponding declared sort 
\family typewriter
s
\family default
.
 Substituting the indices 
\family typewriter
[i ...]
\family default
 for the variables 
\family typewriter
ivar...

\family default
 in 
\family typewriter
t
\family default
 must produce a type equivalent to the type of 
\family typewriter
e
\family default
.
 If so, return 
\family typewriter
TDSum ([(ivar, s) ...], t)
\family default
, which is written 
\begin_inset Formula $\typesum{\sequence{({\tt ivar}\;{\tt s})}}{\tt t}$
\end_inset

 in abstract notation.
 As in the 
\family typewriter
IApp
\family default
 case, index variables' sort tags are corrected.
\end_layout

\begin_layout Subsection*

\family typewriter
Unpack ([ivar ...], v, dsum, body)
\end_layout

\begin_layout Standard
Type check 
\family typewriter
dsum
\family default
, whose type must be a dependent sum 
\family typewriter
TDSum ([witness ...], t)
\family default
.
 Construct new environment entries binding each ivar at the sort of the
 corresponding witness and v at type t.
 Use this new environment to type check body, but make sure the resulting
 type is well-formed 
\emph on
without
\emph default
 the new environment entries -- do not allow any witnesses to escape.
 In the type checker's current state, this form is only useful if the bound
 index variables have the same names as the dependent sum's witnesses.
\end_layout

\begin_layout Subsection*

\family typewriter
Var name
\end_layout

\begin_layout Standard
If the environment has name bound at any type, return that type.
\end_layout

\begin_layout Subsection*

\family typewriter
Lam (bindings, body)
\end_layout

\begin_layout Standard
Extend the environment with the 
\family typewriter
Lam
\family default
 form's new term variable bindings, and use the extended environment to
 find 
\family typewriter
body
\family default
's type 
\family typewriter
t
\family default
.
 If every argument's type declaration is for a well-formed type 
\family typewriter
s
\family default
, then return 
\family typewriter
TFun ([s ...], t)
\family default
, or 
\begin_inset Formula $\typefun{\sequence{\tt s}}{\tt t}$
\end_inset

 in abstract notation.
\end_layout

\begin_layout Subsection*

\family typewriter
Expr e
\end_layout

\begin_layout Standard
For an expression 
\family typewriter
e
\family default
 used as an array element, simply return the type of 
\family typewriter
e
\family default
.
\end_layout

\begin_layout Section
Frame annotation
\end_layout

\begin_layout Standard
Type annotations supply the information needed to know how each function
 gets mapped over its arguments and how each argument gets replicated.
 
\end_layout

\begin_layout Standard
The first pass identifies the principal frame in every 
\family typewriter
App
\family default
 form.
 Each AST node gets annotated with an 
\family typewriter
app_frame
\family default
 -- either 
\family typewriter
NotApp
\family default
 if it is not an 
\family typewriter
App
\family default
 node or 
\family typewriter
AppFrame ([i ...])
\family default
 if it is.
 This type is isomorphic to 
\family typewriter
idx list option
\family default
, but using a separate type helps OCaml's type system enforce proper usage.
 On an 
\family typewriter
App
\family default
 form, compare the return type for the function position (we have a well-typed
 AST, so we know this has atoms of function type) with the type ascribed
 to the entire 
\family typewriter
App
\family default
 form.
 The axes added to the return type are the principal frame for the application.
\end_layout

\begin_layout Standard
Given both type and application frame annotations, we have enough information
 to identify the frames of individual arguments -- what frame axes they
 already have and what axes they must gain via replication.
 An argument frame annotation is an 
\family typewriter
arg_frame
\family default
 -- either 
\family typewriter
NotArg
\family default
 or 
\family typewriter
ArgFrame {frame = [i ...]; expansion = [j ...]}
\family default
.
 Annotating an argument requires knowing some information about the parent
 AST node: the expected cell type (a 
\family typewriter
typ option
\family default
) for that argument and the principal frame (an 
\family typewriter
app_frame
\family default
).
 These are passed in as additional arguments to the argument frame annotation
 pass.
\end_layout

\begin_layout Standard
Every node must compute the argument frame and required expansion from the
 passed-in data.
 The recursive call depends on node variant.
 On an App node, extract the expected cell types [t ...] from the 
\family typewriter
typ
\family default
 annotation at function position (this relies on having a well-typed AST)
 and the application frame 
\family typewriter
node_app_frame
\family default
 from the 
\family typewriter
app_frame
\family default
 annotation on the 
\family typewriter
App
\family default
 form.
 Then recur on each subterm with 
\family typewriter
Some t
\family default
 and 
\family typewriter
node_app_frame
\family default
.
 For non-App nodes, recur with 
\family typewriter
None
\family default
 and 
\family typewriter
NotApp
\family default
.
\end_layout

\begin_layout Section
Type-erased Abstract Syntax
\end_layout

\begin_layout Standard
The only part of Remora's dynamic semantics that requires type information
 is choosing the result of a function application with an empty frame.
 This compiler will leverage type information in other cases (such as consulting
 type annotations to determine what size buffer is needed to hold the atoms
 of an array), but these are not semantic issues.
 The formal presentation of the semantics has a type annotation on every
 term (these can be constructed from partial annotations) and reduces an
 empty-frame application form to the unique inhabitant of that form's type
 (there is, for example, only one empty vector of Booleans).
 This type information is only needed to select the 
\emph on
shape
\emph default
 of the result array, so only the shape-related portion of a type is computation
ally relevant.
 The type of the atoms in an array does not matter for semantic correctness
 but is retained to allow better code generation.
\end_layout

\begin_layout Standard
To avoid looking up types at run time, we use an application form with a
 shape declaration, which will be used to handle lifting in an empty frame.
 This declaration may use index variables, so ILam, IApp, Pack, and Unpack
 forms still matter.
 We can drop TLam and TApp forms and replace all type variables with an
 
\begin_inset Quotes eld
\end_inset

unknown atom type
\begin_inset Quotes erd
\end_inset

 marker (recall, type variables are not allowed to stand for array types).
\end_layout

\begin_layout Standard
The target syntax of this pass is:
\end_layout

\begin_layout Standard
\begin_inset Preview

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
begin{plstx}
\end_layout

\begin_layout Plain Layout

(expressions): 
\backslash
expr
\end_layout

\begin_layout Plain Layout

	::= 
\backslash
erasedapp{
\backslash
expr}{
\backslash
sequence{
\backslash
expr}}{
\backslash
type}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
arrlit{
\backslash
sequence{
\backslash
elt}}{
\backslash
sequence{
\backslash
nat}}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
iapp{
\backslash
expr}{
\backslash
sequence{
\backslash
idx}}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
ilam{
\backslash
sequence{
\backslash
left(
\backslash
var 
\backslash
; 
\backslash
sort 
\backslash
right)}}{
\backslash
expr}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
var
\end_layout

\begin_layout Plain Layout

	| 
\backslash
erasedpack{
\backslash
sequence{
\backslash
idx}}{
\backslash
expr}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
unpack{
\backslash
sequence{
\backslash
var}}{
\backslash
altvar}{
\backslash
expr}{
\backslash
expr}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
tuple{
\backslash
sequence{
\backslash
expr}}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
tfield{
\backslash
expr}{
\backslash
nat}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
letbind{
\backslash
tuple{
\backslash
sequence{
\backslash
var}}}{
\backslash
expr}{
\backslash
expr'}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
letbind{
\backslash
var}{
\backslash
expr}{
\backslash
expr'}
\end_layout

\begin_layout Plain Layout


\backslash

\backslash

\end_layout

\begin_layout Plain Layout

(array elements): 
\backslash
elt
\end_layout

\begin_layout Plain Layout

	::= 
\backslash
base
\end_layout

\begin_layout Plain Layout

	| 
\backslash
lam{
\backslash
sequence{
\backslash
var}}{
\backslash
expr}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
expr
\end_layout

\begin_layout Plain Layout


\backslash

\backslash

\end_layout

\begin_layout Plain Layout

(types): 
\backslash
type, 
\backslash
alttype
\end_layout

\begin_layout Plain Layout

	::= 
\backslash
basetype
\end_layout

\begin_layout Plain Layout

	| 
\backslash
erasedvartype
\end_layout

\begin_layout Plain Layout

	| 
\backslash
typefun{
\backslash
sequence{
\backslash
type}}{
\backslash
alttype}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
typeclosure{
\backslash
sequence{
\backslash
type}}{
\backslash
alttype}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
typeprod{
\backslash
sequence{
\backslash
left( 
\backslash
var 
\backslash
; 
\backslash
sort 
\backslash
right)}}{
\backslash
type}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
typesum{
\backslash
sequence{
\backslash
left( 
\backslash
var 
\backslash
; 
\backslash
sort 
\backslash
right)}}{
\backslash
type}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
typearray{
\backslash
idx}{
\backslash
type}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
typetuple{
\backslash
type}{
\backslash
sequence{
\backslash
alttype}}
\end_layout

\begin_layout Plain Layout


\backslash

\backslash

\end_layout

\begin_layout Plain Layout

	(type indices): 
\backslash
idx, 
\backslash
altidx
\end_layout

\begin_layout Plain Layout

	::= 
\backslash
nat
\end_layout

\begin_layout Plain Layout

	| 
\backslash
var
\end_layout

\begin_layout Plain Layout

	| 
\backslash
idxshape{
\backslash
;
\backslash
sequence{
\backslash
idx}}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
idxplus{
\backslash
idx}{
\backslash
altidx}
\end_layout

\begin_layout Plain Layout


\backslash

\backslash

\end_layout

\begin_layout Plain Layout


\backslash
end{plstx}
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
The compiler first translates the Remora AST without consulting any annotations,
and leaving a special 
\family typewriter
TUnknown
\family default
 value as the result type for each 
\family typewriter
App
\family default
 form (for testing purposes, it is possible to erase an AST that has not
 been typechecked.
 The Remora AST's existing annotations are carried through to the erased
 AST, except when erasing a 
\family typewriter
TLam
\family default
 or 
\family typewriter
TApp
\family default
.
 Since these forms collapse into their expression subterms, their annotations
 must be merged (the default merge procedure just uses the parent node's
 annotation).
 A second pass uses type annotations to replace the 
\family typewriter
TUnknown
\family default
s with the correct result types.
 The erased AST also has mapping and merging operations analogous to those
 of the Remora AST.
\end_layout

\begin_layout Standard
The erasure pass itself is given below.
 The 
\begin_inset Formula $\type$
\end_inset

 in the rule for erasing an application form refers to the otherwise implicit
 type annotation on the AST.
\end_layout

\begin_layout Standard
\begin_inset Formula 
\[
\begin{array}{lcl}
\eraseT{\var} & = & \erasedvartype\\
\eraseT{\basetype} & = & \erasedbasetype\\
\eraseT{\typefun{\sequence{\type}}{\alttype}} & = & \typefun{\sequence{\eraseT{\type}}}{\eraseT{\alttype}}\\
\eraseT{\typearray{\idx}{\type}} & = & \typearray{\idx}{\eraseT{\type}}\\
\eraseT{\typeuniv{\sequence{\var}}{\type}} & = & \eraseT{\type}\\
\eraseT{\typeprod{\sequence{(\var\;\sort)}}{\type}} & = & \typeprod{\sequence{(\var\;\sort)}}{\eraseT{\type}}\\
\eraseT{\typesum{\sequence{(\var\;\sort)}}{\type}} & = & \typesum{\sequence{(\var\;\sort)}}{\eraseT{\type}}\\
\eraseT{\typetuple{\type}{\sequence{\alttype}}} & = & \typetuple{\eraseT{\type}}{\sequence{\eraseT{\alttype}}}\\
\\
\eraseL{\lam{\sequence{(\var\;\type)}}{\expr}} & = & \lam{\sequence{\var}}{\eraseE{\expr}}\\
\eraseL{\base} & = & \base\\
\eraseL{\expr} & = & \eraseE{\expr}\\
\\
\eraseE{\tlam{\sequence{\var}}{\expr}} & = & \eraseE{\expr}\\
\eraseE{\tapp{\expr}{\sequence{\type}}} & = & \eraseE{\expr}\\
\eraseE{\ilam{\sequence{(\var\;\sort)}}{\expr}} & = & \ilam{\sequence{(\var\;\sort)}}{\eraseE{\expr}}\\
\eraseE{\iapp{\expr}{\sequence{\idx}}} & = & \iapp{\eraseE{\expr}}{\sequence{\idx}}\\
\eraseE{\var} & = & \var\\
\eraseE{\arrlit{\sequence{\elt}}{\sequence{\nat}}} & = & \arrlit{\sequence{\eraseL{\elt}}}{\sequence{\nat}}\\
\eraseE{\pack{\sequence{\idx}}{\expr}{\type}} & = & \erasedpack{\sequence{\idx}}{\eraseE{\expr}}\\
\eraseE{\unpack{\sequence{\var}}{\altvar}{\expr}{\expr'}} & = & \unpack{\sequence{\var}}{\altvar}{\eraseE{\expr}}{\eraseE{\expr'}}\\
\eraseE{\app{\expr}{\sequence{\expr'}}^{\type}} & = & \erasedapp{\eraseE{\expr}}{\sequence{\eraseE{\expr'}}}{\eraseT{\type}}\\
\eraseE{\tuple{\sequence{\expr}}} & = & \tuple{\sequence{\eraseE{\expr}}}\\
\eraseE{\tfield{\expr}{\nat}} & = & \tfield{\eraseE{\expr}}{\nat}\\
\eraseE{\letbind{\tuple{\sequence{\var}}}{\expr}{\expr'}} & = & \letbind{\tuple{\sequence{\var}}}{\eraseE{\expr}}{\eraseE{\expr'}}\\
\eraseE{\letbind{\var}{\expr}{\expr'}} & = & \letbind{\var}{\eraseE{\expr}}{\eraseE{\expr'}}\\
\\
\end{array}
\]

\end_inset


\end_layout

\begin_layout Section
Map/Replicate Abstract Syntax
\end_layout

\begin_layout Standard
This phase eliminates the implicit rank-polymorphic mapping.
 Function application lifting is rewritten as explicit map and replicate
 operations.
 The Map/Replicate AST is closer to a conventional 
\begin_inset Formula $\lambda$
\end_inset

-calculus in that expressions, array elements, and type indices are no longer
 separated.
 Function application is now conventional, non-lifting application.
\end_layout

\begin_layout Standard
\begin_inset Preview

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
begin{plstx}
\end_layout

\begin_layout Plain Layout

(expressions): 
\backslash
expr
\end_layout

\begin_layout Plain Layout

	::= 
\backslash
app{
\backslash
expr}{
\backslash
sequence{
\backslash
expr}}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
mrvec{
\backslash
sequence{
\backslash
expr}}{
\backslash
nat}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
mrmap{
\backslash
expr_{frm}}{
\backslash
expr_{fn}}{
\backslash
sequence{
\backslash
expr_{arg}}}{
\backslash
expr_{shp}}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
mrrep{
\backslash
expr}{
\backslash
expr_{frm}}{
\backslash
expr_{exp}}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
mrtuple{
\backslash
sequence{
\backslash
expr}}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
mrlet{
\backslash
sequence{
\backslash
var}}{
\backslash
expr}{
\backslash
expr'}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
letbind{
\backslash
var}{
\backslash
expr}{
\backslash
expr'}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
lam{
\backslash
sequence{
\backslash
var}}{
\backslash
expr}
\end_layout

\begin_layout Plain Layout

	| 
\backslash
var
\end_layout

\begin_layout Plain Layout

	| 
\backslash
base
\end_layout

\begin_layout Plain Layout


\backslash

\backslash

\end_layout

\begin_layout Plain Layout


\backslash
end{plstx}
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
A 
\family typewriter
Map
\family default
 takes as input a (possibly computed) frame shape which specifies how many
 cells to divide each argument array into for mapping.
 The shape argument is used to allocate memory for the final result.
 Given a well-typed program, 
\begin_inset Formula $\expr_{shp}$
\end_inset

 should be a multiple of 
\begin_inset Formula $\expr_{frm}$
\end_inset

.
 A 
\family typewriter
Rep
\family default
 takes arguments specifying the original frame (thus how many cells there
 are) and the expansion (how many copies of each cell to make).
 A 
\family typewriter
Let
\family default
 binds a single variable to an experssion or a sequence of variables to
 the respective elements of a tuple.
 Again, in a Map/Replicate program generated from a valid Remora program,
 a let-binder with multiple variables should only have 
\begin_inset Formula $\expr$
\end_inset

 evaluate to a tuple.
 Remora/erased expressions should still translate to map/replicate expressions
 which produce arrays.
 Merging the term and index namespaces requries name mangling to keep index
 and term variables from shadowing each other.
 A shape is taken to mean the number of elements in an array.
 Because 
\family typewriter
Map
\family default
 splits its argument according to the number of cells and passes each cell
 as a whole to the function, further details about individual array dimensions
 are no longer needed.
 This translation pass requires AST annotations for application and argument
 frame shapes:
\end_layout

\begin_layout Standard
\begin_inset Formula 
\[
\begin{array}[t]{rcl}
\eraseE{\var} & = & \mathit{\var}\\
\eraseE{\ilam{\sequence{(\var\;\sort)}}{\expr}} & = & \lam{\sequence{\mangle{\var}}}{\eraseE{\expr}}\\
\eraseE{\iapp{\expr}{\sequence{\idx}}} & = & \app{\eraseE{\expr}}{\sequence{\eraseI{\idx}}}\\
\eraseE{\erasedpack{\sequence{\idx}}{\expr}} & = & \mrtuple{\sequence{\eraseI{\idx}}\;\eraseE{\expr}}\\
\eraseE{\unpack{\sequence{\var}}{\altvar}{\expr}{\expr'}} & = & \mrletbr{\sequence{\mangle{\var}}\;\altvar}{\eraseE{\expr}}{\eraseE{\expr'}}\\
\eraseE{\erasedapp{\expr}{\sequence{\expr'}}{\type}} & = & \mrmapbr{\appframe{\expr}}{\applyfun{\var}{\sequence{\altvar}}}{\eraseA{\expr}\;\sequence{\eraseA{\expr'}}}{a}\\
\eraseE{\arrlit{\sequence{\elt}}{\sequence{\nat}}} & = & \mrvec{\sequence{\eraseL{\elt}}}{\sequence{\nat}}\\
\\
\eraseL{\expr} & = & \eraseE{\expr}\\
\eraseL{\base} & = & \eraseL{\base}\\
\eraseL{\lam{\sequence{\var}}{\expr}} & = & \lam{\sequence{\var}}{\eraseE{\expr}}\\
\\
\eraseI{\nat} & = & \nat\\
\eraseI{\idxplus{\idx}{\altidx}} & = & \app{\tt +}{\eraseI{\idx}\;\eraseI{\altidx}}\\
\eraseI{\idxshape{\;\sequence{\idx}}} & = & \app{\tt *}{\sequence{\eraseI{\idx}}}\\
\eraseI{\var} & = & \mangle{\var}\\
\\
\eraseA{\expr} & = & \mrrep{\expr}{\argframe{\expr}}{\expansion{\expr}}\\
\\
\end{array}
\]

\end_inset


\end_layout

\begin_layout Standard
At several points, the translation must consult the (implicit) frame annotation
 on an expression.
 The list of shapes 
\begin_inset Formula $\sequence{\idx}$
\end_inset

 in the annotation becomes an expression which computes the product of 
\begin_inset Formula ${\sequence{\eraseI{\idx}}}$
\end_inset

.
 The possibility of arrays of functions appearing in function position slightly
 complicates the translation into an explicit map.
 With possibly no single function to map over the argument arrays, we defunction
alize the application by generating an 
\family typewriter
apply
\family default
 function to map instead.
\end_layout

\begin_layout Standard
Some translation cases generate multiple AST nodes, such as the
\family typewriter
 
\begin_inset Formula ${\tt {MAP}}$
\end_inset


\family default
 and 
\begin_inset Formula $\lambda$
\end_inset

 produced from defunctionalizing an application form.
 While the 
\begin_inset Formula ${\tt {MAP}}$
\end_inset

 has the same type as the source term, the 
\begin_inset Formula $\lambda$
\end_inset

 has a function type generated from 
\begin_inset Formula $e$
\end_inset

's type.
 An index translated into an expression is typed as 
\family typewriter
Int
\family default
.
\end_layout

\begin_layout Section
Closure Conversion
\end_layout

\begin_layout Standard
The explicit map/replicate must then be transformed so that every 
\family typewriter
Lam
\family default
 form is replaced with an explicit closure which contains a copy of the
 environment and a reference to the function code.
 Though it is possible to represent a closure as an ordinary tuple, this
 compiler uses an added form (and hence a new AST type) to make it clear
 whether an AST has been converted.
 Function-typed AST nodes have their type annotations rewritten to closure
 types due to the different run time representation (a structure rather
 than just a bare code pointer).
 Only 
\family typewriter
Lam
\family default
 forms (which are generated as 
\family typewriter
code
\family default
 fields) in 
\family typewriter
Cls
\family default
 forms will get actual function types.
 The new closure application form should be understood as destructing a
 closure and passing the environment to the function alongside the application
 form's own arguments.
 Next, each 
\family typewriter
Lam
\family default
 form must be replaced with a use of a new top-level definition.
 This leaves the enclosing closure to contain only a pointer to the function
 rather than an actual blob of code.
\end_layout

\begin_layout Section
Remaining Work
\end_layout

\begin_layout Subsection
Partial Evaluation
\end_layout

\begin_layout Standard
The Map/Replicate translation tends to introduce needless computation, such
 as defunctionalizing the application of a scalar array and replicating
 with an expansion of 
\begin_inset Formula $\app{\tt *}{1\;1}$
\end_inset

.
\end_layout

\begin_layout Subsection
Replication Rewriting
\end_layout

\begin_layout Standard
The 
\family typewriter
Rep
\family default
 form is convenient but expressible using 
\family typewriter
Map
\family default
.
 Loop fusion later will likely be simpler with one less iterative form to
 deal with.
\end_layout

\begin_layout Subsection
Inlining
\end_layout

\begin_layout Subsection
Fusion
\end_layout

\begin_layout Subsection
A-Normalization
\end_layout

\begin_layout Subsection
Primitive Operations
\end_layout

\begin_layout Itemize
arithmetic
\end_layout

\begin_deeper
\begin_layout Itemize
integer and float versions
\end_layout

\begin_layout Itemize
coercion
\end_layout

\begin_layout Itemize
RNG?
\end_layout

\end_deeper
\begin_layout Itemize
logic, selection
\end_layout

\begin_layout Itemize
list-like things
\end_layout

\begin_deeper
\begin_layout Itemize
head, tail, behead, curtail
\end_layout

\begin_layout Itemize
take, drop, take-right, drop-right
\end_layout

\begin_layout Itemize
reverse
\end_layout

\begin_layout Itemize
rotate
\end_layout

\begin_layout Itemize
append
\end_layout

\end_deeper
\begin_layout Itemize
shape manipulation
\end_layout

\begin_deeper
\begin_layout Itemize
reshape, itemize, ravel
\end_layout

\begin_layout Itemize
transpose
\end_layout

\begin_layout Itemize
shape-of, length
\end_layout

\end_deeper
\begin_layout Itemize
other iteration patterns
\end_layout

\begin_deeper
\begin_layout Itemize
left/right fold
\end_layout

\begin_layout Itemize
associative reduce/scan
\end_layout

\begin_layout Itemize
filter
\end_layout

\begin_layout Itemize
iota
\end_layout

\end_deeper
\begin_layout Itemize
I/O
\end_layout

\begin_layout Subsection
LLVM Code Generation
\end_layout

\end_body
\end_document