Dependent Nuggets
Introductions to the building blocks of dependently typed programs.
The posts in this series are 'living posts', they will be referenced as library modules by future posts, and will be updated as needs change.
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.
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.
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.
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.