When to annotate type

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

명시된 타입의 용도

명시된 타입은 1) 의도를 드러내고, 2) 실수를 방지하는 역할을 하며, 3) 프로그램 작성 과정을 돕는 역할을 한다(Type-driven development).

“의도를 드러내기”라는 측면은 인간에게도 중요하고 타입 검사기에게도 중요한데, 의도를 적절히 드러내면 타입 검사기가 좀 더 유용한 타입 오류를 보여주기도 한다. AI 지원 프로그래밍을 생각하면 “드러난 의도”를 읽는 독자(AI)가 하나 더 늘어난다.

일반적인 지침

보통은 공용(public) 인터페이스 경계에 타입을 명시하라는 지침이 가장 일반적인 것 같다.

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.¹

Footnotes

1. ToDo 출처 찾아서 넣기 ↩