WingNews logo WingNews
top | item 47071688

(no title)

rixed | 11 days ago

Last time I had to implement a typed programming language, it was for short programs only. So for typing I just converted the program into a large set of constraints and throw z4 at it, asking to optimize for smallest possible types. If z4 could find types for every expressions in less than a few seconds then it was well typed.

You had to use a few trick for larger programs, but basically it managed to type any real programs and I never encountered an ambihuous case that caused a problem in practice. In case of failure, the small set of unsatisfiable constraints was easy to translate into nice error messages. This also allows for typing rules that are easy to state and can accomodate operators that adapts nicely to their environment.

I would understand if this approach would be frowned upon, but I still wonder if any serious language ever used this approach?

discuss

order

RobertoG|11 days ago

damn, now I would like to know what you were really answering to.

gravifer|11 days ago

probably under a wrong thread, but can you point me to the one you intended? Really curious about that

rixed|10 days ago

Haha, I've often wondered how one could answer to the wrong thread on HN, and there I am :)

Was intended for https://news.ycombinator.com/item?id=47025885

And z4 is, of course z3 (no I don't have special access to next-gen version of z3)