This will be helpful for testing the new evaluation mode.

We've talked about (and more or less agreed, I think?) how it might be useful to render the selected node's type in an inset window on the canvas, rather than in the sidebar. This would relieve sidebar vertical space pressure, and would make it easy to render types as trees, if the student prefers that rendering. (Currently, in the sidebar, we can only render types as text.)

Once hackworthltd/vonnegut#291 is in, we should be able to port the Alpha Prelude to Vonnegut. As far as I recall, the Alpha Prelude did not include any user-defined types, so I think this work can proceed independently of hackworthltd/primer#112.

We'll certainly want some way to serialize/deserialize programs first, however. It's possible that hackworthltd/vonnegut#320 will be sufficient for that.

Mainly just want to get @hmac's drawing from chat posted someplace permanent.

This is just one idea, but we should probably have a think about how to represent them more usefully than our current { ? } representation.

Assume we want to embed one or more Vonnegut iframes in a web page; e.g., like we do with Repl.it in our Haskell lessons. What do we need in order to facilitate that?

In this scenario, there's no need to save the current state of each iframe if the user quits the browser or closes the window/tab, but a page reload should preserve the current state.

This functionality should not require that the user log in. Each iframe's session should be unique, but anonymous.

Placeholder for now. @annedino4 will work on a few ideas.

Consider the situation

foo :: Bool
foo = ?

bar :: Bool
bar = foo

and you change the type of foo to foo :: Int. This will make bar not typecheck, and (with smart holes) give bar = {? foo ?}. However, this will not be obvious to the user, who is only seeing foo on screen.

We should have a way to

• indicate in the "terms list" that a term is incomplete (e.g. colour it red, or have a red "3" for 3 holes remaining)
• make it clear when (and where) an action has created some (far away) holes

Now that we show the in-scope variables in a dedicated section in the sidebar, we could apply two features we already have elsewhere, in the case when you've selected a hole:

• highlight the variables which are valid fits for the hole
• allow clicking on a variable to insert it into the hole

I think this would be a much nicer flow than having to click "insert a variable" each time.

Following our design principles of "explicit is better than implicit" and "be consistent," I wonder if we should not support Haskell-style function applications (e.g., f a) in text view, and instead render the $ (e.g., f $ a, or even $ f a), just as we do in tree mode. My reasoning:

• It's consistent with tree view.
• It's nice for Haskell because it saves you some typing, but in our structure editor, you need to insert the application node, anyway, even in text view.
• The prefix rendering makes it obvious that you're treating f as an argument to some other operator. My hunch is that this is a major source of confusion for beginning functional programmers.

The only drawback I can think of is that it's not consistent with Haskell syntax, but that's not particularly important.

Here the True and False labels on the case branches are not selectable:

We should visually indicate that restriction to the user somehow.

This is somewhat related to hackworthltd/vonnegut#271 , but if we wanted to support pattern-matching on the "left hand side" in a visual environment like Vonnegut, how could we do that? And if we did, would it be as nice as it is in a text-based language? @annedino4 mentioned in hackworthltd/vonnegut#265 point 6 that she found multiple equations easier to think about at first than case, but that might be because it's what she learned first in our Haskell course; or, perhaps, because the way that we currently render case in tree format is not ideal (again, see hackworthltd/vonnegut#271).

And, if we did support pattern matching, should we allow "deep" matches? Would that get too unmanageable in a visual language?

If we do end up implementing this, it would be interesting to do some A/B testing vs case.

This would be a) consistent with other places in the interface, and b) would allow us to show the student the type of any node in the detail view, and/or in-scope variables.

One potential problem is this: in eval detail mode, we show some static text that describes the reduction sub-steps. These appear in the sidebar but would not change depending on which node is selected, as this is the whole point of the detail view. But this behavior is quite different than any other sidebar content in edit mode, where the contents of the sidebar are completely dynamic.

Showing in-scope variables might also be odd, because it's quite likely that most of them will not be visible in this view, as the detail view purposely cuts out the rest of the tree from the display.

Therefore, I have some UX concerns about this idea. On the other hand, we should probably try it out and see how it feels.

We could potentially address the static vs. dynamic content issue by moving the selected node's type out of the sidebar in all modes; e.g., in a small inset window on top of the canvas. See hackworthltd/vonnegut#688.

https://github.com/hackworthltd/vonnegut/pull/533 makes clear, to me, anyway, that once our trees start getting larger, it's hard to separate expression terms from semantic nodes such as annotations (Ann), function applications (App), type applications (APP), etc. This makes it difficult to scan the tree for familiar terms. For example, when evaluating a map over a list, it's helpful to scan for patterns like x and xs, or syntax like case, but I find this difficult when the tree is a sea of alphabetic labels.

One idea would be to make better use of symbols like @ and $ in the tree. Beginning students won't recognize these symbols or associate them with their semantic concepts, but I don't think that Ann and App and APP are really much better. And if we're consistent with using those symbols @ $ etc. as icons on their respective action buttons, that should help the student establish a correlation over time.

I'd be happy to explore better iconography for these concepts, and we need not be tied to Haskell conventions, but perhaps we should split this effort into 2 pieces: one that's more expedient and solves the immediate problem, and one that's more forward-thinking and takes time to explore better ways to represent these concepts iconically.

There are various behaviours we want to be able to configure globally, for example:

• how we render variable choices when the user chooses "insert a variable" (see hackworthltd/vonnegut#406)
• smart holes (on/off)
• grouped vs split arguments (currently this is per-node, but should probably be global?)

And lots of other things as well, I'm sure. We need a dedicated settings page where the user can toggle these.

It should be relatively easy to add support for name suggestions in the type def UI (e.g., xs and ys for lists).

(Note: @brprice wants to make name suggestions more sophisticated, so that we could use a for a single element of a list of as, and that would be quite a bit more challenging in the form-based UI.)

On the other hand, I'm not certain I want to keep the form-based type def UI (see hackworthltd/vonnegut#646), so maybe it's not worth doing this.

I'm adding this issue now so that we can keep track of it as we get closer to a demo.

Eventually, evaluating touch interactions should be a routine part of our UX approval process for new features and functionality changes, but for now, we've got quite a bit of back-filling to do to ensure that all existing interactions work well in a touch interface.

By "code folding," I mean this:

https://en.wikipedia.org/wiki/Code_folding

We'll want to work out a way to do this for trees.

We previously considered some folding ideas in Viz. There are Figma sketches here:

https://www.figma.com/file/CIZdrV2zzo1jcnltVifDGG/Viz?node-id=21%3A52

(It appears we called it "collapsing" in Viz's trees. That might be a better term, to avoid aliasing with fold operations on trees.)

Currently we render non-empty holes to inert HTML as {? e ?}, when we probably want to do some nice styling of them instead.

As mentioned in issue hackworthltd/vonnegut#265, perhaps there are better ways to rename the definitions.

I have designed 2 testable prototypes below, they work on a browser in both touchscreen and desktop environment.
The keyboard popping up is for the touch screen environments, in the desktop version it will not pop up and the user will type on the psychical keyboard.

** Please rename the definition "a1" to "or" when you are testing the feature.

https://www.figma.com/proto/MFBLOISCCcp9ogJ3CMy2Lw/Rename-definitions---1-1-(Touchscreen)?scaling=min-zoom&node-id=1%3A2

https://www.figma.com/proto/E6HkZDPlWAMtNsoiQOomFk/Rename-definitions--3-(Touchscreen)?node-id=1%3A2&scaling=min-zoom

@dhess @hmac @brprice Please let me know your feedback or if you have any questions regarding the prototypes.

As we're currently working on better auto-generated names (#412), I wonder if we should not automatically generate names for top-level definitions, and instead prompt the student for a name when they press the "Create a new definition" (and "Create a new type") buttons.

The argument here is that top-level names are more important, and should be more meaningful and less generic, than the names we give to function parameters, pattern variables, lets, etc. The latter can be selected from a nicely-curated list of type-appropriate conventional names (e.g., a, b, m, n, etc.), but this is not true of top-level names.

I would argue that in most cases, or at least once the student reaches a certain level of aptitude, the first thing they'll want to do after clicking the "Create a new definition" button is to rename it, so we might as well make that part of the action.

It would be a nice UX improvement if we allowed the student to reorder the list of types and (especially) the list of definitions in the left-hand definition panel. I've even wanted this myself a few times lately, as it's nice to be able to group definitions by some relation (e.g., variables at the top, functions below).

In his exit interview, Harry mentioned an interesting idea. Imagine a puzzle mode in Primer where we give the student an unfinished program and ask them to fill the hole(s) to complete the program.

This would be an interesting way to teach kids about programming without requiring them to write programs from whole cloth. We could also give them much more complicated programs than they could write all by themselves, and upon completing them, allow them to evaluate the program to learn what it does or how it works.

I can imagine this being useful for evaluations in the classroom, as well.

I wonder if it would even be possible to teach programming indirectly in this way. What if we just gave students these puzzles and provided no explanation of how programs work, how to program, or what the various actions in the structure editor do, except for whatever help system and labels we provide in the UI? How much could they learn without any other assistance?

See below, we need to add arrows in the Eval detail screens when the step been selected.

A medium-term goal should be to replace Repl.it with Vonnegut in our Haskell lessons. This is a meta-issue that I'll use to track the progress towards this goal, and for related discussions.

(Note that I'm not speaking here of the exercises in our Haskell course. I suspect that will require quite a bit more effort. In this issue, I refer only to the embedded Repl.it iframes in our Haskell lesson web pages.)

The following issues are necessary, but not quite sufficient, to achieve this goal:

hackworthltd/vonnegut#307
hackworthltd/primer-frontend-web#72
hackworthltd/vonnegut#291
hackworthltd/vonnegut#320
hackworthltd/primer#112

One critical bit of functionality that is not yet captured by a tracking issue is program evaluation. I expect evaluation will be a fairly major project, so I'm marking this issue as "long term" for now.

Re: our eval timeline and how to render a marker for the "frame" that's being displayed in the main view, I made a fiat decision (sorry, all!) to go with hackworthltd/vonnegut#623 over hackworthltd/vonnegut#622. One of my reasons for doing that was so that the student can click on any reduction step in the timeline and jump to the frame that represents its end result. My hunch is that this will be more intuitive for beginners than representing the currently-displayed frame as an interstitial step between successive reduction detail buttons.

To fully explore my hunch and test its validity, we need to be able to:

1. Click on any button in the timeline and jump to the corresponding frame.
2. Double-click on the button to see the details.

This should also solve the problem that we currently have where, when clicking on a detail button that is not either the immediately preceding or immediately following step, there is not enough context in the main view to make sense of the details. The idea here will be that the student clicks on the button to jump to that frame, examines the state of the tree, and then double-clicks it to see the detailed steps showing how we got here from the previous state.

I think we're currently a bit too robotic with evaluation: the student can simply look for the green boxes and double-click them. For the most part, this will eventually result in the expression evaluating to its normal form (with endless reduction of recursive functions being a notable exception). So while we've slightly improved on Viz, where the we gave the student no choice at all, we can and should do better.

Some ideas would be to:

• show the list of reduction rules on the left-hand side of the screen, and require the student to choose the node (or nodes!) to which to apply the rule, and only then perform the reduction. Alternatively, they could right-click (or long press on mobile) on the node(s) and select the rule from a drop-down.
• Ask the student to mimic a particular evaluation strategy, to demonstrate understanding of, e.g., call-by-value vs call-by-name.
• Give the student a certain number of steps in which to reduce an expression to its normal form. Presumably this would require some kind of optimizer so that we could automatically determine a reasonable number of steps for any given (terminating) expression.

Currently when the frontend makes a request we set the CommState to Waiting. When we get a response we set it back to Ready. In this time, if any user action initiates a new API request the frontend will (almost) silently drop it. This ensures that the frontend's interaction with the API is completely serialised, but it could be confusing in real world usage.

We should consider how we want this to work in production.

Some other options are:

• Allow concurrent requests, and let the server figure it out
• Queue up concurrent requests

While testing eval mode, @annedino4 and I came up with a list of ideas for potential improvement. It's a long list and varied, so it's not ideal for a GitHub issue, but we should document them somewhere, so I'll create this tracking issue. As we tackle them, we can create individual issues for them and mark them here.

Not all of these are necessarily good ideas!

View the type of any node (#626)

We need to be able to click on a node in the eval view and see its type. This should probably work in the detail mode, as well.

Clicking/double-clicking detail view buttons

Assuming that the we highlight the detail view button that corresponds to the current program state in the main window (see hackworthltd/vonnegut#623 vs hackworthltd/vonnegut#622), then you should be able to click on that button to jump to that state of the evaluation. Then double-clicking it would zoom into the detail view.

Preview steps

Should we show a preview of the evaluation steps that will be taken when you select a redex? This might be helpful in understanding what's going to happen next. (It would probably be useful to allow the instructor to disable this feature, e.g., for examinations.) For example, in this situation, when I select one of the fs in this expression, I think we should highlight the let f and the λy.Zero so you can see what's going to be substituted for the f:

Another potential preview would be that, when you select a global variable, it shows the definition of that variable in a pop-up.

Add an evaluation "timeline"

We should have a timeline of sorts underneath the detail buttons, with a control you can grab to "scrub" the evaluation timeline back and forth, like you can do in a movie player to scrub frame-by-frame. This is basically the same as the forward and back arrows, but with a linear control.

Render all detail buttons as the same size and shape

I think the detail buttons would look nicer if they were all the same size and shape. Obviously some of them will have different amounts of whitespace, but that's better than differently-sized buttons.

App and APP nodes in patterns (#290)

In case patterns, we should show the App node(s) in the constructor patterns, since that's what the student will see in the matching scrutinee. For example, here the scrutinee doesn't have the same shape as the matching Cons x xs1 branch because the application nodes are missing in the pattern:

This is not unique to evaluation mode, of course, but I think here it's most painful, because the student is likely trying to match shapes by eye.

Only the parts of the tree affected by the reduction should change shape

Tree shapes should be "stable" under rendering in eval mode. What I mean by this is that portions of a tree that are not affected by a reduction will sometimes substantially change shape, which makes it difficult to focus on just the parts of the tree that changed as a result of the reduction. This will probably be hard to do with our current rendering system. (I think we need more control of layout than our current rendering system provides, for this and other reasons.) Here's an example from an application of map:

pre-step:

post-step:

Ideally, only the map node that we're reducing should change; the surrounding nodes (App, Bool, Nat, and the two APPs) should not move.

Easy to get confused when viewing the history of the evaluation

We need a better indication to the student when they're viewing the history of the eval steps. At the moment, when the student "rewinds" and goes back a few steps, the redexes at that step are still rendered with the green outline, and it's easy to forget that you're viewing history and not the next step in the evaluation sequence, so you select a redex and it can take a few moments before you understand why the "step" button isn't highlighted. Possibly the "step" button should just disappear when you're viewing history, and/or the redex highlights should change.

Saving evaluations for future reference

It would be great to be able to save evaluations in a list somewhere in the UI. Students could go back to them for reference, compare them to other evaluations, etc.

Back button

We really need a "back" button from the evaluation mode so you can return to edit mode (e.g., to see a definition) and then return to the evaluation, without losing your steps.

Text view (limited)

@annedino4 mentioned that she'd like a text view toggle for eval mode so that she can see the text representation of each evaluation step, even if we don't implement detail steps in text view.

Inline local variable "macro" step

It might be helpful to have an "inline local variable" macro that substitutes all occurrences of the variable in the expression under the let, all at once. For example, here there are 2 occurrences of f and it would be nice to eliminate them both in a single step:

(This would be in addition to the single reduction, not instead of, because maybe you only want to reduce the one that you expect to use in a later evaluation step.)

Clicking on detail view should zoom in and out

This is pretty low priority, but it would be nice, and would help situate the student, if, when pressing on a detail button, we zoomed into the detail view, and zoomed back out when pressing the "Back" button from the detail view.

If I recall, there was some debate during the sessions discussion about what should happen when you try to reload the browser with the old session slug, but you've since killed that server instance and now the session is invalid. Someone argued that it should just redirect to a new session, and someone said they'd prefer that the server complained so that they didn't think that the server had simply forgotten their program.

I'm here to say that I think "redirect to a new session" is obviously the right behavior. One of my biggest annoyances now in testing is restarting the server, refreshing the page in my browser and getting told that the session is invalid; and this happens a lot. (And I haven't once worried that my program had been lost because there's a bug. The kill-and-restart cycle is very quick.)

IOW, we should go from this:

to this:

I think this is an improvement for 2 reasons:

1. The UI element stays in a fixed location as you add new arguments, unlike the current design, which moves to the right with each new argument. The only effort the student needs to make in order to rapidly add 3 arguments to a new function is to click 3 times — no pointer movement is required.
2. We could then use the exact same control for unambiguously adding new arguments to split-view function types.

IMO, number 2 means we could probably drop grouped view altogether, as we'll have solved the main reason we added it in the first place, which was to ensure beginners don't get confused by which hole to select when adding a new arg to a Haskell-style function type.

This design is slightly less intuitive than the current design because the location of the + doesn't indicate exactly where the new argument will appear, whereas the current design does precisely that. However, I think that after using the button a few times, students will understand how it works.

We realised in https://github.com/hackworthltd/vonnegut/pull/285 that we should distinguish between (for want of better terms) patterns and expressions, where patterns define and bind new variables and expressions reference existing variables. In text view, patterns tend to appear on the left hand side of arrows. For example, x is a pattern in each of these:

λ x → ...

case e of
  Just x → ...

let x = e
 in ...

Whereas x is an expression (specifically, a variable) in each of these:

λ y → x

case x of
  ...

let y = x
 in ...

Patterns in Vonnegut have two forms:

• variable patterns, e.g. x
• constructor patterns, e.g. Just x

We currently only allow constructor patterns in case branches and only at the top level, so e.g. Cons (Just x) xs is not a valid pattern.

Patterns have a different a smaller set of rules governing their behaviour compared to expressions. As a user editing a program, the only things you can do to a pattern are:

• rename it
• replace it with another pattern
• (possibly) delete it?

Patterns also don't really "have types" in the same way as expressions, but we can still associate them with the type of expression they match.

(There's probably more info I can add here - I'll do that shortly)

Currently there's no special case - the lists are just empty. But this seems liable to confuse students - e.g. here it might look like there are two variables in scope called Types and Values:

We kept things simple in the original PR (#379) since we didn't reach any agreement on this (well, it was barely discussed).
One possibility:

• Remove the Types sub-heading if there are no type variables in scope. Likewise for values.
• If there are none of either, change the text Variables in scope to No variables in scope.
  • Alternatively, have a single sub-heading None, perhaps styled differently.

I suggest that we look into the styling of highlighted subtrees when we have time, currently it looks like this:

Maybe below is easier to read? More styling suggestions here.

For example, hovering over an App (or $) node would show text that reads, "Function application".

Consider the following small function:

There are two nodes labeled b in the function's expression. The first is a binding/function parameter:

The second is a "use":

What the student can do at each node is quite different, even though the appearance of both nodes is the same. I can easily imagine students clicking on the b at the use site and wondering why they can't rename it, for example. Likewise, they might think that they should be able to click on the b at the binding site and wonder why they can't do a case analysis on it there.

@hmac's PR hackworthltd/vonnegut#354 goes a long way to addressing this confusion by simply not displaying inappropriate actions at their sites. However, those actions aren't visible until the student actually clicks on the node. I wonder if we could further improve matters by rendering bindings/definitions differently than uses, perhaps with a color tint, or by using a bold font, or by drawing a thicker/double border around definitions, so that users have some visual indication of what sort of a or b it is they're looking at.

(This is a sort of syntax highlighting, I suppose.)

Not sure if this would be helpful at all

While writing this comment https://github.com/hackworthltd/vonnegut/issues/267#issuecomment-773497851, it occurred to me that there are many places where we want to use placeholder symbols (in the style of _) in Vonnegut, and we really out to be more deliberate about how we're choosing those. I would like not to use the same (or very similar) symbol for multiple purposes.

Places where we do this (or will need to do this) that I can think of offhand:

• ? for term hole
• ? for type hole
• _ for wildcard pattern "discard" (not yet supported, but would be the obvious choice)
• _ for partial application in function tuple syntax (#267) (maybe)
• ⎵ for empty parameter names in the user-defined type form UI (#226)

Placeholder, we'll discuss in more detail later.

We need a better way to render case expressions than what we're currently doing. The current implementation looks like this:

There are several issues here, but one chief issue is that the scrutinee, a1, is not visually distinguished between the branch labels, True and False.

@hmac had some thoughts that he posted in Keybase chat, which I'll reproduce here:

The next step is to have a UX meeting to discuss some ideas, but this will have to wait until some higher-priority UX issues are addressed.

We probably give our text projection too short shrift, or at least I am guilty of this. It would be nice to make it at least slightly more usable for the next few months while we restart the front end development.

What can we do to improve it in the current front end implementation, without too much extra work? One thing that seems obvious to me is to make some of the elements that are currently quite small easier to select. Making the default font a bit bigger would also help, or perhaps increasing the spacing between "nodes."

Once we have hackworthltd/vonnegut#419, we'll want to be able to selectively hide definitions, based on this design.

Should we show kind annotations for in-scope type variables in the sidebar? Currently the only kinds we have are Type and Hole, and I don't think the latter could possibly show up here. So it seems redundant. But then it'd be more consistent with value-level variables.

Alternatively, we could remove the Types and Values sub-headings and distinguish types by their kind annotation e.g. : Type. This might make most sense in a dependently-typed world. Do we even currently guarantee there are no name clashes between types and kinds?

We might also want to de-clutter the UI by grouping variables by type. So we'd have sub-headings like Bool, Nat etc. rather than repeating : Bool for every boolean variable.
This would be nice when we have a lot of variables with the same type, but may not work well if we have a lot of more complex types.

While reviewing our Code in UI document, I dug up an interesting comment that suggested creating keyboard hotkeys that correspond to the "icons" on some of the action buttons in the sidebar. For example, we show $ for function application, so we could make "$" a hotkey for inserting a function application at the cursor location.

This is quite a simple change, so I won't describe it in great detail. Currently our integration tests look like this:

  it "construct a program, step 1: add an annotation" do
    ( Edit
        [ MoveToDef id0
        , BodyAction
            [ (SetCursor id1)
            , ConstructAnn
            ]
        ]
    )
      `shouldConstructProgram`
        [ Tuple id0
            ( Def
                { defID: id0
                , defName: wrap "main"
                , defExpr:
                    ( Ann
                        ( Meta
                            (wrap 3)
                            (Just (TCEmb (TCBoth { tcChkedAt: (THole One), tcSynthed: (THole One) })))
                            Nothing
                        )
                        ( EmptyHole
                            ( Meta
                                (wrap 1)
                                (Just (TCEmb (TCBoth { tcChkedAt: (THole One), tcSynthed: (THole One) })))
                                Nothing
                            )
                        )
                        ( THole
                            ( Meta
                                (wrap 4)
                                (Just KHole)
                                Nothing
                            )
                        )
                    )
                , defType:
                    ( THole
                        ( Meta
                            (wrap 2)
                            Nothing
                            Nothing
                        )
                    )
                }
            )
        ]

i.e. they consist of performing an action, then testing that the result matches the given AST, written as source code.

This is a real pain to update when, e.g., we change how we do ID generation or how certain actions behave.

Instead, let's do this:

1. store the actions to run and the expected result in separate fixture files:

# test/fixtures/integration/construct_simple_lambda_1.action
[{"tag": "MoveToDef", ...}, ...]

# test/fixtures/integration/construct_simple_lambda_1.expected
[ { "unID": 0 }, { "defID": { "unID: 0 }, "defName": ... } ]

2. Write a single bit of test code that submits each action in each fixture and checks the response matches the corresponding expected fixture.

3. Write some code to regenerate the expected fixtures by submitting their corresponding actions and storing the result in the fixture.

This is basically the same flow we have for the serialisation integration tests. See for example backend/core/test/fixtures/def.json, frontend/test/Fixture.purs and frontend/test/GenerateFixtures.purs.

The advantage to this approach is that when we change something that invalidates a load of fixtures, we can just regenerate them and then check that the diff looks sane, rather than editing all the test files to update them by hand.

There are several evaluation steps which have to take special measures to avoid variable capture:

• λ reduction
• Λ reduction

In these cases we are creating a let binding to bind the argument in the body of the lambda. We default to the same name as the lambda, but if this would capture variables in the argument, we modify the name to find a safe one. See Vonnegut.Eval.makeSafeLetBinding.

• Pushing an application into a letrec

In this case we are pushing an application argument inside a letrec, so we need to be careful that the letrec doesn't capture variables in the argument. We simply refuse to apply this rule if there are variables in the argument which clash with the letrec. This doesn't impede evaluation because you can always inline variables in the argument to get rid of them.

None of these measure are described in the detail views, so it may be confusing to students when, e.g., a variable is renamed when converting to a let, or when an application sometimes can't be reduced across a letrec.

The student should be able to rename definition name cards and renamable nodes directly.

The interaction should be similar to PR hackworthltd/vonnegut#521

Type annotations can quickly build up during evaluation, and it's not clear whether they're a help or hindrance in understanding what is going on.

Some options:

• Add explicit rules for reducing annotations somehow
• Hide them when rendering expression trees in eval mode
• Remove all annotation nodes after each reduction step

We should work out what to do with constructs added in hackworthltd/vonnegut#291 and the tuple/tree style.

I said that

In rebasing, I have noticed that we do not deal with tuple style, and we should make a decision as to what we want to do. I believe our current strategy is to syntactically glom together all the lambdas or applications, rather than "caring about arity". The question to me is thus: what do we do with intermingled λ/Λ or term/type apps, and what about ∀?
e.g.

• λx.λy.Λα.Λβ.λz.Λγ. t
• t x y @α @β z @γ
• ∀ α:k1.∀ β:k2 . T

The options are to group without distinction, or to group with distinction;

• λ(x,y).Λ(α,β).λz.Λγ.t vs λ(x,y,@α,@β,z,@γ).t
• and similar for application (but we don't have to worry about changing Λ into λ@
• foralls: I think the only sane choice is to group them ∀(α:k1,β:k2).T

As we move to one canvas with multiple definitions in it, we will want to view type defs there also. We need to work out the ui for this

Definition name and step name to be shown in below screens:

Eval defult screen:

Eval detail screen: