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')?

  • 1
    $\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 '16 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 '16 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 '17 at 16:48
  • $\begingroup$ I found a recent paper describing type inference for Python 3 using an SMT solver. $\endgroup$ Dec 17 '20 at 19:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.