I haven't looked too closely at Idris, I'll have to read this. Thanks for pointing me at it as I've been thinking about language design a lot lately (though I have no ideas that would warrant actually implementing a programming language currently).

if i may suggest, as we seem probably similarly thoughtful about language design, and having been a Scheme person long ago, Python of course, optimizing compilers galore, etc. ... I find F# very neat, as it's essentially a Microsoft .Net runtime Ocaml, and is therefore (not syntactically, but semantically) reminiscent of Scheme/Lisp.

I am in fact dabbling in f# of late haha (My day job life is C# and f# does a lot of things well). I just never seem able to only mess with one thing so I'm also doing CL.

we are evidently clones

Haha.

Out of curiosity have you seen the youtube channel Fast f#? He's doing a good job of talking about f# at several levels from simple to deep optimization work.

haven't seen that; thanks for the reference. i've been using the Microsoft dev docs, and fsharpforfunandprofit ... (and just situational awareness from an optimizing compilers background)