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.
This will serve as my checklist of revisions. It also has screenshots of comments I don't understand or would like more context, with each comment I would like clarity on circled in green ink.
Most important:
Abstract:
[x] solved -> addressed
[x] remove "via compilation to a decision tree"
[x] Fix "To resolve these problems" -> compromise!
[x] "contains all the extensions to pm" -> "contains them"
[x] "with some restrictions." -- are these enumerated? characterize them!
[x] Fix "subsumes" to match thesis in pres
[x] change order of "certain computations can only be expressed verbosely using pattern matching primitives" Question: is this ^ the correct interpretation of your copy editing marks?
Questions appear below.
What does "N" mean?
Why did you circle "good"?
How would you recommend fixing this flow? The rest of the flow comments are understandable to me, this one I'm having a hard time with.
Introduction
[x] Line 22: fix order of citations
[x] Line 42: Extensions are subject... designer, not ubiquitous.
[x] rm "across various frontiers"
[x] 46: rm "to pattern matching"
[x] rm "to succinctly solve the problems programmers face."
[ ] 528: create single points of truth. Reference Nice Prop. Rm And by... performance.
[ ] 538: emph "all" the extensions. rm words after extensions.
[ ] rm "Indeed,"
[ ] Fix n.d. in citation list
[ ] Section 2 as 2 sections: pattern matching, and verse
[ ] 555 s/paper/thesis
[ ] Equations present...relate to pattern matching: discussion, if at all.
[ ] Also change "I will" to I inside that paragraph.
[ ] 568: VC's equations test for structural...
[ ] 571: hyphen, not dash after "left"
[ ] 584: Every equation in Verse... : mention e1 = e2. Full verse e1 = e2, VC x = e. This matters, especially for substitution.
[ ] ...unbound names in e to values: cite Robinson?
[ ] FIX TRAPEZOID AREA
[ ] 592: An equation offers a form...
[ ] ...complex to cover here, but choice...
[ ] choice look like in Verse (Figure TODO). Remove fig reference later in sentence
[ ] 602: Paragraph break. Then, s/Like/As: As in the pattern...
[ ] Before you go here (602), Walk your Reader Through The code :
lambda Means, one means, exists means ... and is followed by, ...
Next, how is it evaluated.
THEN ANALYSIS and Comparison
[ ] 608: s/observers/observer functions
[ ] "looks like the algebraic laws" : dubious. Show side by side like in talk, let reader decide.
[ ] "relies more on mathematical notation" : nr does not understand
[ ] "though it doesn't... mathematician would" : WEAK
[ ] does not duplicate {rm} any code.
[ ] as easily as {rm} pattern matching.
[ ] internal values named {rm} explicitly.
[ ] "a compiler cannot help" : untrue
[ ] 631: {rm} You understand...
[ ] 632: prefer equations to observer functions
[ ] 640: ambiguous~5th.
[ ] 643: s/strong/{intriguing, or some alternative that doesn't oversell}
[ ] So what's the catch? {rm} In VC, names ...
[ ] 683: search {rm} requires backtracking
[ ] Pattern matching, by contrast, {rm} can be compiled... more than once (cite Maranget)
[ ] A decision tree, however, does not backtrack: once a program
[ ] s/can't test/does not test
Section 3
[ ] Only one language bridges the gap: V-. P+ enables apples/apples comparison. D establishes efficiency of V-. Ergo, rewrite 1st paragraph.
[ ] 701: {rm} \VMinus has equations and choice...
[ ] 701: V-minus paragraph first, before other langs
[ ] 708: why in Appendix?
[ ] Pull unilang table much forward, it's referenced here
[ ] rm "For all intents... together."
[ ] 720: s/Like/As
Generally: s/Like/As with verbs
[ ] 723: s/they are all/all three are
[ ] page: see nr 5/9
[ ] maybe fix period: see nr 5/9
[ ] rm "Creating a type system ... thesis."
[ ] 726: The only form... application.
[ ] rm "in these core langauges"
[ ] 736: is considered a value constructor because it begins...
[ ] 739: To simulate integers, a programmer can use Peano numbers, or they can use value constructors to implement binary numbers.
[ ] are another {rm} option. No footnote.
[ ] 743: s/goes further in analyzing/discusses
Overall: these should go in V-minus intro, because P+ will not exist
Moving on to V-minus...
[ ] 1047: build on top of {rm} an
[ ] 1049: Having stripped out {rm} backtracking and multiple results,
[ ] are left {rm over}.
[ ] Get rid of the table. Show side by side examples, as in talk!
[ ] without a semantics, it makes no sense to present Lemmas. That thing that is labeled a proof is just handwaving. Fortunately, I don't think you need to prove these things. It should be sufficient just to look at the syntax and give your reader an intuition about how V minus differs from verse and therefore does not return multiple results or backtrack. In order to accomplish this, however, you'll need to compare VC with V minus so that your reader can clearly see the differences.
[ ] In syntax and examples: use actual box, U+25AF
[ ] 1104: \VMinus allows for...
[ ] 1110: with (s/the/a) new semantics of choice.
[ ] Fig "the functions in \VMinus"... : COMPARE SIDE BY SIDE; YOU HAVE FROM TALK
[ ] Metavariables of V- : each should start with "A" or "An"
[ ] Add \gs to metavars
[ ] 1168: Fix figure in description of V-minus
[ ] ... possibly-empty sequence of values- rewrite. fail is a syntactic form.
This will serve as my checklist of revisions. It also has screenshots of comments I don't understand or would like more context, with each comment I would like clarity on circled in green ink.
Most important:
Abstract:
What does "N" mean? Why did you circle "good"? How would you recommend fixing this flow? The rest of the flow comments are understandable to me, this one I'm having a hard time with.
Introduction
[x] Line 22: fix order of citations
[x] Line 42: Extensions are subject... designer, not ubiquitous.
[x] rm "across various frontiers"
[x] 46: rm "to pattern matching"
[x] rm "to succinctly solve the problems programmers face."
[x] rm "for such an alternative"
[x] 49: rm "implicitly" & "without pattern matching"
[x] My central contribution in this thesis is to show -> In this thesis I show
[x] 61: rm "In this thesis"
[x] Fix claim of subsumption
[x] 63: "my central contribution" -> "these claims"
[x] 68: "formalized translations from \PPlus to \VMinus and from \VMinus to \D" Add TOC Section 2
[x] I make in \VMinus (Section TODO)
[x] 83: rm "any" before sub-values
[x] 84: "and it binds"
[x] 85: "Before pattern matching was invented, a programmer had to deconstruct data using \it{observers}"
[x] inquire a piece of data’s structure is garden path
[x] But many functional programmers favor pattern matching over observers. I demonstrate with an example and a claim. -> Fix flow
[x] Fix trapezoid area for goodness' sake
[x] 120: "Now compare ... matching (Figure TODO)."
[x] Page 4: instead of expecting the user to remember nice properties from number, give them names or summarize them.
[x] Fix trapezoid area
[ ] 148: Show observer implementation from talk
[x] 151: "In general, pattern matching is preferred over observers for five reasons."
[x] Move "I refer ... over observers" below properties.
[x] Page 4 general: present first, discuss after.
[ ] Property 4 is weak. Fix it.
[x] Property 5: always given names.
[x] 169: Discuss here
[ ] 172: I show... -> Flow.
[ ] Point 1: "The pattern-matching example more..."
[ ] 2: The observers example.
[ ] 185: 1b -> the pm example
[ ] 3: swap good pm and bad observers in compiler discussion
[ ] Point 4 does not hold up. Fix.
[ ] Point 5: 1b -> name
[ ] 196: "compare name1 & name2," "if you prefer pm,"
[ ] em dashes: no space on either side
[ ] 198: Figure 1b -> name
[ ] 200: 1b -> This code
[ ] 201: scrutinee (sh)
[ ] 206: patterns -> branches. Each branch...
[ ] 214: rename 1 and 2
[ ] 217- instances -> cases: both should be the same
[ ] rm "of exactly this"
[ ] "and I demonstrate"
[ ] 222: rm For the same of comparison
[ ] Put "to denote pattern matching without extensions" before "I coin"
[ ] in bare pattern matching, patterns have only two syntactic forms:
[ ] 224: names and applications -> a name or an application
[ ] 224: value constructors -> a value constructor
[ ] In general of this paragraph: flow, and singular.
[ ] 230: NO FUTURE TENSE
[ ] 243: Haskell has only guards, but a Boolean guard )underline is) a side condition. (maybe rm technically)
[ ] Fig exclaimtall: color?
[ ] tall square -> sizeable square EVERYWHERE
[ ] Fix exclaimBigArea
[ ] 266: rm "try to"
[ ] 304: fix em dash spaces
[ ] rm (and hopefully you, the reader)
[ ] Name nice properties
[ ] 317: minimizes
[ ] Paragraph @322: A Little too grim, but the issue is peripheral
[ ] 332: A side condition adds an extra check EM DASH FIX
[ ] (within -> to) a pattern.
[ ] But it can't... addresses it. => too mysterious without an example.
[ ]
[ ] 373: side conditions give that flexibility
[ ] 389: rename Nice properties
[ ] 393: internal values with y and z.
[ ] 395 AND THROUGHOUT: fix future tense.
[ ] 401: =. Each guard has a ..., followed by ...
[ ] 402: rm "At runtime... processes"
[ ] 403: The guard is evaluated by...
[ ] If it does, the next guard is evaluated in an environment that includes the
[ ] 404: processing -> evaluating
[ ] 406: If (it -> the match/the guard) fails
[ ] 426: Pattern guards enable expressions within...
[ ] Whole 426 paragraph: could drop
[ ] 434: token -> location? something
[ ] 434: fun it is, and (add I) need
[ ] 484: Nice properties 2 and 4. rm rest.
[ ] 487: Once again, an extension comes...
[ ] 488: patterns (which -> that)
[ ] 489: Tie I~exploit
[ ] 528: create single points of truth. Reference Nice Prop. Rm And by... performance.
[ ] 538: emph "all" the extensions. rm words after extensions.
[ ] rm "Indeed,"
[ ] Fix n.d. in citation list
[ ] Section 2 as 2 sections: pattern matching, and verse
[ ] 555 s/paper/thesis
[ ] Equations present...relate to pattern matching: discussion, if at all.
[ ] Also change "I will" to I inside that paragraph.
[ ] 568: VC's equations test for structural...
[ ] 571: hyphen, not dash after "left"
[ ] 584: Every equation in Verse... : mention e1 = e2. Full verse e1 = e2, VC x = e. This matters, especially for substitution.
[ ] ...unbound names in e to values: cite Robinson?
[ ] FIX TRAPEZOID AREA
[ ] 592: An equation offers a form...
[ ] ...complex to cover here, but choice...
[ ] choice look like in Verse (Figure TODO). Remove fig reference later in sentence
[ ] 602: Paragraph break. Then, s/Like/As: As in the pattern...
[ ] Before you go here (602), Walk your Reader Through The code : lambda Means, one means, exists means ... and is followed by, ... Next, how is it evaluated. THEN ANALYSIS and Comparison
[ ] 608: s/observers/observer functions
[ ] "looks like the algebraic laws" : dubious. Show side by side like in talk, let reader decide.
[ ] "relies more on mathematical notation" : nr does not understand
[ ] "though it doesn't... mathematician would" : WEAK
[ ] does not duplicate {rm} any code.
[ ] as easily as {rm} pattern matching.
[ ] internal values named {rm} explicitly.
[ ] "a compiler cannot help" : untrue
[ ] 631: {rm} You understand...
[ ] 632: prefer equations to observer functions
[ ] 640: ambiguous~5th.
[ ] 643: s/strong/{intriguing, or some alternative that doesn't oversell}
[ ] So what's the catch? {rm} In VC, names ...
[ ] 683: search {rm} requires backtracking
[ ] Pattern matching, by contrast, {rm} can be compiled... more than once (cite Maranget)
[ ] A decision tree, however, does not backtrack: once a program
[ ] s/can't test/does not test Section 3
[ ] Only one language bridges the gap: V-. P+ enables apples/apples comparison. D establishes efficiency of V-. Ergo, rewrite 1st paragraph.
[ ] 701: {rm} \VMinus has equations and choice...
[ ] 701: V-minus paragraph first, before other langs
[ ] 708: why in Appendix?
[ ] Pull unilang table much forward, it's referenced here
[ ] rm "For all intents... together."
[ ] 720: s/Like/As Generally: s/Like/As with verbs
[ ] 723: s/they are all/all three are
[ ] page: see nr 5/9
[ ] maybe fix period: see nr 5/9
[ ] rm "Creating a type system ... thesis."
[ ] 726: The only form... application.
[ ] rm "in these core langauges"
[ ] 736: is considered a value constructor because it begins...
[ ] 739: To simulate integers, a programmer can use Peano numbers, or they can use value constructors to implement binary numbers.
[ ] are another {rm} option. No footnote.
[ ] 743: s/goes further in analyzing/discusses Overall: these should go in V-minus intro, because P+ will not exist Moving on to V-minus...
[ ] 1047: build on top of {rm} an
[ ] 1049: Having stripped out {rm} backtracking and multiple results,
[ ] are left {rm over}.
[ ] Get rid of the table. Show side by side examples, as in talk!
[ ] without a semantics, it makes no sense to present Lemmas. That thing that is labeled a proof is just handwaving. Fortunately, I don't think you need to prove these things. It should be sufficient just to look at the syntax and give your reader an intuition about how V minus differs from verse and therefore does not return multiple results or backtrack. In order to accomplish this, however, you'll need to compare VC with V minus so that your reader can clearly see the differences.
[ ] In syntax and examples: use actual box, U+25AF
[ ] 1104: \VMinus allows for...
[ ] 1110: with (s/the/a) new semantics of choice.
[ ] Fig "the functions in \VMinus"... : COMPARE SIDE BY SIDE; YOU HAVE FROM TALK
[ ] Metavariables of V- : each should start with "A" or "An"
[ ] Add \gs to metavars
[ ] 1168: Fix figure in description of V-minus
[ ] ... possibly-empty sequence of values- rewrite. fail is a syntactic form.
[ ] result: see nr note 5/9
[ ] but it can (s/produce fail/fail).
[ ] Eval judgement should not be here- later
[ ] empty if-fi always (s/produces fail/fails)
[ ] change discussion of compile time: