> You can create a bidir system that never requires annotations and uses unification to infer all types in the style of Haskell or OCaml. There is no more bidi

> You can create a bidir system that never requires annotations and uses unification to infer all types in the style of Haskell or OCaml. There is no more bidir if you do that. It's just plain unification. > In some sense I think HM == unification because you can't really implement HM without unification. The first time a type variable encounters another type you'd be stuck. You can't implement HM without unification but you can do unification which is not HM. Actually a lot of what people call HM is not really HM but evolution of it and sometimes significant evolution.