When to annotate type

타입 추론이 충분히 잘되는 정적 타입 언어에서는 타입을 상당 부분 생략할 수 있다. 언제 타입을 명시하고 언제 타입을 생략하는 게 좋을까?

Lean

타입을 필요 이하로 명시하기보다는 필요 이상으로 명시하는 편이 낫다는 견해. 아마도 Lean은 증명 언어이고 타입 시스템이 특히 복잡(Dependent type)하기 때문인 것 같다.

Generally speaking, it is a good idea to err on the side of too many, rather than too few, type annotations. First off, explicit types communicate assumptions about the code to readers. Even if Lean can determine the type on its own, it can still be easier to read code without having to repeatedly query Lean for type information. Secondly, explicit types help localize errors. The more explicit a program is about its types, the more informative the error messages can be. This is especially important in a language like Lean that has a very expressive type system. Thirdly, explicit types make it easier to write the program in the first place. The type is a specification, and the compiler’s feedback can be a helpful tool in writing a program that meets the specification. Finally, Lean’s type inference is a best-effort system. Because Lean’s type system is so expressive, there is no “best” or most general type to find for all expressions. This means that even if you get a type, there’s no guarantee that it’s the right type for a given application.