On 30/01/2026 20:18, Duke Normandin wrote:
It can be a culture shock coming from languages that require many more type annotations.
Thankfully, it seems to me that using type inference can be by-passed most of the time. I'd hate to have to come back to my code 6 mos down the round and wonder what was *inferred* in the code. Commenting the code and/or using more type annotation - finding a suitable balance!
No, you can't bypass the best of the culture.
It is a fine art to write just the right type constraints in the source text --- not to much, not too little --- both for readability, maintainability, robustness of compilation.
This is another opportunity to try our fine IDE for Poly/ML and Isabelle/ML https://isabelle.in.tum.de --- it provides control-hover-mouse tooltips for types inferred by the ML compiler, and many more things.
It also highlights scopes of defined entities, as you have been asking before on this list.
Makarius