Tags

Near the start of january, after bumping into some ecosystem issues and lack of a personal support library while working on the 2024 Advent in Idris, I started working on a project to solve all of the Advent of Code problems from all the years in a single massive entirely literate Idris project and publish it as an mdbook. I'm calling it Idris example.

This might get me some looks, but I have pretty solidly decided to go in on using XChaCha20+Blake3 as the AE of choice for my future open source work. There are numerous reasons for this decision, but it mainly comes down to the desire for defense in depth, and a deep dislike of fundamental properties of polynomial MACs.

This is going to sound really odd, especially if you have have some passing familiarly with Idris, but Idris doesn't actually have generics. Sure, it has something that looks like generics, and can do everything generics can do, but it isn't actually generics, at least not in terms of the usual conceptual framework programmers have for generics. What Idris actually has is something more fundamental, in a sense simpler than generics, yet infinitely more flexible.

For performance reasons, we sometimes find ourselves implementing the interface of a more basic structure in terms of a much more complicated one. In functional programming languages, this often comes up in the context of needing to build a structure through mutation and then "seal" it for further processing as an immutable object. While this often comes with great performance gains, the encapsulation needed to hide the internal mutability or unsaftey, or even the nature of the interior mutability itself, can deprive us of the ability to meaningfully pattern match on the results. Views and dependent pattern matching can overcome this limitation by allowing us to redefine the notion of pattern matching for a type.

Sometimes, especially when dealing with business logic, we have to deal with data that comes in from the real world, or elsewhere, naturally very messily typed, leading to nasty type signatures and messes of macros or code generation to build data structures from a schema. Row polymorphism can help us by abstracting over the fields contained in a record type in the type signature, letting us define records based on data, concatenate records together, and define functions that are generic across any record containing the required fields, all without macros.

When designing interfaces, you may occasionally find a need to thread a proof of non-equality through API, and for ergonomics reasons, you would like that proof to be an auto implicit so the user doesn't have to generate the proof manually. Often, these proofs seem like they really should be trivial for the compiler to generate, but proof search will adamantly refuse to do so.

Due to a number of factors, including the uncertain future of the .io TLD, its growing negative connotations, and my development focus switching to lil baby languages like Idris, I've found myself in need of a new blog. I've been using Raku lately for personal tooling projects, and decided to go full gremlin mode and write a hack together a cursed static site generator in it.

Due to a number of factors, including the uncertain future of the .io TLD, its growing negative connotations, and my development focus switching to lil baby languages like Idris, I've found myself in need of a new blog. I've been using Raku lately for personal tooling projects, and decided to go full gremlin mode and write a hack together a cursed static site generator in it.

When designing interfaces, you may occasionally find a need to thread a proof of non-equality through API, and for ergonomics reasons, you would like that proof to be an auto implicit so the user doesn't have to generate the proof manually. Often, these proofs seem like they really should be trivial for the compiler to generate, but proof search will adamantly refuse to do so.