4 ms·
I've been really enamored of bidirectional type systems [0] lately, which seem to really give the best of all worlds. They explicitly separate inference from ty
by cultus 6y ago
I've been really enamored of bidirectional type systems [0] lately, which seem to really give the best of all worlds. They explicitly separate inference from type checking, with the type checker switching between both modes during checking/inference. It's also more syntax directed, which makes good error messages easy.
A pure HM type-system is pretty restrictive, so most ML family languages don't have global type inference anyway.
[0] https://arxiv.org/pdf/1908.05839.pdf https://arxiv.org/pdf/1908.05839.pdf
- shpongled 6y agoYea bidirectional systems are nice - one of the big benefits is that you can also have polymorphic function arguments, something you can't do in standard HM. I recently implemented the bidirectional system in Rust from the paper you linked, it was fun (and a challenge!) [0] https://bit.ly/2W96K2r https://bit.ly/2W96K2r
- cultus 6y agoWow! Very cool!