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

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

CC BY-SA 3.0
2016-12-26T20:51:14.087Z
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.
Andrej Bauer
CC BY-SA 3.0
2016-12-26T22:57:31.397Z
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.
Andrej Bauer
CC BY-SA 3.0
2017-01-03T16:48:52.723Z
FWIW, I my opinion "no polymorphism" means "not Hindley-Milner", since the key element of HM is how to automatically introduce (and eliminate) polymorphism.
Stefan
CC BY-SA 4.0
2020-12-17T19:21:51.833Z
I found [a recent paper](https://www.ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Mostafa_Hassan_BA_report.pdf) describing type inference for Python 3 using an SMT solver.
Anderson Green
<sat><type-theory>
How to do Type Inference using an SMT solver?
n00b101
# How to do Type Inference using an SMT solver?

(Asked by: username_0 on 2016-12-26)

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

**Tags:** sat, type-theory

> **Comments:**
> **username_1**: 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.  
> **username_1**: 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.  
> **username_2**: FWIW, I my opinion "no polymorphism" means "not Hindley-Milner", since the key element of HM is how to automatically introduce (and eliminate) polymorphism.  
> **username_3**: I found [a recent paper](https://www.ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Mostafa_Hassan_BA_report.pdf) describing type inference for Python 3 using an SMT solver.  

---

## 0 answers

