get the fuck out of here with your kike scam type theory sophistry
Name:
Mr. Irrational2013-12-05 16:59
Type inference, as implemented in e.g. OCaml and Haskell is a unification algorithm.
Practically speaking, most programmers might remember unification from that incomplete Prolog they implemented while at university.
The other big deal in typing is dependent types. This is just applying a proof assistant (i.e. some or other evolution of the 1959 General Problem Solver by Simon, Shaw and Newell) to static type analysis in a programming language.
Funnily enough, two famous dependently typed languages are Coq and Agda, which are also proof asssistants.
I have no idea why there is a million papers a minute from instutitions world wide about these two simple ideas, and why they seem to be so high profile at e.g. various conferences. I think it is one of the biggest farces of our time, especially since as little back as the 90s there were more serious efforts at e.g. bringing unification to hardware.