An experimental subset of OCaml, using constraint-based type inference!
Dromedary is a work-in-progress implementation of a constraint-based type checker for a large subset of OCaml. It is largely based on the work of François Pottier's Hindley-Milner elaboration in an applictive style and the constraint language presented in The Essence of ML Type Inference.
Dromedary implements significantly more features than the language presented in Pottier's paper, including:
- Algebraic data types and pattern matching
- Mutually recursive let bindings
- Side-effecting primitives and the value restriction
- GADTs
- Polymorphic variants
- Semi-explicit first-class polymorphism (record fields only)
- Type abbreviations
- Structures
For a description of the thoery of these extensions in a constraint-based setting, see the accompanying dissertation.
Dromedary is written in OCaml. You'll need to install OCaml version 4.12.0 and opam.
Once installed, run these commands to get started!
make install
make build