I recently implemented a Hindley Milner type checker. The algorithm itself is not necessarily super difficult (once you get your head around it ofcourse) but the way it is explained is. It seems like HM is mostly explained by people with a mathematics background that already know the proper notation. I wonder how much overlap there is between people that know the notation and do not know how HM works, probably not much.

Anyway nice demo. Bi-directional is already quite powerful!