Constraint solving over a complete lattice.

I'm quite pleased with the progress I've made today on the implementation of InforML. I finally put wrote the code to provide a lattice »model« for the little theorem prover over lattice constraints that is used by the type inference algorithm. Below is a sample session with InforML, making use of the #sublabel meta-declarations. It also shows off InforML's support for UTF-8. I could have also used UTF-8 versions of some of the notation in the input, but I was interacting with InforML via a terminal, rather than an emacs buffer, so it was easier to type the ASCII equivalents.

  1. InforML 0.7 $Id: informl.sml 1576$
  2. [Loading standard libraries]
  3. [Finished loading standard libraries]
  4. % #sublabel Bot, Top;
  5. ⊥ <: ⊤
  6. % #sublabel Top, Bot;
  7. ⊤ < / : ⊥
  8. % newlabel L;
  9. newlabel L
  10. % newlabel Foo where Foo <: (L || Top);
  11. newlabel Foo where Foo <: (L ⊔ ⊤)
  12. % #sublabel L, Foo;
  13. L < / : Foo
  14. % #sublabel Foo, L;
  15. Foo < / : L
  16. % #sublabel Foo, Top;
  17. Foo <: ⊤
  18. % #sublabel Foo, (L || Top);
  19. Foo <: (L ⊔ ⊤)
  20. % newlabel Testing where Testing <: Bot
  21. and Testing :> Top;
  22. Lattice model has become inconsistent!
  23. %

At this point I am quite optimistic about getting a rough version of type inference completed this week. Some of the stuff with regards to modules and signatures could prove tricky, but the rest of it is pretty much transliterating the inference rules I have typeset.

Leave a Comment