We should give an inductive language definition and at least state the metatheorems and the theorems relating the functional implementation to the inductive definition. We can prove them later once the language design stabilizes.

We want to put parenthesis into the pretty printed output only where it is necessary to avoid ambiguity, rather than everywhere.

I have some intuitions about how this would work, but is there an established algorithm for this?

We should think more carefully about which font we are using.

One option is to use one with programming ligature, e.g.:

• Fira Code
• Cascadia Code
• Hasklig

These can look nice, but for beginners, it may be the case that they are confusing ("How do I enter that symbol?")

One way to address that problem might be to use a non-ligatured font until they get to a certain point in the tutorial and then give them the option to enable the ligatured font (of course, that option should also appear in some sort of preferences pane, and then we need to figure out how preferences are persisted and all of that).

Here are some nice monospace fonts:

• MonoLisa [non-open]

This does not necessarily need to be addressed soon, just creating a tracking issue since I was recently sent a couple of links to fonts we might consider (see above). Though we should not discount seemingly superficial design issues for too long either, they can have subtle but important effects on user perception of the project as a whole.

There is a tyxml interface to virtual_dom so it should not be too complicated:

https://github.com/janestreet/virtual_dom/blob/master/src/tyxml.ml

The benefit is that we won't be re-rendering the entire expression view on each change. Haven't really experienced any slowness yet, so this isn't high priority, but I imagine that for thousand-line Hazel programs in the future, this will be handy.

The zoom out keyboard shortcut works, but the zoom in shortcut (Ctrl +) creates a let-binding instead. Looks like the key listener that listens for the = key ignores modifiers and blocks the default zooming behaviour.

Trying to write (\x : _. x x) (\x. x x) makes the page crash in the browser. I'm wondering if this is due to a missing occurs check?

I'm on a mac, using Chrome, and doing Control-D, which for me is "delete".

rebuild isn't supported anymore

Iterated ML-style constructor applications to build trees for tests and small examples are a real pain point. If you have a particular shape in mind, it can be hard to see if you've actually attained that shape. Much easier would be a palette that let you draw it, tikz style, and interop'ed with the datatype constructors in the described way.

You may also want to have a function like complete : list A -> tree A that builds a complete tree with the elements of the argument at the leaves, or stick : int -> A -> tree A that makes a linked list of a given length with the repeated argument, or something, as tools that you use in the drawing in the place of nodes to produce whole subtrees that you combine in a particular way. (I've done exactly this for lecture notes any number of times.)

The nice thing is that the kind of gives you a schema for a tree-palette for any W-type, since all inductive types are basically trees with whacky node names if you squint at them the right way.

Sometimes hole numbers get really large even though there aren't a lot of holes in the program. It would be good to be able to explicitly renumber holes. Should be a nice simple starter project for somebody.

The current action semantics for let construction assumes that the cursor gives the RHS of the constructed let form. Sometimes, however, we want the cursor to give the BODY of the constructed let form, leaving the cursor in an empty RHS.

In particular, when we have an existing sequence of lets, there is currently no way to insert a new let at the start of the sequence. Consequently, let sequences can only be constructed (currently) from the outside in (from the start of the sequence to the end, and never in any other order).

For example, you cannot currently insert a new let just ahead of the first x, below:

There is a Git implementation in OCaml that compiles using js_of_ocaml. Would be cool to be able to save/load to Git.

https://twitter.com/eriangazag/status/1053308261783535616

To prevent infinite loops

I can use the = and c keys for Let and Case when I'm in a type.

Reason uses this library, might be something we can draw from this (probably can't use it directly because we need to generate HTML and some stuff on the side):

https://mjambon.github.io/mjambon2016/easy-format.html

so that you can place a cursor anywhere in the view and get the corresponding z-expression

(set of z-expressions in some cases? richer cursor model?)

the build.sh thing is a little clunky, we should have a proper makefile (or whatever the equivalent is?) and an install.sh script that runs the proper opam commands.

this will happen via Travis, side benefit we will get CI too.

relevant papers:

• Dunfield and Krishnaswamy 2013
• this paper on adding type consistency to that: http://i.cs.hku.hk/~bruno/papers/gradual-esop18.pdf

The Successor ML version of them is quite nice because the guard is part of the syntax of patterns (compared to the OCaml one and others where it is part of the syntax of rules).

John Reppy had a short paper at the ML workshop 2019 for reference.

before too much new UI code gets written, we should decide if we are going to use Bucklescript or js_of_ocaml. Discuss!

from SNAPL 2017 paper.

also would be good to factor out the surrounding chrome into hazel_chrome.ml, rather than it all being in hazel.ml.

There are really two actions here:

• Edit variable binding in place without renaming all uses (so uses can become free or rebound)
• Rename all uses

I think initially, we'll follow the principle of "hybrid structure editing" and do what you would expect in a text editor, i.e. option 1.

It would be good to add either a one-time shortcut or a user toggled setting to change the behavior to the rename-all-uses option when you want that.

In the case of rename all uses, we have to figure out what to do in the situation where the new name is shadowed by another binding at the use site. One option would be to add a de Bruijn style "skip" argument to each variable use that allows you to skip back n bindings of that variable, with the default being 0 (and not shown).

some major syntactic changes so we should do this soon.

there is some automatic way to do this conversion.

Seems like there's a bug where injection construction always creates a Left injection, even when the user asks for a right injection.

Right now, it deletes the hole and replaces it with a fresh hole. This ends up looking stupid. This would be a good starter project for someone!

Introduction

TODO: what are labeled products
TODO: why do we want them in Hazel
TODO: what do we have now

Labeled Product Types

TODO: add .label as a new type form
TODO: recognize operator sequences containing .label1 ty1, .label ty2, ..., .labeln tyn as labeled product types
TODO: do we want to allow partially labeled product types?

• allow non-labled prefix, but once you use a label as subsequent positions have to be labeled
• alternatively, allow labeled and non-labeled positions to be interleaved
  TODO: how does this affect type equivalence? e.g. are (.x Num, .y Num, .z Num) == (.z Num, .y Num, .x Num)
  TODO: singleton labeled products -- should we support them (.x Num is a labeled product type?)
  TODO: syntax errors

• .label1 .label2 ty
• .label1 by itself
• .label1 ty .label2
• we will need some way to mark erroneous uses of labels and indicate that in the cursor inspector
• duplicate labels: (.label1 Num, .label1 Num) is not a valid type, so we also need duplicate label errors

• does the error message go on the subsequent uses, or on the type as a whole?

Labeled Tuple Expressions

TODO: add .label as a new expression form
TODO: similar considerations as above
TODO: can you omit labels by providing values in order: (1, 2, 3) <= (.x Num, .y Num, .z Num)
TODO: "Record punning" in Reason: {x, y, z} => {x: x, y: y, z: z} -- is there anything analogous that we can do? Does this interact with positional values? (y, x, z) <= (.x Num, .y Num, .z Num) does that operate positionally or via punning?
TODO: partially labeled values, where some of the arguments are in order: (1, 2, .z 3) <= (.x Num, .y Num, .z Num). what about interleaving vs. requiring all the explicit labels at the end ala Python?
TODO: what are the type synthesis and type analysis rules for the labeled tuple expressions

Projection Expressions

TODO: add e.label as a new expression form
TODO: can you press backspace on e |.label and get to e.label?
TODO: can you press space on e|.label and get to e .label
TODO: what are the type synthesis and type analysis rules?

Labeled Tuple Patterns

TODO: similar considerations to labeled tuple expressions
TODO: we might want punning for labeled tuple patterns:

f(.x 1, .y 2)```
instead of 
```let f = fun(.x x, .y y) ...
f(.x 1, .y 2)```
TODO: what are the pattern type synthesis and pattern type analysis rules? (ask Yongwei for paper draft if you want to formalize)

# Other Ideas

TODO: clean up

# Overall Possibilities

Option 1: Use reason like ~label annotations
Option 2: Use a space to separate between label and type/expression/pattern.  Period operator is added before label to specify that it is a label. Ties in well with linking the period to labeled products, as the period is also used for projection.  Possible problem: Issues with using a period as both binary operator (projection) and unary operator (label definition)
Option 3: Use space operator between labels and type/expression/pattern.  Problem: No way to tell distinction between undefined function variable application and labeled expression
Option 4: Use colon operator between labels and type/expression/pattern.  Problem: Confusion between type annotations and labeled pair type annotation
Option 5: Use colons and braces to signify a labeled tuple.  Problem:  This syntax is more typical for a record, and may create confusion about labeled tuples as a value and records as a type definition, as well as create issues if there are any future plans for adding records to Hazel, makes development task larger to define braces syntax

# Labeled Product Types

Currently: `ty1, ty2, ..., tyn`
With Labels: `~label1: ty1, ~label2: ty2,..., ~labeln: tyn`
With labels: `.label1 ty1, .label2 ty2, ..., .labeln tyn`
With labels: `label1 ty1, label2 ty2, ..., labeln tyn`
With Labels: `label1: ty1, label2: ty2, ..., labeln: tyn` 
With labels: `{label1: ty1, label2:ty2, ..., labeln:tyn}'

# Labeled Product Expressions

Currently: `e1, e2, ..., en`
With labels: `~label1=ty1, ~label2=ty2, ..., ~labeln=tyn`
With Labels: `.label1 e1, .label2 e2, ..., .labeln en`
With Labels: `label1 e1, label2: e2, ..., labeln: en`
With Labels: `label1: e1, label2: e2, ..., labeln: en`
With labels: `{label1: e1, label2:e2, ..., labeln:e2}'

# Labeled Product Patterns
Currently: `p1, p2, ..., pn`
With Labels: `~label=ty1, ~label=ty2,..., ~labeln=tyn`
With Labels: `.label1 p1, .label2 p2, ..., .labeln pn`
With Labels: `label1 p1, label2 p2, ..., labeln pn`
With Labels: `label1: p1, label2: p2, ..., labeln: pn`
With labels: `{label1: p1, label2: p2, ..., labeln: pn}'

In pattern position, we would also want to support type annotations.

# Projection

Currently: no projection
With Labels: `e.label`

(For many of these, we will need label holes.)