hazelgrove/hazel

Hazel, a live functional programming environment with typed holes

Hazel

Hazel is a live functional-programming environment rooted in the principles of type theory. You can find the relevant papers and more motivation at the Hazel website.

You can try Hazel online: the dev branch is the main branch at the moment. Every other branch that has been pushed to GitHub and successfully builds can also be accessed at:

https://hazel.org/build/<branch_name>

Building and Running Hazel

Short version

If you already have ocaml version 5.0.0 and least version 2.0 of opam installed, you can build Hazel by running the following commands.

• git clone [email protected]:hazelgrove/hazel.git
• cd hazel
• make deps
• make dev

To view Hazel, you have to serve it, on localhost for development (you can't run it from a file:/// URL due to browser restrictions on e.g. web workers.)

If you have python3 on your path, you can use the Python server via make serve, then navigate to http://0.0.0.0:8000/ in your browser.

Otherwise, run make echo-html-dir which will echo the directory that needs to be served using some other server of your choice.

Long Version

If you are unfamiliar with ocaml or opam, do not have them installed, or just get stuck, we recommend you follow the step-by-step installation instructions contained in INSTALL.md.

Contributing

From OCaml to ReasonML

Hazel is written in ReasonML, which is a syntactic sugar atop OCaml. This link lets you type OCaml and see what the corresponding ReasonML syntax is: https://reasonml.github.io/en/try.

This is useful if you are trying to figure out the ReasonML syntax for something that you know the OCaml syntax for.

You can also convert between OCaml and ReasonML syntax at the terminal using refmt at the terminal. See refmt --help for the details.

Suggested Extensions for VS Code

Most of our team uses Visual Studio Code (VS Code) to write code. If you use VS Code, here are a few extensions that might be helpful.

• This extension provides full support for editing ReasonML source code and relevant tools:

  • ocaml-platform

• Due to Reason's poor parse errors, unbalanced parentheses can be difficult to find. The following extensions help with that.

  • Bracket Pair Colorizer 2
  • Indenticator
  • indent-rainbow

In addition to these extensions, enabling the breadcrumbs bar can make navigating a large code base easier. There are multiple ways to make the breadcrumbs bar visible:

• Click View / Show Breadcrumbs from the menu bar.
• Press Ctrl+Shift+P (macOS: Cmd+Shift+P), start typing breadcrumbs, and select View: Toggle Breadcrumbs from the dropdown menu to toggle breadcrumbs on and off.
• Press Ctrl+Shift+. to start breadcrumbs navigation.

Suggested Setup for NeoVim

If you enjoy your Vim binding and Vim setup, the following may help you set up your Reason IDE in NeoVim.

If you use vim, I recommend you to switch to NeoVim since it has a better support for multi-thread, and thus less likely to block you when you are programming.

To set up the LSP (Language Server Protocol), you need to set up your Language Client for Neovim and Language Server for ocaml.

• ocaml-language-server
• LanguageClient-neovim

After installing the previous two, you may want to copy the following to your neovim config file. (assuming npm have ocaml-language-server installed under /usr/bin)

let g:LanguageClient_serverCommands = {
    \ 'ocaml': ['/usr/bin/ocaml-language-server', '--stdio'],
    \ 'reason': ['/usr/bin/ocaml-language-server', '--stdio']
    \ }
" LanguageClient-neovim
nnoremap <F5> :call LanguageClient_contextMenu()<CR>
" Or map each action separately
nnoremap <silent> K :call LanguageClient#textDocument_hover()<CR>
nnoremap <silent> gd :call LanguageClient#textDocument_definition()<CR>
nnoremap <silent> gr :call LanguageClient#textDocument_references()<CR>
nnoremap <silent> gf :call LanguageClient#textDocument_formatting()<cr>
nnoremap <silent> <F2> :call LanguageClient#textDocument_rename()<CR>

Build System Details

Hazel is compiled to Javascript for the web browser via the js_of_ocaml compiler.

Though make targets are provided as a convenience, they mostly translate to dune commands.

Invoking make by itself is equivalent to invoking make dev. With these commands we pass additional flags to js_of_ocaml that cause the insertion of comments that map locations in the generated JS to locations in the source files. This is useful for debugging purposes.

make dev also auto-formats Reason source files using refmt (this is what the @src/fmt alias is for). This ensures code from all contributors follows the same style.

The make dev and make release commands do three things:

1. Generate some internal parsers using menhir.
2. Compile the Reason code to OCaml bytecode using the OCaml compiler.
3. Compile the OCaml bytecode to JavaScript (_build/default/src/hazelweb/www/hazel.js) using js_of_ocaml.

For a smoother dev experience, use make watch to automatically watch for file changes. This may require installing fswatch (see INSTALL.md). You can also run make watch-release to continuously build the release build (takes longer per build).

Clean Build

To obtain an clean build, you may need to:

• Clone the repository (if you have not), and enter the project root of your cloned Hazel project.

  git clone [email protected]:hazelgrove/hazel.git
  cd hazel

• Setup a local OCaml environment specific to the project, and compile. If you have setup a local OCaml environment (there is a directory called _opam), you may want to first remove it.

  # opam switch remove ./
  opam switch create ./ 5.0.0
  eval $(opam env)
  make deps
  make

This sets up a standalone OCaml environment in the cloned project, independent of the one you sent in your home directory. This allow you to alternate dependencies, or test dependencies changes, without affect existing OCaml projects.

NOTE: You may see the following warning when building:

Warning 58 [no-cmx-file]: no cmx file was found in path for module Ezjs_idb, and its interface was not compiled with -opaque

This is due to an upstream library issue and does not cause problems with Hazel:

OCamlPro/ezjs_idb#1

Debugging

Printing

You can print to the browser console using the standard print_endline function. This is probably the easiest method right now. Most datatypes in the codebase have something like [@deriving (show({with_path: false}), sexp, yojson)] on them. This generates helper functions for printing and serializing this data. For a type named t, the show function will be named show. Otherwise, for a type named something else like q, it will be show_q.

Source Maps

js_of_ocaml does support source maps and has some other flags that might be useful. If you experiment with those and get them to work, please update this README with some notes.

Debug Mode

If Hazel is hanging on load or when you perform certain actions, you can load into Debug Mode by appending #debug to the URL and reloading. From there, you have some buttons that will change settings or reset local storage. Refresh without the #debug flag and hopefully you can resolve the situation from there.

Testing

You can run all of the unit tests located in test by running make test.

Unit tests are written using the Alcotest framework.

Continuous Integration

When you push your branch to the main hazelgrove/hazel repository, we have a GitHub Action setup (see .github/workflows/deploy_branches.yml) that will build that branch (in release mode) and deploy it to the URL https://hazel.org/build/<branch name>, assuming the build succeeds.

It usually takes about 2 minutes if the build environment cache hits, or 20+ minutes if not. You can view the status of the build in the Actions tab on Github.

hazel's Issues

Next/previous hole actions

Add current git hash to the UI

Log UI interactions

Refactor view layer into Elm architecture

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.

Hexadecimal int constants. (Maybe with arbitrary base.)

Renumber holes action

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.

Cannot insert `let` at start of `let` sequences, which only grow from start to end

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:

`omega` causes the page to hang

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?

Add `in` delimiter to `let`

Make backspace/delete not generate a new hole number on empty holes

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!

Remove unused @deriving show

Finish Coq core and replace hazel_semantics.ml with the extracted output

Convert everything to Reason syntax

compute a mapping from locations to z-expressions

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?)

Switch to Dune

rebuild isn't supported anymore

Disable live evaluation in study mode

Add labeled products

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.)

minimal parenthesization

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?

Pattern guards

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.

Tutorial page

improve handling of line breaks and indentation in pretty printer

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

Highlighted expression construction buttons when cursor is in types

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

Timeout holes

To prevent infinite loops

Sometimes I can delete things that I should not be able to

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

Restart hole numbering whenever the program becomes complete

Include non-empty holes when moving to prev/next hole

Inductive definitions of typing and action rules and statement of theorems in Coq

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.

decide about using Bucklescript

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

Make move to prev/next hole actions wrap around

Typing a comma before a closing paren in a type produces the comma after the closing paren

type variable instantiation at applications

relevant papers:

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

Extract a language definition from Coq core using coqdoc

Undo / redo

make column width of pretty printer depend on viewport width

Cursor on delimiters

reorganize chrome to look more like mockup

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.

Binary trees

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.

Pages

Enable arbitrary variable names and add new cursorinfo state indicating invalid name

Zoom in shortcut (Ctrl +) doesn't work

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.

Hard-coded left injection

hazel/src/semantics.v

Line 802 in a04ae65

(ZExp.RightAsc (HExp.Inj side (HExp.EmptyHole u')) (ZTyp.LeftSum (ZTyp.CursorT HTyp.Hole) HTyp.Hole)),

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

Import / export to Git

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

case around a construct inj in a hole doesn't remove hole

List literals

transition from Reason 2 to Reason 3

some major syntactic changes so we should do this soon.

there is some automatic way to do this conversion.

Logic for editing variable bindings

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).

Auto-update website Hazel

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

Create Steps module with prepend/append_step

Improve font choice

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.

Makefile / install.sh

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.