Sulfur

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.

Features

• 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")

Hacking

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

References

Sulfur is a research project towards the design and implementation of functional programming languages, and uses the following references for its implementation.

• Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism
• Grace, a functional programming language with a bidirectional type system