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.