I understand that Hindley-Milner Type Inference can be implemented using an off-the-shelf SMT (Satisfiability Modulo Theories) solver?

How would this work, for example for a very simple type system (just primitive base types and function types, no polymorphism, no subtyping, no nuthin')?

  • 2
    $\begingroup$ You can think of type inference as a unification problem. If your SMT solver can do unification, that's pretty much it. There isn't any logic involved, just a bunch of equations. $\endgroup$ Dec 26, 2016 at 20:51
  • 5
    $\begingroup$ Could people who are downvoting this please explain their downvotes? I realize this is probably not research-level, but an explanation would still be nice, thanks. $\endgroup$ Dec 26, 2016 at 22:57
  • $\begingroup$ FWIW, I my opinion "no polymorphism" means "not Hindley-Milner", since the key element of HM is how to automatically introduce (and eliminate) polymorphism. $\endgroup$
    – Stefan
    Jan 3, 2017 at 16:48
  • 1
    $\begingroup$ I found a recent paper describing type inference for Python 3 using an SMT solver. $\endgroup$ Dec 17, 2020 at 19:21


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.