How should we curate edit histories in Hazel so that we can make sense of them, and find patterns and structure in them?
Let's step back and consider related systems like Cog and Agda (both provide interactive editor services for functional programs, though these have depedent types, unlike Hazel; let's ignore dependent types). Though all of these systems have similar interaction models, Agda's way of doing things is very different from Coq, and both should be different than Hazel:
In Agda, you use emacs and Agda's interactive services to write a functional program, and all of the "commands" that the programmer performs along the way imperatively change the edit state of that functional program, but are otherwise lost (not saved in final Agda file). In Hazel (or emacs), these edit commands could be saved somewhere, as an action list. In either case, if we look at this action list, it's not really very meaningful on its own. (Inspecting it is like looking at a bash history, and trying to recall what one was doing and why).
In Coq, one does the reverse: One writes some imperative stuff, that interactively changes the proof state (which one sees in emacs as one does this), but when one is finished, what they've left as an artifact is an imperative script. Behind the scenes, Coq saves the (typically unreadable) proof term, which is not meant to be understood directly by the programmmer.
In Hazel we want both artifacts (a piece of software, and the fine-grained, editor-level history of its construction/maintenance) to be constructed interactively, as they both are in the systems above.
But, unlike those systems above, we want to save both artifacts in a form that is human-understandable, or at least as the potential to be. (Of course, both should also be meaningful formally/mechanically, too).
I can imagine doing this in phases, which resemble what I do today (or often want to do today):
- I edit my program (e.g., using emacs)
- I look at the history of what I just did (e.g.,
git diff) - If I have the time and energy, I use git to reorganize those edits into ones that are more meaningful, and give each a commit message.
What I want to do, is in steps 2 and 3, reorganize the edits into larger ones (even just "lists" or "trees" of primitive actions) and then name these groupings and sequences. I may even annotate certain edits as being commutative, and I may want to verify (by testing) that this is true.
The point of this activity is to curate the edits in a way that will make sense when someone looks at the equivalent of the git commit history.
The additional benefit of this activity is that we may start to see patterns in what we do to programs, and to create abstractions for refactorings (e.g., renaming stuff, inlining/outlining functions, changing the signature of a function in a module interface to an isomorphic one, and refactoring all uses systematically, etc.).
Then, those abstractions can go into the edit history, including their fine-grained trace structure (a list of primitive edit actions).
Also, by viewing the edit history as a structure in Hazel, we can include lots and lots of information (e.g., many levels of abstraction, from high-level traces of compound edits, to low-level traces of primitive actions), and just project out what we want, when we want to inspect it.
"The more we can do that by reflecting the tech on itself the bettter."
--Ian
The curation process described above may seem straightforward, but it gives rise to a series of important questions.
One strange property of the curation process above is that, without some care, the system may loose track of the "levels" of the edits: The edits in curation step 3 occur to a term, which themselves represent edits on a (distinct) term, from curation step 1.
This gives rise to an inductive notion "edit levels":
- Hazel Terms
- Terms that represent Edits to Terms at 1.
- Terms that represent Edits to Terms at 2, or 1.
- ...
This stratififcation also begs the question: What's the equivalent of Escher's "drawing hands", and is that in any way "well-formed"? (Also, what does "well-formed" mean? Some ability to trace and replay, perhaps?).
If such circular patterns are meaningless, than what enforcement mechanism in Hazel rejects them?