I wrote a little post about the typechecking algorithm I devised for SaberVM, a typed stack-based bytecode language like Web Assembly, designed from the ground up for being the target of functional programming languages