I accidentally discovered a bug in the Idris2 codegen. Let's explore how to narrow it down, and hopefully fix it.
Tue, 25 Apr 2023
What do you do if you need a pseudorandom number generator but don't know anything about how to implement that and, crucially, don't care how good it is? You _could_ read some papers, but ChatGPT had been making waves for a while, so why not try that?
Thu, 16 Mar 2023
As part of my Ph.D. exploration on how we know the types we're using model what we think they do, I decided to try to implement a constraint solver in Idris (technically Idris2, but Idris1 is deprecated at this point, so I use 'Idris' and 'Idris2' interchangeably).
Thu, 16 Feb 2023
The best way to learn & understand a thing is to implement it. So let's implement (a subset) of Idris2! This part is an introduction and covers some function exercises that will help later.
Fri, 2 Sep 2022
Intro This is yoinked from an answer I gave on the Idris2 discord where someone was confused about using IO when there was multiple functions involved. I’ve slightly restructured it, but it’s still basically the Discord answer verbatim.
Fri, 25 Mar 2022
One of the more difficult concepts in Idris, I've found, is proving things through dependent types. The 'simplest' introduction to this is probably the `DecEq` interface, which this post aims to introduce, explain, and implement.
Tue, 15 Mar 2022
Explaining and implementing Birell's 2003 paper on Condition Variables for Modula-2+, in Racket.
Tue, 27 Jul 2021
A dive into functional concurrency, FFIs, and thread weirdness.
Wed, 24 Feb 2021