Oops. On the plus side, I just implemented a thing that GHC has been doing for about 25 years and got a small performance gain.
So far I've seen some beautiful semantic highlighting in the emacs mode, and something close to web documentation generation.
For my part, I've written two lines of code and the typechecker has written 14 for me. At least everyone else is productive :).
I've been bad at promoting this, but we're doing lots of Idris hacking this week... https://github.com/idris-lang/Idris2/wiki/Idris-Developers-Meeting,-April-2021
Looking forward to seeing what comes of it!
The explanation even turns out to be slightly interesting (!).
Lots of things in the concrete syntax start with an open bracket, so the parser only does that once then branches...
Here's a non-answer: There aren't smileys in error messages. I'm not a monster!
Well this has horrified people about as much as I expected. I'll leave you to speculate for a bit...
If you're wondering: yes, I do find it hilarious that the first Idris 2 paper will appear in a (formerly) OO conference, and that I got the notification on April Fools Day.
I woke up to the news that my ECOOP submission "Idris 2: Quantitative Type Theory in Practice" was accepted. Hooray! Here's the draft: https://www.type-driven.org.uk/edwinb/idris-2-quantitative-type-theory-in-practice.html
Apparently I collect prints of old railway posters now. I've just put this up in my spare room to mess with visitors, should I ever be allowed to have any. #beseeingyou
Okay, maybe not completely properly, but the User Guide still made you believe you had a fighting chance.
I loved this programme when I was little (okay, I was a bit of a strange child, but you probably knew that already). I might show this to my students next year so they know how I learned to program :).
"Some genius has programmed it so I don't have to type every word, I wish all programming was done like this"
Yes! Me too! Come to 2021, we're getting there! (But please wear a mask and wash your hands - I'll explain when you get here.)
CS Lecturer at University of St Andrews. Idris hacker, programming language researcher and developer. He/him.
Server run by the main developers of the project It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!