Ch. 4 introduction

[JacquesCarette]

This is based on commit 2a1878f

• "we concluded that metaprogramming is an inescapable road on the journey toward first-class modules in DTLs". 'inescapable' is just plain wrong. metaprogramming is a reasonable road to take to explore the ideas involved.
• "As such, we begin by forming an ‘editor extension’ to Agda with an eye toward the minimal number of ‘meta-primitives’ for forming combinators on modules." This sounds fantastic! Too bad the chapter does not deliver on the "eye towards the minimal number of 'meta-primitives'. Of course, 'minimal' is dangerous, as that would require some kind of proof. But let's assume 'small' instead. So what do I expect to read?
  • an overview of the tasks that are in scope for these combinators (example-driven would be great)
  • an analysis of what the tasks actually involve (again example-driven)
  • a synthesis of the features needed to perform these tasks
  • a presentation of that small set of meta-features So chapter 4 has to go hand-in-hand with chapter 3, which is supposed to do some of the above (but does not, at least not yet)
• "The purpose of writing the editor extension is to show that the ‘flattening’ of value terms and module terms is not only feasible, but practical" This was essentially already known, via the MathScheme prototype. But the prototype at hand actually does quite a bit more. Unfortunately, because the 'story' is not systematic (see the previous point), that the prototype actually delivers quite a bit more is buried.

[alhassy]

1. Reasonable is a reasonable phrasing ;-)

2. Small does seem more reasonable.

   • Did section 4.3 not deliver on an example-driven approach? Perhaps I should insert a forward reference to that section.
   • The discussion on meta-features, meta-primitives, is indeed missing.

3. I'll try to rephrase that sentence and insert references.

Thanks!

[alhassy]

This seems obsolete - closing.

[JacquesCarette]

It only 'seems' obsolete if you read the first bullet, which is about a particular sentence, which may well have disappeared.

The next 2 bullets are about having some specific, actual content be present in your thesis. You should not close this until you have told me where this content actually is.

[alhassy]

The chapter's title page is the place to look, in the most recent commit.

If need be, we can make new issues with the time constraints kept in mind.