Idris/advent
1
0
Fork 0
Code Issues Pull requests Actions Packages Projects Releases Wiki Activity

Revise Runner

Browse source
This commit is contained in:
Nathan McCarty 2025-01-23 00:29:53 -05:00
parent 407149dd4a
commit 76fcb6c34b
1 changed files with 34 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

69
src/Runner.md
View file

@ -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