> type annotations are not (always) just typechecker-hints, but can be explicit documentation of intent More than this, in highly expressive type systems such

> type annotations are not (always) just typechecker-hints, but can be explicit documentation of intent More than this, in highly expressive type systems such as Haskell's, they can carry proofs. This can be useful for constraining the capabilities of effects (ie: we can state that a particular function has the ability to make a network request but cannot open files) as well as assisting us in writing the correct implementation by construction. As an author of a type-level library it's also highly useful for generating code from arbitrary types that is also correct by construction and deriving obvious implementations so we have to write less code. Haskell's type system may soon be able to check for usage as well by encoding linearity into the type system. This will enable to tell the type checker that a function which has a resource must use it at least once. Without explicitly sequencing our nice, pure code the compiler can ensure that linearity is preserved. Idris 2 is experimenting with this as well. It seems like a pretty good idea. And all of this type level stuff is so useful that we want to do more of it. Dependently typed languages remove the separation between the type language and the language of terms. This is powerful stuff.