# -*- mode:text; coding: utf-8 -*- [ Note: still a work in progress. ] This is an implementation of the constraint-based type inference algorithm described in chapter 10 of Advanced Topics in Types and Programming Languages, "The Essence of ML Type Inference", by François Pottier and Didier Rémy. The book: http://www.cis.upenn.edu/~bcpierce/attapl/index.html The chapter: http://cristal.inria.fr/attapl/ At 100 pages (with the extended version at ~150 pages!), it's pretty challenging stuff, even after a year of studying type theory. But as far as I know it's the only complete published description of a constraint-solving type inference engine. My intent with this code is to have a standalone implementation that can be easily understood and experimented with. The 'mini-prototype' code that comes with the chapter is 1) written in OCaml and 2) much more of a 'production' implementation than an expository one. I found it very difficult to reconcile it with the formal description in the chapter. Hence I've tried to stay as close as possible to the algorithm as described in the book. In 'step' mode each move of the algorithm is displayed, along with the state of the stack. The name of each rule is printed as it is invoked. I've included a simple lisp-based front end, a stubbed version of the front end of my Irken compiler: http://www.nightmare.com/rushing/irken/ The input syntax is Scheme-like. So for example the identity function is "(lambda (x) x)". To run a self test: $ python solver.py -t To enter expressions interactively: $ python solver.py -i Enjoy, and please contact me with suggestions/corrections/etc: http://www.nightmare.com/~rushing/ Thanks to François Pottier and Yann Régis-Gianas for assistance.