From 76fcb6c34bbfdae36a76194bbc41d55aa0c3ba35 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 23 Jan 2025 00:29:53 -0500 Subject: [PATCH] Revise Runner --- src/Runner.md | 69 +++++++++++++++++++++++++-------------------------- 1 file changed, 34 insertions(+), 35 deletions(-) diff --git a/src/Runner.md b/src/Runner.md index 201baff..31b036e 100644 --- a/src/Runner.md +++ b/src/Runner.md @@ -22,16 +22,15 @@ import public Util.Eff # Effectful Parts 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. +the effect stack is meant to be the same across both parts, only varying in the +type of the error value for the `Except` effect, we construct a type level +function to have a single source of truth. The `err` type can be any type with a +`Show` implementation, but that constraint will be tacked on in the next step. The `Logger` 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 +to pass in the input, 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 will come in handy if a part needs `IO` for performance reasons. ```idris @@ -46,19 +45,19 @@ PartEff err = # The `Day` Record 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. +effectful `part2` computation, and the day number, with some type wrangling to +get the type system out of our way. `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 +we can display them in `Main`, where the `Day` is consumed, without having to actually know what the types are. 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`. +resulting from parsing, between `part1` and `part2`. This is achieved through +the erased `ctx` type, which is totally opaque to the runner. The code in `Main` +will provide the value of the `ctx` type produced as part of the output of +`part1` and as the input of `part2`. ```idris ||| Model solving a single day @@ -80,9 +79,9 @@ record Day where 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. +requiring that `part2` be wrapped in a `Just` when there is one. We provide a +pair of constructors for the case where there is only a `part1`, as well as one +for when there is a `part1` and a `part2`. ```idris namespace Day @@ -91,8 +90,7 @@ namespace Day ### First 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.' +`part2` with `Nothing` and setting all of `part2`'s type arguments to `()`. ```idris ||| Constructor for a day with only part one ready to run @@ -106,8 +104,8 @@ us.' ### Both -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`. +The `Both` constructor does less heavy lifting, the only thing it needs to do is +wrap `part2` in a `Just`. ```idris ||| Constructor for a day with both parts ready to run @@ -123,16 +121,17 @@ needs to do for us is wrap `part2` in a `Just`. ## Freshness 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. +[structures](https://git.sr.ht/~thatonelutenist/Structures) package to build our +API defensively against duplicate days and cosmetically annoying out of order +day registration. A Fresh List structurally only allows you to prepend/cons an +element onto it when it satisfies some _freshness criteria_ relative to the +elements already contained in the list. -Here, we compare the day numbers of the two `Day`s using the less-than +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. +Fresh List of `Day`s is sorted in ascending order and that no two `Day`s have +the same day number. ```idris ||| Freshness criteria for days @@ -150,7 +149,7 @@ FreshDay x y = x.day < y.day # The `Year` Record The `Year` record collects a number of `Day`s into a single Fresh List for the -year, and is mostly just a simple container. +year, also containing the year number for this collection. ```idris ||| Collect all the days in a given year @@ -166,9 +165,10 @@ record Year where 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`. +`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`. ```idris ||| Freshness criteria for years @@ -186,8 +186,7 @@ FreshYear x y = x.year < y.year # The `Advent` Record 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. +`Year` collects a number of days. ```idris ||| Collect all years