Type Error Debugging in Hazel [part-ii-hazel]

This project will add some features to the Hazel language. Hazel is a functional research language that makes use of gradual types to support unusual features such as: holes (code place-holders) to give type meaning to incomplete programs. Importantly for this project, all Hazel programs, even ill-typed or incomplete programs, are evaluable. This allows dynamic reasoning about ill-typed programs via evaluation traces with the potential to improve the user’s understanding of why ill-typed programs go wrong.
This project aims to exploit further this potential by providing some extra features to both: aid with finding values/inputs that demonstrate why type-errors were found (type-error witnesses) and linking the evaluation traces back to source code.

Context

Part II Students 2024 [part-ii-2024]

September 10, 2024

In the final year of the Cambridge undergraduate degree in computer science, students undertake a coding project with an accompanying dissertation.

Type Error Debugging in Hazel [part-ii-hazel]

This project will add some features to the Hazel language. Hazel is a functional research language that makes use of gradual types to support unusual features such as: holes (code place-holders) to give type meaning to incomplete programs. Importantly for this project, all Hazel programs, even ill-typed or incomplete programs, are evaluable. This allows dynamic reasoning about ill-typed programs via evaluation traces with the potential to improve the user’s understanding of why ill-typed programs go wrong.
This project aims to exploit further this potential by providing some extra features to both: aid with finding values/inputs that demonstrate why type-errors were found (type-error witnesses) and linking the evaluation traces back to source code.

A Universal Data Access DSL [part-ii-udsl]

The design and implementation of a jq-like EDSL allowing programmers to abstract away the format in which data is stored (YAML, EXIF metadata etc.) and the file system being used – e.g. open("a/b/[c,d]") could mean "fields c, d in YAML file b of ZIP file a", or it could mean "fields b.c, b.d in JSON file a". My project would statically examine the filesystem to decide which case we're in, giving data scientists an easy way to declare the shape of the data they depend on. Success criteria include projection (correctly reading the data based on the file type), subtyping (e.g. JSON-LD is a child of JSON) and perhaps some compiler optimisations related to parsing (e.g. only loading a JSON library if the file is actually JSON).

Implementing Parallel Algebraic Effect Handlers in OCaml [part-ii-paraeff]

Algebraic effects are becoming increasingly common, but it can be difficult to use them in parallel computations. Xie et al. (2024) present a new structure for effect handlers which allows parallel subcomputations to perform effects independently without synchronisation. I plan to implement the traverse handler in OCaml 5 and evaluate its performance against equivalent programs which do not use effects using a variety of benchmark programs. As extensions, I will devise similar handlers for other types of parallelism, possibly including a more general form which works for many types simultaneously, and investigate how to improve its real-world performance.

Effective Geospatial Code in OCaml [part-ii-geocaml]

This project is co-supervised with Michael Dales.

Geospatial processing is critical in environmental science and is used in a range of environmental scenarios, both in areas of carbon accounting like digital Monitoring, Reporting and Verification in Reforestation Carbon Removal, and also biodiversity analysis like calculating worldwide extinction rates.
However there are problems with the current state of affairs, Python is one of the most popular data science libraries, and when doing geospatial data science with Python you use the GDAL geospatial data library. This workflow is not ideal [2]. For environmental scientists, interacting with the geospatial data in the imperative way that Python requires can be very difficult, and it is also not designed for the scale of computation needed for large geospatial projects. Furthermore, Python’s dynamic type system means that tricky type errors due to heterogeneity of data points can go unchecked. GDAL also only allows synchronous IO for loading GeoTIFF files, which can hurt performance.
I will write a non-blocking library for reading GeoTIFF files in OCaml (built on top of the WIP OCaml-TIFF library1 written by one of my supervisors, Patrick Ferris). I will then use OCaml to write an embedded Domain Specific Language (eDSL) which will be used to interact with geospatial data in a declarative way.

Backlinks

ICFP 2025 [icfp-2025]

October 24, 2025
Patrick Ferris

Two weeks ago I was fortunate enough to attend the International Conference on Functional Programming in Singapore. My first time in Asia and my second time at the conference, what follows are some thoughts and presentations I enjoyed whilst I was there.

I must thank my office mate (and friend!) Ryan Gibb for his camaraderie and sage advice: "the best track is hallway track". Not to mention all of his photos too. Thanks Ryan!

From right to left, top to bottom: Anil Madhavapeddy, Sadiq Jaffer, Patrick Ferris, Ryan Gibb and Roy Ang.

Random Hacking

October 24, 2025
Patrick Ferris

Below are just some of the pieces of random hacking I got up to whilst in Singapore.

OxCaml and Uring [oxcaml-and-uring]

Patrick Ferris

Jane Street were a big presence at ICFP 2025, carting along with them a shiny new OCaml compiler: OxCaml. If have been playing around with OxCaml recently but nothing outside toplevels in Javascript. Until now!

After talking to David, I spent some time converting a small corner of the ocaml-uring library to use a part of OxCaml. In particular making the following change:

  module Heap = struct
    type ptr = int32#
    (* ... *)
  end

  type cqe = {
    user_data_id : Heap.ptr;
    res : int32#;
  }

The idea being that a completion queue entry (a notification that some operation has completed) could be fully represented using 64 bits (two 32-bit, unboxed values). You can see how this impacted the library! I'm not certain about this change (and I'm sure I did it wrong) but it was nice to realise OxCaml gives you this kind of control. However, I am worried about the ergonomics of manipulating values like int32# and the temptation to case it into an int (presumably losing a good portion of the value of having an unboxed value in the first place).

Bibtex Parser

October 24, 2025
Patrick Ferris

On the flight over to Singapore, I started to write a post for this website. Some readers may remember that I use forester after a preprocessing step via graft to build this site. Part of that preprocessing consumes bibtex files and outputs forester trees. For the initial graft release I used the excellent Talaria Bibtex library. Unfortunately, it presented a pretty confusing API that, whilst nicely typed, felt a little cumbersome to use. Additionally, it was too specific in what it would accept as valid Bibtex. I wanted something that was a little more straight-forward to use (if a little fast-and-loose when it comes to types...). And so I built bib.

This was my first real attempt at using the Bytesrw library. I was happy with the results, although I did have to copy a substantial amount of code from other bytesrw-compatible libraries. I'd be happy to shift to this bytes-first world if it wasn't for the ever-present-in-my-mind issue of relocatable values in the OCaml heap!

Geocaml Libraries

October 24, 2025
Patrick Ferris

There has been some excellent outreachy work happening on the geocaml/ocaml-tiff library which is a potential Outreachy internship project for December 2025. More on this in a future post.

On the way back (and a little during the conference), I spent some time building an OCaml counterpart to geotessera, a library for working with Tessera. The library is not ready for people to use directly, but I was working on various constituent parts including:

Modern OCaml bindings to PROJ (a coordinate reference system projection library)
Further work on a WKT library for OCaml
Coming soon... ocaml-geotessera

Talks

October 24, 2025
Patrick Ferris

Hazel of OCaml at TyDe

October 24, 2025
Patrick Ferris

The type-driven development (TyDe) workshop was held on the first day of ICFP at the NUS School of Computing. I find the workshop name to be a little misleading, but perhaps this comes from my engineering background. The talks focused a lot on type theory, presenting the formal mathematics of interesting type systems with less focus on why it might be useful to have such an exotic type system... but then again, that was the nature of the entire conference.

I presented a talk on hazel_of_ocaml. The slides are here, along with the extended abstract. My talk ended up focusing a lot on the pedagogical benefits of having a type system that helped explain the most important thing a type system does... catch type errors! This work represents a small piece of work inside Max Carroll's excellent part II project, which he presented at the HATRA workshop: Decomposable Type Highlighting for Bidirectional Type and Cast Systems.

Scientific Programming at PROPL

October 24, 2025
Patrick Ferris

I think it is important to be honest whenever you get a talk accepted that you otherwise feel should not have been. My talk "what we talk about when we talk about scientific programming" is one such talk. The slides are here. The talk itself was nothing to write home about, but I think there were a few nice ideas that came out of it and the conversations I had with fellow PROPL attenders.

TMF Data Discrepancies Redux

October 24, 2025
Patrick Ferris

On the eve of my talk, I decided to re-run some analysis I did a few years ago on the tropical moist forest dataset, knowing that since then a few more years had become available. After fighting with some bit-rot in the Google Earth Engine script I had used, the new results were not very uplifting.

Land Use Class	Percent Change
Undisturbed	-2.9
Degraded	-5.5
Deforested	8.6
Regrowth	0.5
Water	0.0
Other	-0.6

The data in the table corresponds to the land use class values in Indonesia in the year 2008. The analysis computed the difference across each of the classes between the dataset released in 2021 and the dataset released in 2024. Most notably, the amount of deforested land has gone up by 8.6 percent!

As a somewhat tangential, though related, aside, I had the pleasure of talking to Sam Westrick, Seong-Heon Jung and Sundara Vishnu Satish of the ParCour research group. They were telling me about MaPLe, a programming language from the MLs built for parallelism. We discussed some ideas of using real-world, geospatial algorithms as benchmarks for MaPLe. Michael, if you got this far remind me to chat to you about this!

Shelter Reactions

October 24, 2025
Patrick Ferris

At the end of my talk, I briefly mentioned shelter. By far, this was the topic I got the most engagement on post-talk. During the conference, this was also true when people asked what I was working on. The tag line "a shell with undo" seemed to capture the attention of most people.

I'm feeling a renewed sense of interest in my own work thanks to that, even if the "research" contributions are not very apparent. However, I also had a good discussion with KC about the underlying MRDT in Shelter and how we might think about collaborating in the future on MRDT-related work.

Related to that, I managed to spend the evening in Chinatown with Roly Perera. Roly's work has focused on Fluid, a transparency-based programming language that allows authors to reveal their computation to their user. Excitingly, Roly presented a new text-based part of the language at PROPL. Our work is in the same universe, loosely orbiting some notion of reproducibility and explainability, but quite different in engineering work and how users might actually interact with our systems. I thoroughly enjoyed talking about solutions or research ideas that preserve existing workflows. Roly was great at pulling that out of the current work I have been doing.

Other Talks and Highlights

October 24, 2025
Patrick Ferris

I was a part of, often in a very small way, some other talks that were presented at ICFP including

Functional Networking for Docker, I encourage you to read Anil's notes on the topic. It is also worth mentioning Anil's post-posix talk (not unrelated to my Uring musings above).
Michael gave an excellent, very live, talk about Yirgacheffe at PROPL which I thoroughly enjoyed. I'm also excited about his recent developments which I'm sure you can clue into over on his blog.

Below is a non-exhaustive list of talks I enjoyed whilst at the conference. Some relevant, most of them not!

By far, one of the best talks was Polynomial-time Program Equivalence for Machine Knitting. I think the talk really nailed the "here's the idea, the details are in the paper"-presenting style as they described an "...algorithm that canonicalizes the algebraic representations of the topological semantics of machine knitting programs".
I attended most of the OxCaml tutorial presented by the incredibly friendly Gavin Gray.
Ryan's talk Spatial Programming for Environmental Monitoring at PROPL was excellent.

There's plenty more to talk about, and I'm sure my future posts will reference other parts of my experience at ICFP 2025. Thanks for reading, and if anybody is interested in any aspects of this do reach out!

OCaml Weekly 2025 w32 to w35 [ocaml-weekly-2025-w32-w35]

September 2, 2025
Patrick Ferris

I have been working on a few different OCaml-related projects over the last few weeks. This is also coinciding with my partner and I moving across the UK, which has made finding time to write weeklies and posts a little tricky. Nevertheless, here are some of the things I have been thinking about and working on!

I managed to publish one signficant post this month: a retrospective on Irmin.

Eio

September 2, 2025
Patrick Ferris

Increasingly, I'm feeling the dream of a unified framework for asynchronous IO slipping through the OCaml community's fingers. It is perhaps not such a bad thing, and I think with the right library authoring we can at least get to a place where it isn't so bad, for example providing read functions as opposed to using an opinionated IO library directly.

That being said, I am a very happy user of Eio when those choices do not matter, as is the case in building your own application (e.g. Shelter). To this end, I have spent a good bit of time upstreaming support for various missing pieces in Eio's API including:

Setuid and setgid fork action's for the process API.
Set process group support for job control in the process API.
Responding to Buf_write.of_flow request, and tinkering with the example there. I think this does highlight the awkwardness of making code portable across concurrency mechanisms, particularly with Eio's structured concurrency.
I did some investigating into EINTR bug which seems to be stemming from a known-issue on Uring in that writes are not buffered which usually does not matter except perhaps when there are parallel writes to stdout.
Spent some time thinking about the fiber local storage across domains issue, I've passed on some thoughts to folks working on this.

Vpnkit

September 2, 2025
Patrick Ferris

You might recall I was interested in using vpnkit. Hannes has done an amazing amount of work (patching and releasing) a series of packages to get this into a place that is much better and could be considered soon for merging. This defunctorisation is actually very useful for the Eio port I wrote a long time ago.

Papers and Talks at ICFP

September 2, 2025
Patrick Ferris

Somehow, I have ended up on lots of papers and talks at ICFP and the co-located events in October. The vaguely OCaml-related ones include:

Essentially a Vpnkit Experience Report.
An extended abstract on generating a corpus of ill-typed Hazel programs was accepted into TyDe workshop.
Relatedly, the work that project supported was accepted into HATRA which was the Part II project I supervised: Decomposable Type Highlighting for Bidirectional Type and Cast Systems.
And two PROPL talks!

Outreachy

September 2, 2025
Patrick Ferris

We have come to the end of another Outreachy round! I will write more on this soon in its own separate post. But for now I am very grateful to this round's mentors gridbugs and mdales, and also our fantastic interns. If you are interested, please do watch our demo day presentations.

The next round is fast approaching and we still need to work out the logistics. But I had a good conversation with mdales about possible Geocaml projects that I intend to submit!

Quarterly OCaml Q2 [ocaml-quarterly-q2]

July 18, 2025
Patrick Ferris

Thanks to Tarides sponsorship, I get to work on open-source OCaml. This quarterly is a companion to my weeklies, summarising the last three months of development, peppered with ideas and thoughts about OCaml, its community and its future.

What I wanted to work on?

July 18, 2025
Patrick Ferris

There were two main things I hoped to continue working on: ppxlib and outreachy. These are projects that I was previously working on, and in the case of Outreachy I have now been involved for many years.

In addition to this, all of my Part II projects this year used OCaml in some regard. In general, I want to see more adoption of OCaml. Over the years this has taken many forms including my initial work on developing workflows for OCaml that just turned five years old. This directly fed into the rebranding and rethinking of ocaml.org itself.

What I worked on?

July 18, 2025
Patrick Ferris

Ppxlib

July 18, 2025
Patrick Ferris

Ppxlib is the de facto standard library for building OCaml preprocessors. At the time of writing, opam list --depends-on=ppxlib informs me that there are 267 reverse dependencies. Janestreet is a heavy user of ppxes and has authored many.

One of the main accomplishments this quarter was bumping the internal AST to 5.2. This allows ppx authors to use new OCaml language features in their ppxes. In bumping the AST, we knowingly broke compatability for pretty much every single reverse dependency. As best we can, we have been sending patches to ppx libraries and helping users migrate to the latest ppxlib.

There is an interesting dicussion to had about the nature of open-source, and its interaction with industrial monorepos and community tended package repositories. Package ecosystems thrive whenever there is a dedicated community creating, maintaining and publishing packages. The idea is that the published world should be healthy. The publishing medium can act as natural limiting factor in the churn of breaking changes (in the case of OCaml this is via PRs to the opam-repository). This, I have come to notice, reacts poorly to changes coming from internally consistent monorepos where introducing breaking changes is easily fixed by applying patches there and then. Whatsmore, OCaml is often stated as an incredibly safe language to perform large refactorings thanks to its type system.

Ppxlib sits awkwardly in the space of possible breaking changes. Tied to OCaml's parsetree, impacts of changes there ripple down to ppxlib. The compiler itself can remain internally consistent, and is protected as it need only parse source code. Ppxlib, on the other hand, exposes the parsetree to users and thus any changes to the parsetree will likely be felt by ppx authors. Since I started working on ppxlib, it feels as though the number of syntax changes has gone up (primarily from Janestreet work). Unless we make changes to how we provide support for these, maintainers of ppxlib will forever be stuck doing busy work! Thankfully, Nathan has thoughts on how to improve this.

There are a slew of other features I have added to ppxlib including:

Support for deriving from classes.
Support for deriving from module bindings and signatures.
Fixing compiler and ppxlib dummy locations.
Bumping to 5.3.
Migrations for 5.4.

Outreachy

July 18, 2025
Patrick Ferris

Our two projects this year, one on claudius and one on dune, are going extremely well. At the time of writing, we just had a mid-internship call to catch up, and I was blown away by the progress each intern has made. Unfortunately, Outreachy is struggling with funding and the next round is perhaps not going to happen. This is a real shame and I am hoping that it will not be the case.

Outreachy has been a wonderful source of new, committed OCaml developers. If you haven't already, do peruse the webpage on OCaml.org to see past internships or watch the demo day presentations. For the mentors involved, I believe it has also been a rewarding experience (though at times a challenging one). We are always looking for new mentors and project ideas, please do reach out to me if you are interested.

Hazel

July 18, 2025
Patrick Ferris

OCaml's feature set allows it to shine at writing programming languages (and things of that ilk: compilers, interpretters, static analysis tools). Hazel is a research programming language with typed holes written completely in OCaml (via the reason dialect).

Relating this back to the original intent of my work, to improve OCaml adoption, I believe this also means keeping existing users happy. In the last quarter I developed a compiler from OCaml to Hazel. Whilst new features are still being added to Hazel, I hope this could serve as a tool to help develop test-suites and standard library functions using existing OCaml solutions. In a student's work (Typed Debugging for Hazel), we used this tool to build a corpus of ill-typed Hazel programs to great effect.

OCaml should continue to be a world-class programming language for building other programming languages. I hope to upstream some of this work to Hazel and provide some low effort maintenance to help keep their compiler in good shape.

Systems Programming in OCaml

July 18, 2025
Patrick Ferris

In a cross-over with my own research, I have been developing many tools related to systems programming in OCaml including:

An eBPF-based open syscall tracing tool.
A library in OCaml for spawning void processes.
A shell session manager that uses Irmin to manage sessions. It is nice to see a new push to finally land the direct-style Irmin PR!

This work is means to develop the underlying libraries that support it. For example, I have opened a few PRs to Eio to add new "fork actions" to the spawn API. I also investigated the feasibility of changing the underlying mechanisms in Eio to use Picos. In the future, I think this could be important avoid further splitting the OCaml ecosystem.

OxCaml

July 18, 2025
Patrick Ferris

I dabbled a little with OxCaml and build try-oxcaml to let people take it for a spin without having to perform opam repository gymnastics. It turned into a lot of work to track down some pretty inane bugs (type definitions differeing between js_of_ocaml and the OxCaml compiler, resulting in different Javascript runtime representations...).

This unblocked a few of my colleagues to get OxCaml working on tools like odoc_notebooks and x-ocaml.

Forester

July 18, 2025
Patrick Ferris

A good proportion of my work this quarter has been focused on how to present the very work that I am doing. Jon Sterling has been developing a tool for scientific thought called Forester which seemed like a possible candidate for writing and sharing my work.

Porting my existing blog posts and website content from markdown to Forester's LaTeX-inspired syntax didn't seem like an option. In particular, many of my posts made use of additional markdown-based tools (like ocaml-mdx).

This lead to the development of Graft: a preprocessor for Forester forests, converting markdown and bibtex to trees.

What's next?

July 18, 2025
Patrick Ferris

So, I worked on most of what I wanted to work on and then some! Going forward I hope to keep maintaining ppxlib in some capacity and coordinating the OCaml community's Outreachy efforts.

I hope to continue my small experiments (e.g. converting Eio to Picos). My own research makes heavy use of Irmin, and I would be interested to help with that too. More recently, a new library has been released for working with numerical data in OCaml called Raven: I am interested to use this library in Geocaml, a suite of geospatial tools written in OCaml that I maintain.

I feel conflicted about the OxCaml efforts. I admit, I am not fully aware of the full benefits of the features, but I worry about some proliferation of modes that make the type system in OCaml unbearable to use. On top of this, with my ppxlib hat on, I worry about the impact of changing the compiler so frequently, placing strain on an already small community. That being said, by releasing OxCaml separately I do believe running it as an experimental set of packages will help understand the tool better. But I would not be building anything I intend to maintain or research with right now as that ecosystem is far too volatile.

Finally, over the past two years I have done a lot of teaching. From Part II projects to supervisions. Going into next (academic) year, I intend to reduce my in-person teaching to focus on my research. However, I am interested in producing more materials for learning, maybe some of this in OCaml, perhaps something similar to Beautiful Racket. I have tried in the past to do these sorts of things, for example The Irmin Book.

Thank you

July 18, 2025
Patrick Ferris

Thank you for reading this wrap up! And thank you again to Tarides for letting me work so freely on things that I think are good for the OCaml community.

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?

reference. Hazel [hazel]

Cyrus Omar
https://hazel.org

Hazel is a live functional programming environment that is able to typecheck, manipulate, and even run incomplete programs, i.e programs with holes. There are no meaningless editor states.