# Hindley-Milner: How do I separate constraint generation and unification phases in Algorithm W when inferring types of patterns?

I am self-teaching myself Hindley-Milner type inference by writing my own implementation, separating tree traversal and constraint solving. The tutorials that I've been following only allow patterns that are variables, but I decided to implement pattern matching, and I've hit a wall concerning the separation of traversal and unification when inferring the pattern types.

My tree traversal phase maintains an "environment," a mapping of identifiers to polytypes. Patterns can introduce new bindings into the environment.

Given a let expression let id = expr in body, the tutorials that I follow compute id's polytype by generalizing expr's type with the current typing context, quantifying over all tvars not defined in the environment.

However, if non-identifier patterns are allowed, unification must be done in order to give identifiers in the pattern type schemes. For example, given

let (a, b) = foo in
body


, assigning a the tvar t0, b the tvar t1, and foo some monotype t3, t3 must be unified with (t0, t1) in order to give a and b the correct monotypes to generalize, at least to my understanding. Is it possible to me to separate constraint collection and unification when supporting patterns in my language, and if so, how? Thank you in advance!

For context, I am a high-school student not formally educated in computer science.

• Have you come with an answer? I'm in the same process; although I graduated years ago, but never took Type Theory classes. I'm currently studying the chapter 10 of Advanced Topics in Types and Programming Languages. You may find it online: gallium.inria.fr/~fpottier/publis/emlti-final.pdf – manu Jan 15 '19 at 16:37
• @manu My main confusion was about how to handle patterns when performing type inference, because the Hindley-Milner tutorials I read only covered let bindings with names on the left. I tested out OCaml and Haskell and to my surprise, they have different generalization semantics. OCaml generalizes in match expressions; Haskell does not generalize in case expressions. In my own type inferencer, I wrote a function that walks patterns and creates constraints the same way that one walks expressions and creates constraints. The function returns a map of identifiers to types. Then, I... – Types Logics Cats Jan 16 '19 at 20:53
• generalize those types and add the bindings to the typing context. See gitlab.com/emelle/emelle/blob/master/src/typing/typecheck.ml; the relevant functions are infer_pattern, infer_expr (see the Term.Case case), and infer_branch. Posting my comment, I realize that my code could be more readable, so let me know if anything is confusing. Note that in my type inferencer, I immediately solve type variables instead of collecting constraints. – Types Logics Cats Jan 16 '19 at 20:57
• Pattern matching, for type checking requires some sort of rewriting. The book by Simon Peyton Jones 'The implementation of functional programming languages' is a good starting point. Chapter 9 contains an ML implementation of HM type checker (unification based). Chapter 6 by Philip Wadler is about Pattern Matching. My about Patterns and type checking are in github.com/merchise/xotl.fl/blob/master/docs/source/drafts/… – manu Jan 16 '19 at 23:22
• Notice that I use "compile" to actually mean syntactical transformation. – manu Jan 16 '19 at 23:27