This looks really good and complete. And I like that it starts from normal programming stuff rather than immediately jumping into type universes and proof expressions.

Edit: some feedback on the monads page:

1. "The bind operation (written >>=) is the heart of the monad." .. but then it doesn't use >>= at all in the code example.

2. "The left arrow ← desugars to bind; the semicolon sequences operations." .. again, no semicolons in the code example.

3. I don't really understand the List Monad section. The example doesn't seem to use any monad interfaces.

4. "The same laws look cleaner in the Kleisli category, where we compose monadic functions directly. If f:A→MB and g:B→MC, their Kleisli composition is g∘f:A→MC" - it was going so well!