Idris 2 is self-hosting, faster, compiles to Chez Scheme, and has a bunch of PL design lessons!
miniblog.
Related Posts
Using Idris' C FFI to do compile time type generation! https://docs.idris-lang.org/en/latest/guides/type-providers-ffi.html
(Lovely clear example.)
Lovely talk on type driven development in Idris 2, largely a live demo!
https://youtu.be/mOtKD7ml0NU
10 things Idris improved over Haskell
https://deque.blog/2017/06/14/10-things-idris-improved-over-haskell/
(good discussion of Haskell design flaws that Idris has tackled)
