FreshLists skeleton

db/posts/7.json

@@ -0,0 +1,16 @@
+{
+  "edited-at": [
+  ],
+  "hidden": false,
+  "idris": true,
+  "ipkg": "/home/nathan/Projects/Blog/projects/Idris/Idris.ipkg",
+  "posted-at": "2025-03-15T18:07:00.649227-04:00",
+  "slugs": [
+  ],
+  "source": "/home/nathan/Projects/Blog/projects/Idris/src/DependentNuggets/FreshLists.md",
+  "source-code": "https://git.stranger.systems/thatonelutenist/website/src/branch/trunk/projects/Idris/src/DependentNuggets/FreshLists.md",
+  "special": false,
+  "tags": [
+    "idris"
+  ]
+}

db/series/1.json

@@ -0,0 +1,7 @@
+{
+  "desc": "Introductions to the building blocks of dependently typed programs.",
+  "post-ids": [
+    7
+  ],
+  "title": "Dependent Nuggets"
+}

projects/Idris/Idris.ipkg

@@ -19,6 +19,7 @@ authors = "Nathan McCarty"
 modules = Idris
         , Posts.HelloWorld
         , LessMacrosMoreTypes.Printf
+        , DependentNuggets.FreshLists
 
 -- main file (i.e. file to load at REPL)
 -- main =

projects/Idris/src/DependentNuggets/FreshLists.md

@@ -0,0 +1,8 @@
+# FreshLists: Containers That Only Accept "Fresh" Elements
+
+```idris hide
+module DependentNuggets.FreshLists
+```
+
+When programming, we quite frequently encounter the for a data structure that can contain at most one of each given element. Typically, we would use a `Set`, which satisfies this constraint, but does so as a runtime invariant that must be taken on trust, and results in ergonomic concerns when used as a component of API design.
+