0 | # Unified interface for any day from any year
2 | This module provides some basic data types for building an application containing all my solutions to all of the parts of all the days across all of the years.
4 | This provides a defensively built API for constructing the overall `Advent` data structure that prevents declaring a day twice or declaring days out of order.
10 | import Structures.Dependent.FreshList
17 | The solution to each part of a day is run as an effectful computation, and as the available effects are meant to be the same across both parts, only varying in the type of the error value in the `Except` effect, I construct a type level function to have a single source of truth for this. The `err` type can be any type with a `Show` implementation, but that constraint will be tacked on in the next step.
19 | A `Writer` effect is provided for logging, and a `Reader` effect is provided to pass in the input, just to make the top level API a little bit cleaner. `IO` is also provided, even though the part solutions themselves shouldn't really be doing any IO, this may come in handy if a part needs `IO` for performance reasons.
25 | PartEff : (err : Type) -> List (Type -> Type)
27 | [IO, Except err, WriterL "log" String, ReaderL "input" String]
32 | The `Day` type groups together an effectful `part1` computation, an optional effectful `part2` computation, the day number, and does some type wrangling to get the type system out of our way on this one.
34 | `part1` and `part2` are allowed independent output and error types, and this record captures `Show` implementations for those output and error types so that we can display them in `Main` where the `Day` is consumed without having to actually know what the types are.
36 | It is often useful to pass a bit of context, such as the data structures resulting from parsing, between `part1` and `part2`, and this is achieved by the erased `ctx` type, which is totally opaque here. The runner code in `Main` will provide the value of the `ctx` type produced as part of the output of `part1` as the input of `part2`.
44 | {0 out1, out2, err1, err2 : Type}
45 | {auto showOut1 : Show out1}
46 | {auto showOut2 : Show out2}
47 | {auto showErr1 : Show err1}
48 | {auto showErr2 : Show err2}
49 | part1 : Eff (PartEff err1) (out1, ctx)
50 | part2 : Maybe (ctx -> Eff (PartEff err2) out2)
51 | %name Day
day, day2, day3
54 | ## Smarter Constructors
56 | The default `MkDay` constructor is slightly cumbersome to use, always requiring _something_ for the `part2` slot, even if there isn't a part 2 yet, and requiring that `part2` be wrapped in a `Just` when there is one, so we provide a pair of constructors for the case where there is only a `part1` and for where there is a `part1` and a `part2` that handle that for us.
64 | The `First` constructor only accepts a `part1`, it does the work of filling in `part2` with `Nothing` and setting all of `part2`'s type arguments to `()` for us.'
69 | First : Show err => Show out =>
70 | (day : Nat) -> (part1 : Eff (PartEff err) (out, ctx'))
73 | MkDay day part1 Nothing {out2 = ()} {err2 = ()}
78 | The `Both` constructor does a little bit less heavy lifting, the only thing it needs to do for us is wrap `part2` in a `Just`.
83 | Both : Show o1 => Show o2 => Show e1 => Show e2 =>
84 | (day : Nat) -> (part1 : Eff (PartEff e1) (o1, ctx')) ->
85 | (part2 :ctx' -> Eff (PartEff e2) o2)
87 | Both day part1 part2 =
88 | MkDay day part1 (Just part2)
93 | We will be using a _Fresh List_ from the [structures](https://git.sr.ht/~thatonelutenist/Structures) package to build defensiveness into the API. A Fresh List structurally only allows you to prepend an element onto it when it satisfies some _freshness_ criteria relative to the elements already in the list.
95 | Here, we compare the day numbers of the two `Day`s using the less-than relationship. Since we are operating on the start of the list when this comparison takes place, this enforces, through type checking, that the resulting Fresh List is sorted in ascending order and that no two `Day`s have the same day number.
106 | FreshDay : Day -> Day -> Bool
107 | FreshDay x y = x.day < y.day
110 | # The `Year` Record
112 | The `Year` record collects a number of `Day`s into a single Fresh List for the year, and is mostly just a simple container.
120 | days : FreshList FreshDay Day
121 | %name Year
year, year2, year3
126 | Much like `Day`s are stored in a `FreshList` in `Year`, `Year`s will be stored in a `FreshList` in `Advent`, so we need to provide a freshness criteria for `Year` as well. We do so by applying the less-than relationship against the year number of the two `Years`, for the same reasons and with the same results as with `FreshDay`.
137 | FreshYear : Year -> Year -> Bool
138 | FreshYear x y = x.year < y.year
141 | # The `Advent` Record
143 | The `Advent` record collects a number of `Year`s in much the same way that `Year` collects a number of days, sorting the `Year`s in a `FreshList` to provide API defensiveness.
148 | record Advent where
149 | constructor MkAdvent
150 | years : FreshList FreshYear Year
151 | %name Advent
advent, advent2, advent3
162 | This is a utility function that searches the `FreshList` of `Year`s for the provided year number, then searches the resulting `Year`, if one exists, for the provided day number.
164 | We don't have to worry about potentially encountering duplicates here because of the freshness restriction.
169 | locate : (year, day : Nat) -> Advent -> Maybe Day
170 | locate year day advent = do
171 | year <- find (\x => x.year == year) advent.years
172 | find (\x => x.day == day) year.days