Render type parameters as lambdas, and render typedefs more like term defs

[dhess]

After some debate, we've decided that we would like to treat type parameters as being akin to term-level lambdas. Though they're not completely analogous, for our purposes, they're close enough, and the general consensus is that treating type parameters in this way will hopefully provide a bridge which leverages what students have learned about function parameters/lambdas to help them understand type parameters, in the sense that a type parameter binds a (variable) name to the scope in which the type's value constructors are defined.

To make the proposal more concrete, here's an example of how we might render a parameterized type in Primer's text representation, after adopting this proposal:

type Maybe : Type → Type

Maybe = Λα . Nothing | Just α

[Note here type is used as data is used in Haskell, and not as a type alias as would be the case in Haskell. Also, we're thinking that, as part of this change, we will drop the * notation in the frontend and switch to Type, as then it's obvious that parameterized types take an argument of type Type.]

Also, we should then change how we render typedefs in tree representation to match how we render term defs — currently, with the type of the type on the left, and the constructors on the right. We also tentatively agreed that it would be good to render value constructors under the type lambdas, as expressions would be in function bodies, and from left to right with boxes around each constructor that mimic how we render value constructors in match with patterns in terms, in order to reinforce the association of pattern-matching to the value constructors of the corresponding type.

Note that we don't expect this to require any major backend changes, as this is more or less a rendering decision, and not a change to the language's semantics. However, it should be reflected in Primer's terminology and documentation.

[georgefst]

I've certainly never liked rendering parameters off to the right - they just ended up there because it was the easiest thing to implement. And it's become really ugly now that we also display kinds.

My other idea had been to move back to something more form-like, with trees only where necessary (param kinds and field types), which would become feasible with #1043, which would free us from needing to represent each definition as a connected unit. But I'm increasingly keen on this approach instead. I really like the way that it unifies things with the term UI, by separating all parameter kinds in to their own subtree.

There are still some important details I'd like to work out before I can say I'm 100% behind proceeding with this:

Which character to use for the lambda?

The proposed new node is not really equivalent to either our current λ or Λ nodes, both of which appear only in value-level expressions. And I think this is the major reason why I was initially skeptical about this proposal.

But it now occurs to me that this problem is actually very closely related to how we used to confusingly use @ for both type-to-type application (where Haskell just uses space) and type-to-term application (where Haskell does use @), and now we unify these along with term-to-term as just ←. Those three applications correspond respectively to this new sort of lambda, Λ and λ, in that each lambda-abstraction is eliminated by the corresponding application. So actually, there's a strong argument for dropping big lambdas from the UI entirely, and rendering all three abstractions as λ! The only drawback I see here is that while applications are at least distinguished by the sort of their children, and thus can be identified based on whether they are rounded or not, this would not be the case for the existing value-level Λ and λ nodes.

(I originally suggested ∀, but @brprice pointed out that that would be odd since ∀ expressions do not get applied. After thinking this through above, it's now clear to me that this was a major misunderstanding on my part, and ∀ really wouldn't make any sense.)

How exactly should we render the tree?

The obvious first draft would be to have lambdas above the definition name, and keep everything else as-is. But I think this would look a bit odd.

We've discussed severing the links between the definition name and its two subtrees (again, helped by #1043). I'm in favour of this in general, but it's not clear quite how we should then connect the lambdas to the constructors. We played around with this a bit at our meetup two weeks ago but failed to come up with a compelling overall design.

This might be affected by whether we display constructors similarly to pattern boxes.

What action UX do we want?

One option would be that we modify the kind tree in order to add parameters, with lambdas being read-only, but I'm not sure this would be intuitive. It would also mean "choose a parameter name" modals being necessary for certain kind edits.

We could have an "add a parameter" action, which just adds a new parameter with kind *. And restrict actions on the kind tree so that we can only use it to change the kinds of existing parameters and not add new ones, i.e. don't modify the rightmost path.

Whatever we do, it's likely that some backend work will be required here. I think our API is slightly too tied to the idea of rendering each parameter kind separately.

[dhess]

I think I'm on board with the idea of unifying the symbols for all bindings as λ.

[georgefst]

The only drawback I see here is that while applications are at least distinguished by the sort of their children, and thus can be identified based on whether they are rounded or not, this would not be the case for the existing value-level Λ and λ nodes.

This concern actually disappears if we render variable bindings separately from the nodes which they are now currently part of: Λ, λ, ∀, let. This is an idea which @dhess has mentioned a few times* but I've previously been sceptical of because I'm wary of drawing subtrees which aren't subexpressions. But maybe we can find a clever way to render them, perhaps off to the right, to match patterns which are also non-expression trees.

Another advantage (and I think the original reason we'd discussed this) is that in eval mode, it would make it easier to see how a lambda is converted to a let in beta-reduction.

* I don't think we actually have an issue for this? Perhaps it belongs in #54.

[dhess]

Yes, I would like to find a way to visually unify bindings, while still respecting the important semantic differences.

[georgefst]

This concern actually disappears if we render variable bindings separately from the nodes which they are now currently part of: Λ, λ, ∀, let.

This is implemented in #1183.