@vitaut The Little Typer is a slower intro but good (in the style of The Little Schemer). There's also Type Driven Development with Idris which I haven't read but I'm sure is good because Edwin was my advisor in undergrad.

- https://thelittletyper.com/
- https://www.manning.com/books/type-driven-development-with-idris

Resurrecting my favourite pull quote from… actually I lost the source a long time ago. Still true though.

i had an utterly deranged compiler idea but i forgot it already :(