"Idris: Practical Dependent Types with Practical Examples" by Brian McKenna