4.1 Why textual transformations? III

[JacquesCarette]

This is based on commit 2a1878f

Given that #33 advocates for removal of the content before "Thus, rather than work with abstract...", the "Thus" becomes pointless.

On the other hand the 'design decision' to rewrite "phrases" from an extended syntax does need to be commented on. "legitimate existing syntax" can be deleted, as "Agda syntax" already contains that information.

There are alternatives to phrases. One could have considered annotations, for example. I'm sure there are other possibilities.

I am quite sure that the choice in the prototype was quite pragmatic. Your job is to convince your reader of that too.

[alhassy]

I'm still not sure about deleting the preceding content; we can continue to discuss it at #33.

The rewriting could be elaborated on. The concluding clause, "legitimate existing syntax", is to emphasies that we are not altering existing Agda, and is used to avoid having the phrase "Agda syntax" repeated in such a close proximity.

"Annotations" would be inaccurate, since PackageFormer does not generally annotate existing Agda code, but instead serves to produce new Agda code. As such, the generic, albeit vague, term "phrases" was used. I'm open to other terms.

The purpose of that collection of paragraphs was to justify why textual rewriting was the way to go. It seems however that I did not communicate that sufficiently well; I'll rewrite that section.

Thanks for pointing out an opportunity for improvement!

[JacquesCarette]

I think #33 addresses things fine now.

Again "purpose of..." is great - you know what you're trying to convey. And I agree that that message is topical. The question is, how to do so?

My point about annotations is not to say you should have done it that way, but that it seems to me that part of a justification of doing X using method Y is to first look at the array of available methods (showing that you do know the domain and the choices), give pros and cons of these methods wrt to solving X [this usually entails giving more details about what 'solving X' really means], which naturally arrive at one method (here: text rewriting) as a good one to use for the purposes of the prototype.

I suggest that, rather than rewriting that section, you first put here an outline of your intended rewrite. I can then ask questions based on the outline, instead of the longer turn-around (and time use) of commenting on fully written text.

You can also write some meta comments meant for me/Wolfram: The purpose of this subsection is to explain Z. Then we can help you when there is a disconnect between Z and the longer form of what you wrote.

[alhassy]

The idea of terse meta-comments designating aims of a section is brilliant!!

I thought the paragraphs Why an editor extension, above Why textual transformations, discussed, albeit briefly, possible routes. Perhaps I should back reference to that earlier heading, or bring the two a bit closer.

I like the idea of outlining before major writing, and I do believe that Why an editor extension, somewhat, meets the specification you've outlined above; still, below is an outline for a possible rewrite of some the section on textual transformation.

Let me know what you think!! xD

---

Why Textual transformations?

• How do we extend a programming language?

1. By changing the compiler and existing concrete syntax.

   • Pros: [P1] Can make nearly any desired addition in a smooth fashion.

   • Cons: [C1] Can be non-trivial and costly to do so; [C2] may ‘break’ other features of the language; [C3] may not be backward compatible; [C4] may be difficult to use, requiring a new compiler toolchain; [C5] may splinter-off and not be useful for problems in existing code, which the extension was made to solve.

     ( Sweet.js is such an effort to add AST/syntactic macros to JS. )

   ∴ There are too many cons to follow this route; let's look for another route.

2. Using the language's language-extensibility features.

   • Pros: [P2] In-language architecture; easy to distribute, and maintain; [P3] can be provided as a library and so allows plug-and-play access.

   • Cons: [C6] Most languages only allow a primitive textual substitution extensibility in the style of C-macros; [C7] weak macro mechanisms could lead to difficult to manage code, both at the definition site and at the usage site ---e.g., a weak macro system might differentiate between built-in and user-defined elements (something that Lisp does not do).

   • Aside/tangent:

     ( For me, a “strong macro system” allows the introduction of at least new binding constructs, such as exception handling and control flow that can explicitly manage the order and number of evaluation of its elements, and fresh variable names; and as such, can introduce new concrete syntax; i.e., embed DSLs naturally. Sometimes a language can achieve this by careful organisation of higher-order features (along with laziness, keyword arguments, and variable-length args, or Python Decorator annotations); eg allowing flexible λ's (such as Ruby's “do…end”) to simulate new binders or using a nice concrete syntax for hashmaps (as in Python or JS) to simulate them, as well as objects, keyword arguments, and case/switch statements. Agda's mixture of the syntax keyword along with mixfix names allow a lot to be accomplished ---perhaps ‘common-enough’ tasks and in a typed fashion; that is pretty neat.

     The most crucial characterising factor of strong macro systems would be their ability to introduce, or act as, top-level-items in a language: For example, Lisp's standard function-definition mechanism is actually a macro; as are it's type declaration mechanisms.

     Agda, unfortunately, cannot achieve this goal. If it could, PackageFormer would have been written in Agda. In a sense, PackageFormer is an attempt to tack-on to Agda the ability to experiment with top-level package declarations. ( This is somewhat in alignment with the Ometa project (p21): Providing language support for what-if scenarios, or many-worlds semantics. )

     Finally, I would consider a strong macro system to be one that allows the creation of macros-that-create-macros. E.g., in Agda, for each 𝓃, we can create a mixfix function if𝓃_,…,_then_,…,_else_,…,_ : ∀{A : Set} (c₀ c₁ … cₙ : 𝔹) (t e₀ e₁ … eₙ : A) → A that simulates 𝓃-way-branching conditionals; e.g., if3 c₀ , c₁ , c₂ then t else e₀ , e₁ , e₂ which yields eᵢ if ¬ (c₀ ∧ ⋯ ∧ cᵢ), and otherwise t. (This is a variation on McCarthy's Conditional.) However, the number of underscores depends on 𝓃 and so we are creating syntax that depends on a value, which is sometimes doable in Agda but not always and not easily; e.g., one can mimic Haskell list-syntax [x₀, …, xₙ] in Agda, but it is too brittle to work with, say, products in scope. Also, Agda's macro mechanism requires the syntax unquoteDecl new-name = macro-call and so even if we define an if𝓃 macro in Agda, we must unquoteDecl each instance, rather than, say, have if0, if1, ..., if9 be generated for us ---this is not possible since we cannot produce names in Agda, last I checked--- and so the alternative is to pass vectors to a function rather than have a pleasant (variable-value-dependent) syntax. Btw, even without the comma-syntax, just if𝓃 c₀ c₁ … cₙ t e₀ e₁ … eₙ application style may be doable with Agda macros but suffers the same unquoteDecl concern and so grows linearly with 𝓃.

     Yeah, you probably know all of this but I like metaprogramming and you're partially to blame ;-)

     Slightly related: Guy Steele has a super neato talk, “on growing a language”. )

   Agda, in particular, essentially only allows C-style macros but with the additional constraint that all code-fragments must be well-defined, and so the result is a weaker (albeit safer) extensibility system.

   ∴ Let's look for another route.

3. By augmenting the coding/input environment to produce auxiliary files in addition to the user-created files ---the extra files are due to comments of the existing syntax that contain new preprocessor syntax.

   • Pros: [P3] The extra preprocessing is silently handled in the background; [P4] since new files are created, one can use the resulting files without having the preprocessor and as such can use it for one-off scenarios.

   • Cons: [C8] There is an additional syntax to learn, as is the case with all the other approaches, and so not a real con; [C9] you need to have the extra plugin, this is akin to having a lightweight altered compiler; [C10] one would need to perform such environment integration at least for a number of the most popular coding environments, for the resulting preprocessing tool to be useful to a large portion of the community.

   Since C10 is hardly a concern for the Agda community and C8 is applicable across the board for possible approaches, this option has the least number of cons and so is a promising route to pursue. ( Aristotle: “Man is a rational animal”; Heinlein: “Man is a rationalising animal”. )

   ∴ Editor extensions ftw

[JacquesCarette]

I'm going to have to insert reviewing this in my 'to do' list, I can't give it the attention it deserves right now.

[JacquesCarette]

Using the same numbering for commenting. Note that you should not be exploring the options 'sequentially' (your explanation above has these "∴ Let's look for another route." which only make sense if things are understood that way.

1. • P1 good
   • C1 good, C2-C5 less so. C2 is not a con unless you count "the programmer is not good enough to do it properly" as a con; incompetence is not a con! C3 is trickier, but is close in spirit to C2: if you can't make it backwards compatible, it's not really an 'extension' at all, it is a language change. So I don't C3 counts either. I don't believe C4, again for the same competence argument. C5 is kind of real, but you're assuming it's done in a branch [think of the hundreds of GHC extensions]. Your cons are under-justified and feel like post-facto justifications. You can do better!

2. If the language has its own extensibility features, and you use them to extend things, you're not really extending the programming language, you're using the language as it is meant to be used. Also, what 'most' languages do/do not provide is not relevant at all, because here you only care about one language: Agda. [I won't comment on the aside as it is irrelevant.] So you should look in real detail at Agda's extension facilities here.

3. This is really "by meta-programming". Here, you should investigate different kinds of meta-programming. For example, you could use an external too to do macros. Or you can extend the de-facto IDE. Second, your analysis for point 1 was more careful, by here you were getting a little too discursive. This should feel like a proper analysis.

Fundamentally what you're missing is a higher-level explanation that fits your full thesis. Why? Because, later on, you switch from editor extensions to in-Agda extensions! You have to justify that too!

In my mind, the proper justification goes through the route:

• we needed to explore a lot of thing, do a lot of experimenting
• we weren't sure quite where we'd end up, we needed to discover, through real experiments, what was really needed ==> build a prototype!
• a prototype has very different requirements than an integrated solution
• for example, a non-prototype solution would have as many parts coded (and verified) in Agda as possible
• not knowing where this is all going, lots of types and not having access to all parts of the language is quite limiting.
• (etc)

It doesn't have to be exactly like that, but close. In my mind, this section isn't "Why textual transformation" or "Why editor extension" but rather "First: an prototype for exploration". The rest, to me, flows smoothly from that.

[alhassy]

I've only briefly browsed your feedback ---I'll need to come back to it.

Your final remark, First: an prototype for exploration, has made its way at the start of 4.1 in the margins :: https://alhassy.github.io/next-700-module-systems/thesis_new.pdf

At the moment, I suspect this discussion thread's end results will lie at the start of a section on reflection in Agda.

[alhassy]

Stale ;; good ideas for another life ---closing.