From e00ec274ca2a8c0cbcafebae421aaf41e086641d Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 27 Jan 2025 19:47:47 -0500
Subject: [PATCH] Year 2015 Day 12 Part 1

---
 README.md                |  4 ++
 src/SUMMARY.md           |  1 +
 src/Years/Y2015.md       |  7 +++
 src/Years/Y2015/Day12.md | 99 ++++++++++++++++++++++++++++++++++++++++
 4 files changed, 111 insertions(+)
 create mode 100644 src/Years/Y2015/Day12.md

diff --git a/README.md b/README.md
index 1598931..731d675 100644
--- a/README.md
+++ b/README.md
@@ -128,6 +128,10 @@ solution.
 
     Introduces refinement types
 
+  - [Day 12](src/Years/Y2015/Day12.md)
+
+    New Parser Effect stack and DLists
+
 ## References
 
 [^1]: Idris 2 Manual:
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 2cf1e0b..f0b09eb 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -33,3 +33,4 @@
   - [Day 9 - Naive Graph Traversal](Years/Y2015/Day9.md)
   - [Day 10 - Digits View](Years/Y2015/Day10.md)
   - [Day 11 - Refinement Types](Years/Y2015/Day11.md)
+  - [Day 12 - Custom Parser Effect and DLists](Years/Y2015/Day12.md)
diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md
index c2a0326..8f94f4f 100644
--- a/src/Years/Y2015.md
+++ b/src/Years/Y2015.md
@@ -18,6 +18,7 @@ import Years.Y2015.Day8
 import Years.Y2015.Day9
 import Years.Y2015.Day10
 import Years.Y2015.Day11
+import Years.Y2015.Day12
 ```
 
 # Days
@@ -94,6 +95,12 @@ y2015 = MkYear 2015 [
   , day11
 ```
 
+## [Day 12](Y2015/Day12.md)
+
+```idris
+  , day12
+```
+
 ```idris
   ]
 ```
diff --git a/src/Years/Y2015/Day12.md b/src/Years/Y2015/Day12.md
new file mode 100644
index 0000000..92ce6dc
--- /dev/null
+++ b/src/Years/Y2015/Day12.md
@@ -0,0 +1,99 @@
+# [Year 2015 Day 12](https://adventofcode.com/2015/day/12)
+
+This day provides an introduction to our new
+[`Parser.JSON`](../../Parser/JSON.md) module, as well as the use of `DList`s[^1]
+to collect values from an indexed type family into a single collection.
+
+```idris hide
+module Years.Y2015.Day12
+
+import Control.Eff
+
+import Runner
+```
+
+```idris
+import Structures.Dependent.DList
+
+import Parser
+import Parser.JSON
+```
+
+## Parsing
+
+Parse a list of JSON values into a `DList`.
+
+`JSONValue`'s type constructor has the signature `JSONType -> Type`, forming
+what is known as an "Indexed Type Family".
+
+Each type of JSON value has a separate type, e.g. a Bool has type
+`JSONValue TBool`, a String has type `JSONValue TString`, etc. While these are
+all separate types, they all share the `JSONValue` component of the type
+constructor, making them members of the same family.
+
+Despite being members of the same type family, they still have different types,
+so we can't just shove `JSONValue`s of different types into, say, a
+`List JSONValue`, we need a collection with some amount of heterogeneity. While
+a `List (type : JSONType ** JSONValue type)` would _work_, that introduces
+various ergonomic headaches, so instead we return a `DList`[^1], a `List` like
+data structure specifically designed for collecting values from an indexed typed
+family into a single collection.
+
+The parsing logic is otherwise quite simple, we use the `many` combinator to
+turn the `value` parser, which parses a single JSON value, into one that parses
+a list of JSON values, and then use `DList`'s `fromList` method to collect the
+results into a `DList`.
+
+```idris
+parseJsons : Has (Except String) fs => Has IO fs => (input : String)
+  -> Eff fs (types : List JSONType ** DList JSONType JSONValue types) 
+parseJsons input = do
+  result <- runFirstIO (many value) input
+  case result of
+    Left err => throw $ show err
+    Right result => pure $ fromList result
+```
+
+## Solving
+
+A reducer for `DList.dFoldL` that sums all the numbers within the contained JSON
+Value.
+
+The outer function is meant to be called on a top level object, using
+`DList.dFoldL` on a `DList` of `JSONValue`s, where as the inner function
+directly reduces a `JSONValue` using `JSON.dFoldL`.
+
+```idris
+sumNumbers : Double -> (type : JSONType) -> (value : JSONValue type) -> Double
+sumNumbers dbl type value = dFoldL sumNumbers' dbl value
+  where
+    sumNumbers' : Double -> (type : JSONType) -> (value : JSONValue type) -> Double
+    sumNumbers' dbl TNumber (VNumber d) = dbl + d
+    sumNumbers' dbl _ value = dbl
+```
+
+## Part Functions
+
+### Day 1
+
+Parse our JSONs, then fold our `sumNumbers` reducer over them.
+
+```idris
+part1 : Eff (PartEff String) 
+            (Double, (types : List JSONType ** DList JSONType JSONValue types))
+part1 = do
+  input <- askAt "input"
+  (types ** values) <- parseJsons input
+  let result = dFoldL sumNumbers 0.0 values
+  pure (result, (types ** values))
+```
+
+```idris hide
+public export
+day12 : Day
+day12 = First 12 part1
+```
+
+## References
+
+[^1]: <https://git.sr.ht/~thatonelutenist/Structures/tree/trunk/item/src/Structures/Dependent/DList.md>