Code and proofs for Verse-ML, an equation-style sub-ml language. Part of an undergraduate senior thesis with Norman Ramsey, Milod Kazerounian, and Roger Burtonpatel.
Milod’s comment:
Abstract: Overall good and to the point. I would only alter the final two sentences to make it clear that these are your contributions, rather than facts established by someone else. Consider changing to: "I formalize Verse as V-, a core language that uses Verse’s equations with some restrictions, and show that it can be compiled to a decision tree. I also show that V- subsumes P+, a core language with three popular extensions to pattern matching."
May conflict with Landes's advice on the abstract. Let's discuss.
Resolution: "I propose:"
Talk about “lines 985 to 1025: this page isn't working for me. Let's talk about it tomorrow.”
Not bad to start with problem V- is trying to solve. "Equations in VC look attractive, but..."
s/study/"something of engineering, not science". You have a problem, and are trying to create an artifact to solve it.
Problem: discussing design before presenting the thing. Along with other things, we can put into discussion.
Ending with discussion, rather than conclusion, is an option.
"Your job is to repeat everything in the Verse paper that's important for your reader's understanding."
This isn't the place to compare V- and VC.
The question to answer is: What ideas from VC are stolen for V-?
A: Decisions made by combinations of success/failure and choice, "binding" (values of bound variables are determined) done by symmetric equations
The word for number 2 is "unification."
Both languages restrict choice. V- restricts it more. <- Put in discussion.
NICE PROPERTIES:
For (3); s/user-defined types/constructed data
Nr's notes:
want laws to include arbitrary equations -> "where" in algebraic laws.
what do people want to write? equations and bindings
When talking about implementation of P+, note that side conditions make Nice Property 5 an np-hard problem.
"When you focus on the extensions: less code duplication, laws look more like what you want to write at the board, exhaustiveness analysis is technical but important. Other properties can be split off into another group."
Observers section: example first, properties second.
2 GROUPS: Why better than observers?
And: the code is more like what we're thinking about.
These we'll improve through extensions and wish to preserve in a new proposal.
We want code to look better: laws and duplicate. In order to get that, we compromise exhaustiveness analysis.
V- is comparable to P+: makes the same compromises.
NR claims this is 2 points:
V- is a viable alternative to P+ in terms of code we want to write
V- is a viable alternative to P+ in terms of efficiency
For our meeting tomorrow, it would be good if you had a sample of what
you might say in the paper—and if you like we can work out some of the
details of an approach.
\DTran\ then repeatedly chooses a guarded expression $G$ and attempts the
following:
\begin{enumerate}
\item If there are no guards, insert a \it{match} node with the
right-hand side of $G$.
\item Choose an equation in $G$ of the form $x = e$ s.t. $x$ is not \it{known}
and all names in $e$ are \it{known}.
\item If one is found, generate a \it{let} node, make $x$ known, prune
the \it{if-fi} of all duplicate instances of that $x = e$, and invoke
\DTran\ again.
\item If none is found, choose an equation in $G$ of the form
$x = K \dots$ s.t. $x$ is \it{known}.
\item If one is found, use it to generate a \it{test} node, building
each subtree of the \it{test} by pruning all branches in \it{all}
guarded expressions of the \it{if-fi} in which $x = e$ and $e \neq K
\dots$ and invoking \DTran\ on the remaining ones with a context where
$x$ is known. The algorithm builds the default tree of the \it{test} by
finding it in the \it{if-fi} or assembling one that fails at runtime.
\item If no equation of the form \it{x = K \dots} is found, try to
find a condition $e$ s.t. all names in $e$ are known.
\item If one is found, use it to generate a \it{let}-\it{if-then-else}
pair, pruning each subtree of $e$.
\item If no condition $e$ is found, try to find an equation $x = e$ s.t.
both $x$ and all names in $e$ are \it{known}.
\item If one is found, generate an ifeq/x node and prune subtrees.
I will explain this in our meeting.
\item If none is found, the \it{if-fi} cannot be compiled to a decision
tree. The algorithm halts with an error.
Resolution: "I propose:"
Both languages restrict choice. V- restricts it more. <- Put in discussion.
NICE PROPERTIES:
For (3); s/user-defined types/constructed data
Nr's notes:
When talking about implementation of P+, note that side conditions make Nice Property 5 an np-hard problem.
"When you focus on the extensions: less code duplication, laws look more like what you want to write at the board, exhaustiveness analysis is technical but important. Other properties can be split off into another group."
Observers section: example first, properties second.
2 GROUPS: Why better than observers? And: the code is more like what we're thinking about. These we'll improve through extensions and wish to preserve in a new proposal.
We want code to look better: laws and duplicate. In order to get that, we compromise exhaustiveness analysis. V- is comparable to P+: makes the same compromises.
NR claims this is 2 points:
V- is a viable alternative to P+ in terms of code we want to write
V- is a viable alternative to P+ in terms of efficiency
\DTran\ then repeatedly chooses a guarded expression $G$ and attempts the following:
\begin{enumerate} \item If there are no guards, insert a \it{match} node with the right-hand side of $G$.
\item Choose an equation in $G$ of the form $x = e$ s.t. $x$ is not \it{known} and all names in $e$ are \it{known}.
$x = K \dots$ s.t. $x$ is \it{known}. \item If one is found, use it to generate a \it{test} node, building each subtree of the \it{test} by pruning all branches in \it{all} guarded expressions of the \it{if-fi} in which $x = e$ and $e \neq K \dots$ and invoking \DTran\ on the remaining ones with a context where $x$ is known. The algorithm builds the default tree of the \it{test} by finding it in the \it{if-fi} or assembling one that fails at runtime.
\item If one is found, generate an ifeq/x node and prune subtrees. I will explain this in our meeting.
\end{enumerate}