Agreed, Koka has great documentation, although I will acknowledge that it is incomplete. The papers are suprisingly approachable with good user applicable examples and motivation before they get too deep into type theory etc. I recommend reading a few of the more recent ones, which have mind blowing implications.
Amazing stuff -- thank you for sharing these papers.
The implications for things like data science frameworks and spreadsheets are particularly interesting. Perhaps we are within reach of a much more equational approach to programming with high performance.