# When to annotate type

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

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

## 명시된 타입의 용도

명시된 타입은 1) 의도를 드러내고, 2) 실수를 방지하는 역할을 하며, 3) 프로그램 작성 과정을 돕는 역할을 한다([Type-driven development](https://wiki.g15e.com/pages/Type-driven%20development.txt)).

"의도를 드러내기"라는 측면은 인간에게도 중요하고 타입 검사기에게도 중요한데, 의도를 적절히 드러내면 타입 검사기가 좀 더 유용한 타입 오류를 보여주기도 한다. [AI 지원 프로그래밍](https://wiki.g15e.com/pages/AI-aided%20programming.txt)을 생각하면 "드러난 의도"를 읽는 독자(AI)가 하나 더 늘어난다.

## 일반적인 지침

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

## [Lean](https://wiki.g15e.com/pages/Lean%20(programming%20language.txt))

타입을 필요 이하로 명시하기보다는 필요 이상으로 명시하는 편이 낫다는 견해. 아마도 [Lean](https://wiki.g15e.com/pages/Lean%20(programming%20language.txt))은 증명 언어이고 타입 시스템이 특히 복잡하기 때문(<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.[^1]

## Footnotes

[^1]: <ToDo> 출처 찾아서 넣기