Earlier quoted context omitted.
What I’m suggesting is that you could literally just run HM or another typechecker at runtime. You’d give an empty list the type “list ” for a fresh type variable T; appending an integer would introduce the constraint T = int; appending a string would introduce T = string and raise a runtime error. (Or not—it’s up to the typechecker if it wants to degrade to “int|string” or something.)
At runtime, the original program (i.e., the syntax tree, or some other representation from which the syntax tree is recoverable) may well not exist anymore. If you don't have a syntax tree, you can't type-check anything. Now, you may say “okay, the original program doesn't exist anymore, but my language implementation is a term rewriting engine, so I have a current program that I can submit to the type checker”. Alas…
Re: Where Do Type Systems Come From?
#171Who says you need a syntax tree? You just store a byte of metadata next to each variable with the type. There should be more than enough data from that to recover the parts that you can't store like that and do type inference on them.