Authors: Addison Sasko, Reed Mullanix
What is the problem?
We will be using prolog to implement a type-checker and interpreter for a subset of ML. This will include HM type inference.
What is the something extra?
We will first create a parser using DCGs that creates an abstract syntax tree. After that, we will use Algorithm W to infer the most general type of the expressions, as well as check that the program is well typed. Finally, we will implement an interpreter that takes the type-checked AST and executes it to produce a value.
What did we learn from doing this?
The bottom line is that prolog does make implementing type-checking algorithms easy, but debugging and checking for mistakes is very, very difficult, and the code becomes very difficult to read after it hits a certain point. This is exacerbated by the fact that you need to give everything a name, and can't nest function calls. All in all, this was an interesting, if not challenging, exercise.