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.

(From microsoft.com/en-us/research/w)

Doing various optimisations/transformations on the Idris 2 code generator.

As far as I can tell, Chez Scheme's response is typically "Thanks for the advice, but I was already doing that".

"If you don't know Haskell, it's like Idris, but with less fancy types" - @chrismarkbrown

(And with colons in the wrong place :))

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 :).

Show thread

I've been bad at promoting this, but we're doing lots of Idris hacking this week... github.com/idris-lang/Idris2/w

Looking forward to seeing what comes of it!

I've had a deadline extended from Saturday lunchtime to Sunday lunchtime (okay, Friday AoE to Saturday AoE).

While helpful, sometimes I wonder if any academics are interested in weekends...

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...

Show thread

Here's a non-answer: There aren't smileys in error messages. I'm not a monster!

Show thread

Well this has horrified people about as much as I expected. I'll leave you to speculate for a bit...

Show thread

Useless fact: there are 896404 open parentheses in the generated scheme from Idris 2, and 896419 closing parentheses.

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.

Show thread

I woke up to the news that my ECOOP submission "Idris 2: Quantitative Type Theory in Practice" was accepted. Hooray! Here's the draft: type-driven.org.uk/edwinb/idri

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.

Between 5pm on Friday and 9am on Monday, I've had an invitation to review for a journal, and a reminder that I haven't responded to said invitation.

I can only hope that this is automated and the computer forgot that humans take the weekend off.

Okay, maybe not completely properly, but the User Guide still made you believe you had a fighting chance.

Show thread

Got some new laptop stickers, to reflect the last time I felt I properly understood some technology.

I have just Fed The Fish. The Fish seems to be happy. UK academics will understand...

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 :).

Show thread

"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.)

Show thread
Show older

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!