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.