/ml-repl

A REPL for a bare-bones subset of ML, to illustrate Hindley-Milner type inference using Algorithm W

Primary LanguageScala

ML Language REPL

(Work in progress)

A REPL for a bare-bones subset of ML, as presented in the course notes for the Type Systems for Programming Languages course at Imperial.

ML expressions are defined as a combination of what's presented in Milner's A Theory of Type Polymorphism in Programming and Damas's PhD thesis Type Assignment in Programming Languages:

$E ::= x\ |\ c\ |\ \lambda x . E\ |\ E_1 E_2\ |\ \text{let } x = E_1 \text{ in } E_2\ |\ \text{fix } g .\ E$

Type inference using Algorithm W is implemented in a manner which is visually very similar to the way it is presented in the course notes.

TODO

  • Fully implement ML expressions
  • Parse ML expressions
  • Implement Algorithm W type inference
  • Implement expression evaluation via beta reduction
  • Improve error messages
  • Add option to show intermediate steps for inference/evaluation
  • Polish REPL program