Recent Posts

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.

When programming, we quite frequently encounter the need for a data structure that can contain at most one of each given element. Typically, we might use a Set, which satisfies this constraint, but does so as a runtime invariant, which must be taken on trust, and results in ergonomic concerns when used as a component of API design. We introduce "Fresh Lists" as an alternative that provide a type-level guarantee of the uniqueness of each element, while also generalizing the notion of uniqueness and providing compile-time checking of literals.

While C can provide "convenient" string formatting by having hideously unsafe variadics, and dynamic languages, like python, can do the same, many type safe languages, such as Rust, are forced to provide such functionality through the use of a macro. Dependently typed languages, like Idris, can provide a printf like formatting interface, while maintaining both memory and type safety, without the need for macros. We will explore this by implementing a simplified version of printf in Idris from scratch.

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.