Type checker prototype for dynamic languages Link Bibtex

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