3 ms·
That's why you go with bidirectional type checking instead. This scales much better to more interesting language constructs like rank-n polymorphism, and depend
by bjz_ 8y ago
That's why you go with bidirectional type checking instead. This scales much better to more interesting language constructs like rank-n polymorphism, and dependent types, gives better localised error messages, and the downside of having to have some top level annotations is worth it, because that's best practice anyway.
- YorkshireSeason 8y agoBidirectional is a nice, pragmatic compromise, but it is a reaction to the difficulty with taking full type inference beyond let-polymorphism. We wouldn't be using bidirectional, if Damas-Hindley-Milner would scale.
- bjz_ 8y agoI dunno, I do prefer having type directed editing (eg. auto case splitting, and autocomplete), so full type inference is less of a holy grail to me. Damas-Hindley-Milner inference is also hyper-optimised to a specific point on the design space, and does an excellent job there, but (to echo Conor McBride) I would love to see less conflation of the ideas of execution phase, parametericity, and implicitness going forward.
- YorkshireSeason 8y agoless conflation of That's interesting. But I'm not sure what you mean. Would you be able to explain this more, or point me to something I can read on this?