Hazel and OxCaml [weekly-2025-05-04]
- May 10, 2025
- Patrick Ferris
I missed a week of posting last week, mainly because I spent more time writing posts.
Hazel of OCaml
- May 10, 2025
- Patrick Ferris
I mentioned previously that I was building a tool to transpile OCaml code to Hazel. This work is now in a good enough state that, along with one of my students, we have transpiled a good number of OCaml programs to help them write their evaluation for their third-year project.
I wrote up a little summary of that work, which I've transcluded below.
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?
OxCaml
- May 10, 2025
- Patrick Ferris
I spent some time this week getting more familiar with Oxidized OCaml. I have a habit of wrapping new OCaml tools and libraries into toplevel, browser applications. For example, try-irmin and try-eio.
Naturally, I tried to wrap OxCaml into a toplevel so people could play around with the new modes that are part of the OxCaml type system. This turned out to be a lengthy debugging session (where type declarations did not align so the raw Obj.repr js_of_ocaml representation was broken for some parts of the toplevel). I would say that I do question the time-spent/value trade-off, but a mostly working toplevel with OxCaml is available at: https://patrick.sirref.org/oxcaml.