A type checker prototype for a custom functional language, featuring:

• Set-theoretic types (with intersection, union, negation and recursive types)
• Precise types for functions, pairs and records
• Parametric polymorphism
• Type inference
• Optional user type annotations
• Precise typing of type-cases (occurence typing)
• Pattern matching

Some missing features (and thus, future work):

• Support of side-effects
• Row polymorphism for records

This prototype is implemented in OCaml (source code), and a (slow) web version using js_of_ocaml is available for testing.

A DOI for an older version is available: http://dx.doi.org/10.1145/3462306