Comments on Hazel prototype, somewhat "organized"

Hazel_prototype_comments.md

2018.03.05

Nested contexts

2018-3-5-screenshot

Nested contexts (e.g., nested lets) give rise to nested hole contexts. The current Hazel interface displays paths through this nested structure, with clickable links, which is very cool.

This makes we wonder: Rather than show the structure one piece at a time, from the vantage point of a single hole, is there a way to show the entire nested structure, and then simply "highlight" the parts shown now in the lower right-hand corner? Likewise, I think this could lead to ideas for rendering these structures in papers, talks, etc.

E.g., It'd be cool to see a structure that's similar to (isomorphic to) the nested let expressions themselves.

Example

Here's a smaller version of the same program pattern:

let b1 = 
  let a1 = _1
  let a2 = _2
  _3
let b2 =
  let c1 = _4
  let c2 = _5
  _6
_7

Incomplete hole-context structure

The context for hole _7 consists of variables b1 and b2, whose values are holes _3 and _6, respectively. The context for each of these holes consists of a pairs of variables, and so on.

The program's structure follows that of a binary tree, and this "incomplete superstructure" of holes and contexts mirrors that binary tree structure.

My suggestion is that we render this superstructure in the Hazel interface, and then project each "path" shown now onto this structure as a highlighted sub-structure. In particular, each path consists of holes and variables, linking the "root" hole _7 with the hole in question, by following a path through the following AST (notice that it looks the same as the program listing above):

b1 = {
  a1 = _1
  a2 = _2
  _3
}
b2 = {
  c1 = _4
  c2 = _5
  _6
}
_7

A few more thoughts:

1. Observe that in this case, the program is largely incomplete, so this "incomplete superstructure" is similar in size to the entire program.

2. However, in programs that are mostly complete, this incomplete superstructure would be a small fraction of the entire program; it would be the "incomplete backwards slice" of the program's output, or something like that.

Example 2

Now, suppose we fill in the first few holes:

let b1 = 
  let a1 = 11
  let a2 = 22
  33 * (a1 + a2)
let b2 =
  let c1 = _4
  let c2 = _5
  _6
_7

The incomplete hole-context structure gets smaller:

b1 = 1089
b2 = {
  c1 = _4
  c2 = _5
  _6
}
_7

2018.03.04

Summary:

Really nice improvements to the design, layout and styling of Hazel!

Overall, it's starting to look like something that students in an intro FP class could really use to do some of their work.

I played around editing small programs, and also found that experience has improved too. More details below.

Feature ideas

1. incomplete programs often use hole types, and hole-typed lambda terms often lead to resutls with casts, which may be distracting for students that are new both to functional programming, and the basic (non-cast-based) operational semantics of the lambda calculus. To make Hazel easier to explain to such students, we could have an option to "summarize" casts in results, as some kind of styled box shape, but without the full type information. Then, students can inspect/unfold that box to get the full cast info shown now.

Some questions that came up while I was playing with it:

1. λ terms: unannotated variables versus annotated (in results)? As a user I wonder: How many forms of lambda terms are there? How do they arise?...

2. ...After peeking at Semantics.v a bit, I see that there are "static" hole expressions for editing ("unassociated" HExps), and dynamic hole expressions, and that the AST structure is quite different between these forms (beyond associated ops versus unassociated ops). As a user, I don't notice the difference, except for the types on variables bound by lambda.

Pedantic technical comments

1. I was able to edit an incomplete Hazel program to introduce and then remove each form of expression (even paren!)...
2. ...However, some forms introduce extra parens when inserted (depending on the context), and require removing the parens separately. So one insert requires two deletes, and some navigation. This seems okay to me, but was noteworthy as a user.

For instance, suppose my cursor is on a hole within an operation sequence, and I insert a new let binding. Doing so will insert parens around the let (which is good), and the let and parens each require separate removal steps (which also seems fine).

_*>_<*_

_*(let x = >_<  _ )*_

Now delete let by placing cursor on, e.g., =
Now delete remaining parens enclosing the hole

Again, I don't see that this behavior is "bad", it's just a noticeable assymmetry, but may also be a natural one.