Sulfur is a simple functional programming language derived from ML and implemented in OCaml with rich type inference. It makes use of bidirectional type system in the spirit of the Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism paper which allows for terms to be inferred with minimal type annotations.
- Type inference and type checking Types of expressions can be inferred with miniaml type annotations. At most, a single top-level type annotation is required in order to infer more complex types.
- Higher rank polymorphism
Universal quantifiers (
forall
) can appear inside the right-hand side of a universally quantified type. This allows functions to accept and return polymorphic values. As an example:
x :: (forall a. a -> a) -> (Int, String)
x f = (f 42, f "meaning of life")
This project uses dune
and opam
. To create a development environment, create a local opam
switch.
# This command will take some time
$ make dev-switch
Once the dependencies are installed, you can now run dune
commands for development.
# Build the project
$ make build
# Test the project
$ make test
# Generate coverage report
$ make coverage
Sulfur is a research project towards the design and implementation of functional programming languages, and uses the following references for its implementation.