Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

PHI 14 - Compiler #16

Draft
wants to merge 40 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
6e676ed
first intro for compiler design
coned Jan 21, 2022
9a053ba
Expand high-level explanation for compiler
mirryi Jan 23, 2022
3f19d9f
chore: create folder
hilbert-yaa Jan 30, 2022
1916f31
docs: update annotated bib
hilbert-yaa Jan 30, 2022
9ad15d4
chore: trim directory
hilbert-yaa Feb 4, 2022
18a629a
feat: add notes on grift and its paper
hilbert-yaa Feb 4, 2022
008e9b6
chore: trim directory
hilbert-yaa Feb 21, 2022
8e93c14
docs: add annotated bib on herman's coercion paper
hilbert-yaa Feb 21, 2022
a463bef
docs: add embed_interpreter paper notes
hilbert-yaa Mar 22, 2022
2d7b3fd
Update pipeline diagram to match architecture changes
mirryi Mar 31, 2022
318e891
Remove empty_hole.md
mirryi Mar 31, 2022
105a6e1
Add hole contexts example and diagrams
mirryi Mar 31, 2022
b87c0e7
Update document to match current implemenation choices
mirryi Mar 31, 2022
6c30409
Update for recent architecture changes
mirryi May 19, 2022
8f1af8d
Remove hole-contexts.dot
mirryi Sep 24, 2022
a7608fe
Reorganize gradual typing paper notes
mirryi Sep 24, 2022
a36f065
Add framework for LaTeX based PHI document
mirryi Sep 24, 2022
75b30aa
Add motivation section
mirryi Sep 24, 2022
dabcbc2
Add references from paper/poster/slides
mirryi Sep 24, 2022
926e575
Add approach section discussing approaches towards holes
mirryi Sep 24, 2022
d4890b7
Add formalization section stub
mirryi Sep 24, 2022
fc903d6
Add implementation section stub
mirryi Sep 24, 2022
e3d8860
Add make targets to build pdfs
mirryi Sep 24, 2022
b702f18
Add more control flow analysis referenes
mirryi Sep 24, 2022
cb612cb
Start adding formalization for lower IR
mirryi Sep 24, 2022
e18457e
Add more syntax and rules to LIR formalization
mirryi Sep 26, 2022
845ae1c
Continue working on formalism for LIR
mirryi Sep 30, 2022
9605ef5
Use report class to have more heading numbers available
mirryi Sep 30, 2022
34392f5
Make figure/table numbering to be per-chapter
mirryi Sep 30, 2022
edb621e
Add functions to LIR syntax
mirryi Sep 30, 2022
df9e548
Add some gotchas and warnings
mirryi Sep 30, 2022
25f04ef
Add type assignment rules for LIR application
mirryi Oct 3, 2022
1df87ab
Clean up LIR TA rules with two immediates
mirryi Oct 3, 2022
431dac5
Remove old md file
mirryi Oct 5, 2022
98c86a1
Various cleanup + add coercion calculus section stub
mirryi Oct 5, 2022
b828f79
Add syntax for coercion language
mirryi Oct 5, 2022
2ce8bc1
Clean up LIR syntax command names
mirryi Oct 5, 2022
0a067c0
Start to define coercion language and typing
mirryi Oct 5, 2022
ff4ac82
Add cast conversion rules for coercion language
mirryi Oct 6, 2022
23febf2
Begin to formalize dynamics of coercions
mirryi Oct 9, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions 14-compiler/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
*.pdf
target/
47 changes: 47 additions & 0 deletions 14-compiler/01-motivation.tex
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
\documentclass[index.tex]{subfiles}

\begin{document}
\section{Motivation}
\label{motivation}
Right now, \Hazel{} has a simple tree-walk evaluator based on environments, but not a compiler that
can output fast, optimized executables. This PHI proposes such a compiler.

\subsection{Objectives}
\label{objectives}
There are a number of criteria we would like the compiler to satisfy:
%
\begin{itemize}
\item Compiled programs should match the semantics and output of the existing evaluator. This
means the compiler should
%
\begin{itemize}
\item support the incomplete programs, i.e. programs with holes.
\item produce programs that have the same final result as an evaluated program.
\end{itemize}

\item Compiled programs should have faster execution speed than evaluated ones.
\item Complete \Hazel{} programs should execute as normal functional programs; they should require
no extra machinery related to holes.
\end{itemize}
%
In addition, it may be interesting to explore interoperability with the evaluator and live
programming environment:
%
\begin{itemize}
\item Dynamic compilation with hand-off between evaluator and compiler.
\item Incremental compilation, to reduce overhead of compilation in a live environment.
\item Incremental execution, via fill-and-resume-like behaviour.
\end{itemize}

\subsection{Challenges}
\label{challenges}
The presence of holes poses fundamental challenges for compilers, as \emph{indeterminate results}
produced by \Hazel's semantics are not values. Hence, we are concerned with
%
\begin{itemize}
\item Speed- and space-efficient representations for holes and indeterminate results, as well as
performant operations on them.
\item Static analyses for optimizing incomplete programs.
\item Incrementality and liveness; see above \cref{objectives}.
\end{itemize}
\end{document}
81 changes: 81 additions & 0 deletions 14-compiler/02-approach.tex
Original file line number Diff line number Diff line change
@@ -0,0 +1,81 @@
\documentclass[index.tex]{subfiles}

\begin{document}
\section{Approach}
\label{sec:approach}
This section outlines the approaches we take towards various aspects of compilation and execution
related to holes.

\subsection{Runtime representation}
\label{sec:runtime-representation}
We represent indeterminate results as syntax trees in the runtime, and operations taking
indeterminate results merely accumulate a new syntax tree.
%
\begin{example}
In the program $1 + (5 * 6 + \SyEHole{1}{})$, $5 * 6$ produces an ordinary number $30$, but the
subsequent $+ \SyEHole{1}{}$ gives an indeterminate syntax tree with root $+$, left child $30$, and
right child $\SyEHole{1}{}$. The final result is an indeterminate syntax tree with root $+$, left
child $1$, and right child that is the previous tree.
\end{example}
%
\noindent This necessitates dynamics checks before each operation to determine whether operands are
values or indeterminate results; therefore, there must be some runtime data that discriminates
between values and indeterminate results.

\subsection{Casting}
\label{sec:casting}

\subsubsection{Embedding/projection}
In a first pass, we adopt a type-indexed embedding/projecting pairs approach \cite{benton2005,
new2018}: casting $x$ from type $\tau$ to the hole type \emph{embeds} $x$ with type information
about $\tau$ into a proxy; casting to the type $\tau'$ \emph{projects} the proxy, dynamically
checking if $\tau = \tau'$.

\subsubsection{Coercions}
In the future, a coercion-based approach should be taken, which has some space efficiency guarantees
\cite{herman2010, kuhlenschmidt2019}. A ``coercion calculus with holes'' is probably a whole
research topic in itself.

\subsubsection{Static analysis}
It might be possible, as with determining if expressions are possibly indeterminate at runtime
(\Cref{sec:completeness-analysis}), to statically determine where casts might show up. This might
lend itself to some optimizations, particularly when casts appear as scrutinees of pattern matching
(\Cref{sec:pattern-matching}).

\subsection{Pattern matching}
\label{sec:pattern-matching}
It should be possible to compile pattern matching with holes into ordinary functional pattern
matching:
\begin{itemize}
\item \emph{Hole patterns} may be compiled into wildcard patterns that immediately stop and return
the entire $\textsf{match}$ expression as an indeterminate results.
\item In the presence of casts, types must be matched on as data. This is something to consider
when designing the runtime representation of indeterminate results
(\Cref{sec:runtime-representation}).
\end{itemize}

\subsection{Completeness analysis}
\label{sec:completeness-analysis}
Since we want complete portions (i.e. no holes) of a program to run as ordinary functional programs
and not require the machinery necessary for handling holes, we perform a static \emph{completeness
analysis} that determines whether an expressions is guaranteed to be hole-free. To do this, we
define a notion of \emph{completeness}:
%
\begin{definition}[name=Completeness, label=completeness]
An expression may be (1) \emph{necessarily complete}, i.e. it must be a value at runtime; (2)
\emph{necessarily incomplete}, i.e. it must be an indeterminate result at runtime; or (3)
\emph{indeterminately incomplete}, i.e. it may be either a value or an indeterminate result at
runtime.
\end{definition}

\subsubsection{Function-local completeness}
A basic function-local analysis which treats function parameters as indeterminately
incomplete by default may be implemented in a single pass over the expression tree. See
\Cref{fig:lir-completeness-analysis-local} for the formalization.

\subsubsection{CFA-based completeness}
A more complex analysis may use control-flow analysis techniques on higher-order functions
\cite{shivers1991, nielson1999}. Other papers to consider reading: \textcite{vardoulaskis2011} (but
apparently $2^{n}$ complexity), \textcite{gilray2016}.

\end{document}
10 changes: 10 additions & 0 deletions 14-compiler/03-01-middle-ir.tex
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
\documentclass[index.tex]{subfiles}

\begin{document}
\subsection{Middle intermediate representation (MIR)}
\label{sec:mir}

\subsection{Sequentialization}
\label{sec:sequentialization}

\end{document}
Loading