This project, originally conceived by Anil Madhavapeddy, hopes to make it easier to answer questions like "What is the safest route to Pembroke College from Cambridge train station?". Here, "safest", can have lots of meanings: the best lit road, a route with tactile paving or accessible pedestrian signals etc.

In addition to this, we may wish to provide suggestions for how to improve the current folksonomy of information OSM stores.

Following the work of Adaptive Functional Programming and Implicit self-adjusting computation, this project will build an incremental computation engine in OCaml alongside an expressive combinator library for build such computations. As an extension, a small DSL will be built that makes use of the engine to build an implicitly incremental programming language.

The core of this project is to implement an eDSL and a runtime in OCaml for self-adjusting computation. I also propose a new TDT which allows for generic monoidal folds over modifiable sequences: the library will include a native foldMap primitive that allows performant reduction over a modifiable sequence of modifiable values for any general monoid, giving logarithmic updates with a small trace. I will then compare foldMap to the generic fold implemented in plain SAC.

-- From Boris' Proposal

This project wants to reuse OCaml's typechecker to provide a safe way to create graphics shaders. As an extension, a ppx rewriter will provide a translation layer from OCaml to the embedded DSL making it possible to write shaders in a subset of the OCaml language.

When interacting with the GPU for graphics programming, parts of the rendering pipeline are written as standalone shader programs. The standard method of using these is to store the shader source code as a string, which is then compiled at runtime by the GPU driver. This is not a performance issue, as shader programs are usually small enough that compilation time is negligible. However, it does mean simple syntax errors or incorrect types, which would normally be caught at compilation, won’t manifest until the entire program is run.

I propose a new library, Shaders_of_ocaml, allowing for shader programs to be written inline as native OCaml, which is then compiled to shader code strings to be passed to the existing graphics libraries. This would allow the OCaml compiler to provide type checking for every shader written.

-- From Rohan's Proposal

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.

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

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.

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.

This project was completed by Michał Mgeładze-Arciuch and supervised by Anil Madhavapeddy and Patrick Ferris.