Reference. Hazelnut: a bidirectionally typed structure editor calculus [omar-hazel-2017]

2017
Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, Matthew Hammer
10.1145/3093333.3009900
https://doi.org/10.1145/3093333.3009900

Abstract

2017
Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, Matthew Hammer

Structure editors allow programmers to edit the tree structure of a program directly. This can have cognitive benefits, particularly for novice and end-user programmers. It also simplifies matters for tool designers, because they do not need to contend with malformed program text. This paper introduces Hazelnut, a structure editor based on a small bidirectionally typed lambda calculus extended with holes and a cursor. Hazelnut goes one step beyond syntactic well-formedness: its edit actions operate over statically meaningful incomplete terms. Naively, this would force the programmer to construct terms in a rigid "outside-in" manner. To avoid this problem, the action semantics automatically places terms assigned a type that is inconsistent with the expected type inside a hole. This meaningfully defers the type consistency check until the term inside the hole is finished. Hazelnut is not intended as an end-user tool itself. Instead, it serves as a foundational account of typed structure editing. To that end, we describe how Hazelnut's rich metatheory, which we have mechanized using the Agda proof assistant, serves as a guide when we extend the calculus to include binary sum types. We also discuss various interpretations of holes, and in so doing reveal connections with gradual typing and contextual modal type theory, the Curry-Howard interpretation of contextual modal logic. Finally, we discuss how Hazelnut's semantics lends itself to implementation as an event-based functional reactive program. Our simple reference implementation is written using js_of_ocaml.

Backlinks

A Transpiler from OCaml to Hazel [hazel-of-ocaml]

May 2, 2025
Patrick Ferris

Over the past few months, I have been piecing together a transpiler from Hazel to OCaml. This is, in part, to help one of my third-year undergraduate students who is working on type error debugging in Hazel.

Typed Holes

May 2, 2025
Patrick Ferris

Hazel is a functional programming language with typed holes. Holes are pieces of your program that have not yet been filled in. Holes can appear anywhere in your program both as expression or types. Hazel can still evaluate your program in the presence of holes.

To get a flavour of Hazel, take a regular map function for lists.

let map = fun f -> fun xs -> case xs
  | [] => []
  | x :: xs => f (x) :: map(f)(xs) 
end in
map(fun x -> ?)([1, 2, 3])

The question mark (?) is a hole. The program evaluates to the following expression of type [?] (for people more familiar with OCaml types ? list).

[ ?, ?, ? ]

Hazel supports local type inference but nothing involving unification variables. For example, a simple add_one function in Hazel (fun x -> x + 1) has type ? -> Int.

From OCaml to Hazel

May 2, 2025
Patrick Ferris

The ability to transpile OCaml programs to Hazel programs is motivated by one simple thought: there are more OCaml programs than there are Hazel programs. This could help bootstrap projects by alleviating the need to rewrite boilerplate code (e.g. URI parsing or standard library functions for strings).

A Transformation of Syntax

May 2, 2025
Patrick Ferris

Hazel markets itself as an "Elm/ML-like functional programming language". From the previous example of map, it should be apparent just how close to OCaml the language is.

It turns out that a majority of the transpiler is a transformation of syntax. Take a simple ADT for an arithmetic programming language.

type expr =
  | Float of float
  | Add of expr * expr
  | Sub of expr * expr
  | Mul of expr * expr
  | Div of expr * expr

And when we run hazel_of_ocaml over this OCaml type declaration.

type expr =
  + Float(Float)
  + Add((expr, expr))
  + Sub((expr, expr))
  + Mul((expr, expr))
  + Div((expr, expr))
 in ?

Not much has changed expect some syntax. Hazel does not have a notion of top-level expression so hazel_of_ocaml wraps the program into one set of value bindings. For the most part, Hazel acts as a subset of the pure, functional part of OCaml. At the time of writing, this subset is fairly limited with no support for modules or labelled records out of the box (there are plenty of development branches with these features).

If we try out the same map function but written in OCaml and transpiled to Hazel we get.

let rec map f = function
  | [] -> []
  | x :: xs -> f x :: map f xs

Which becomes the following hazel program.

let map = fun f -> fun x1 -> case x1
  | [] => []
  | x :: xs => f(x) :: map(f)(xs)
end in ?

We could have a field day discussing the syntax of OCaml and Hazel (parentheses for function arguments, well-scoped cases for pattern-matching, a different arrow for pattern-matching etc.). What would be more interesting is taking a look at how to handle polymorphism in Hazel.

Explicit Polymorphism

May 2, 2025
Patrick Ferris

Hazel has explicit polymorphism. So far, we have not seen it as we have let the types have holes in them. The map function in OCaml has the following type.

val map : 
  ('a -> 'b) -> 'a list -> 'b list

We must remind ourselves (by reading Craig's excellent blogpost on the matter) that in OCaml

... type variables in signatures are implicitly universally-quantified

So in reality, we have that map has the following type.

val map : ∀ a b. (a ->  b) -> a list -> b list

In Hazel, we have to explicitly type our map function to be polymorphic. Not only does this mean the type annotation requires universally quantified type variables, but we must also perform type application wherever we choose to apply the map function (whether that be recursively or somewhere later in our program).

let map : forall a -> forall b -> (a -> b) -> [a] -> [b] =
  typfun a -> typfun b -> fun f -> fun xs -> case xs
    | [] => []
    | x :: xs => f (x) :: map@<a>@<b>(f)(xs) 
end in
map@<Int>@<Int>(fun x -> ?)([1, 2, 3])

forall introduces a universally quantified type variable into our type annotation, and typfun introduces it into the function itself (à la System F). Type application requires @<T> where T is some type. This allows hazel to quite easily support higher rank polymorphism, but we will not worry too much about that.

Propagating OCaml Types into Hazel

May 2, 2025
Patrick Ferris

Most often, OCaml users interact with prenex polymorphism (rank-1) where the universal quantifiers are at the front of the type. OCaml does support quantifiers inside certain types like records.

What this means for the transpiler is that we can reuse OCaml's type inference to safely instantiate the correct type annotations and type applications in Hazel! To do this, hazel_of_ocaml uses Merlin to inspect the type of the function in either a value binding or at the point of a function application.

Take a simple, polymorphic length function.

let rec length = function
 | [] -> 0
 | _ :: xs -> 1 + length xs

let int_len = length [ 1; 2; 3 ]
let str_len = length [ "only"; "two" ]

When we run this through hazel_of_ocaml with the -type flag we get.

let length : forall a -> [a] -> Int = typfun a -> fun x1 -> case x1
  | [] => 0
  | _ :: xs => 1 + length@<a>(xs)
end in
let int_len : Int = length@<Int>(1 :: 2 :: [3]) in
let str_len : Int = length@<String>("only" :: ["two"])
in ?

hazel_of_ocaml has correctly instantiated the type for length inside the recursive function and then in each case with the integer list and the string list.

A Corpus of Hazel Programs

May 2, 2025
Patrick Ferris

The impetus for this work was to derive a corpus of ill-typed Hazel programs. Luckily, such a corpus exists for OCaml! Seidel et al. created a corpus of OCaml programs from their undergraduate students at UC San Diego. Some of these programs have been transpiled to Hazel.

Future Work

May 2, 2025
Patrick Ferris

Hazel is a fun, research programming language. Potential third-year students may find it interesting to take this work further. For example, how would this look in terms of a module system? From a purely engineering perspective, plenty of work would be needed to convert a multi-library OCaml project to Hazel (e.g. handling the cmi files).

Another line of research would be to have Hazel target one of the intermediate representations in OCaml which would give Hazel a fully functioning compiler to "native" code?