Brady has a presentation about Idris where he shows Type-Driven development (where you write code that could typecheck with some holes and you get the compiler to help you figure out the missing types for your "whatever/something" untyped variables)

https://youtu.be/X36ye-1x_HQ?t=5m15s

Suppose you declare some:

const transformFoo: (foos: Foo[]) => Bar

and you start implementing it and get stuck with some callback or whatever you can put a `hole` and it will tell you the type signature of what you're missing.