Je vais à Paris en février, je m'excuse d'avance.

Parce que nos passeports seront bleus, c'est très important!

(pardon my French...)

This came in the post today. I'll wear it while it's true, and until it's true again.

I don't usually tweet about football, because my team usually lose, but... Wow. Usually this goes the other way... bbc.co.uk/sport/football/51101

If you're interested: The concept being "detaggability" of constructors, and the problem being how to know whether an argument is erasable even if we're pattern matching on it.

I've just solved a problem using a concept from my thesis that I rejected as useless at least 10 years ago. So that's nice...

A matching pen and pencil! Just the thing I need, how nice!

I've just entered the Skye Go tournament. I don't play Go nearly often enough these days, but when I do, it is in the middle (or in this case on the edge) of nowhere! britgo.org/tournaments/2020/sk

I've just had to restart my battery charge monitor because it was taking up 2Gb RAM and stopping me being able to build Idris 2... (which is currently at 2.7Gb)

I suppose, in a sense, it's true - Idris 2 the language combines lots of things that exist already. I don't want to invent any new features.

The goal, now, is to make fancy type level programming (which we know is capable of so much good stuff) more widely accessible.

I looked at reddit and found out Idris 2 has all been done before. So that'll save me some time.

Just procrastinated so hard I set up a blog and wrote about linearity and erasure in Idris 2. type-driven.org.uk/edwinb/line

I'm probably not going to make a habit of this...

Combining exceptions and linear types turns out to be achievable too. As long as: a) App is parameterised over whether a code fragment can throw; b) I've implemented the type checker competently... github.com/edwinb/IdrisApp/blo

Which is also efficient enough, easy enough to use, and a reasonable way to combine external libraries.

This seems to be getting closer, at least...

It's so tempting to write libraries that can do All The Things, but really I just want something a bit like an IO monad in Haskell but with the ability to easily add exceptions and internal state.

Maybe I should keep staring at it and wish very hard. What could possibly go wrong?

I've been on a break for the last fortnight, in which I've been variously eating too much, and hacking in Idris 2 (which turned out to be fun, so I'm sure it's allowed).

Not sure why the big pile of exam scripts hasn't marked itself though...

Show more
Mastodon

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!