It's a bit more than that in Haskell (and I guess Idris, but never tried). In Haskell you can write 'undefined' in any definition. 'undefined' is of any type, s

It's a bit more than that in Haskell (and I guess Idris, but never tried). In Haskell you can write 'undefined' in any definition. 'undefined' is of any type, so the code will type-check. Then you can write a high-level sketch of your program, including functions, purely based on types and 'undefined'. When you are satisfied playing the types puzzle, you proceed to write implementations. This is referred to as "hole-driven programming" or "type hole-driven programming". Also, like the other guy mentioned, the types lend themselves very well to auto-completion. It's no coincidence than in Hoogle, you can often find a function by its type. E.g., what could "[a] -> [b] -> [(a,b)]" possibly do? https://hoogle.haskell.org/ https://hoogle.haskell.org/