Types for checking things are correct is really important which is what this talks about.

For me though they really come into their own when those types then help to eliminate boilerplate. Haskell's foldMap function is my classic example of handling the accumulation of a result where it does the hard work based on the types. Idris goes even further by supporting the ability to infer obvious code for your code editor like handling each case in a sum type.