fuckhole CS neckbeards shitting up my maths

get the fuck out of here with your kike scam type theory sophistry

butts

seven hundred butts

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.

>>4
New ideas require thought and patience; there's no time for that in the go go go world of academia. The computer language theory philosophers of our time can only get hard if there's a new twist on a type system that advances the impracticality of the state of the art. Furthermore, there must be a few proofs about the type system involving a page of inference rules because that's the only way to rigorously get off. Anything else is more appropriate for other venues. Sorry-- Strong Reject.