search

inc-lc / ilc-scala

Scala implementation of ILC, with benchmarks
http://inc-lc.github.io/
Other
25 stars 0 forks source link

Type inference for open terms / principal typings #15

Closed Blaisorblade closed 9 years ago

Blaisorblade commented 9 years ago

For type inference, the environment can be an input or an output. Having it as output allows producing principal typings, and doing type inference on open terms. The need for open terms came up in testcases, but makes general sense. The most compelling application of principal typings is separate compilation (as I learned checking out a comment from Paul Phillips).

Blaisorblade commented 9 years ago

So, it turns out that I had already run into a principal typing algorithm at the time of starting the project. I and @yfcai had noticed that presentations of type inference for STLC have the environment as either input or output, but we missed the significance of that.

See this presentation by Peter Thiemann & Manuel Geffken for an algorithm — which is however not really constraint-based, since it does not separate constraint collection from type inference.

https://proglang.informatik.uni-freiburg.de/teaching/compilerbau/2012ws/17-simply-typed.pdf

Blaisorblade commented 9 years ago

This seems done. The only non-obvious bit is removing identifiers from contexts for all binders — not only it seems easy to forget, but while this is dual to adding identifiers in contexts when inferring principal types*, the two duals take different effort to unit-test. For instance, we had zero test failures because of the bug fixed in e17f648382b3a511613019ec03d84cd97e3da16a, until I wrote a specific test after spotting the bug.

*EDIT: This change is needed because usually context flow inwards (from binders, which extend contexts with bindings, to users, which use bindings), while for principal typings (and whenever handling free variables) they flow outwards (from users, which extend contexts with bindings, to binders, which must remove bindings from contexts — so there's even more work to do).

Blaisorblade commented 9 years ago

Forgot to note: performance seem to get slightly worse with this inference (in fact, the biggest regression seems due to switching from Lists to Maps).

Blaisorblade commented 9 years ago

Fixed by #18, closing.