advent/src/Runner.md

# Unified interface for any day from any year

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.

This provides a defensively built API for constructing the overall `Advent` data
structure that prevents registering a day/year twice or registering days/years
out of order.

```idris
module Runner

import Control.Eff
import Structures.Dependent.FreshList

import public Util.Eff

%default total
```

# 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 `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
reasons.

```idris
||| The effect type is the same in boths parts one and two, modulo potentially
||| different error types, so we calucate it here
public export
PartEff : (err : Type) -> List (Type -> Type)
PartEff err =
  [IO, Except err, Logger, ReaderL "input" String]
```

# 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.

`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.

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`.

```idris
||| Model solving a single day
public export
record Day where
  constructor MkDay
  day : Nat
  {0 out1, out2, err1, err2 : Type}
  {auto showOut1 : Show out1}
  {auto showOut2 : Show out2}
  {auto showErr1 : Show err1}
  {auto showErr2 : Show err2}
  part1 : Eff (PartEff err1) (out1, ctx)
  part2 : Maybe (ctx -> Eff (PartEff err2) out2)
%name Day day, day2, day3
```

## Smarter Constructors

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.

```idris
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.'

```idris
  ||| Constructor for a day with only part one ready to run
  public export
  First : Show err => Show out =>
    (day : Nat) -> (part1 : Eff (PartEff err) (out, ctx'))
    -> Day
  First day part1 =
    MkDay day part1 Nothing {out2 = ()} {err2 = ()}
```

### 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`.

```idris
  ||| Constructor for a day with both parts ready to run
  public export
  Both : Show o1 => Show o2 => Show e1 => Show e2 =>
    (day : Nat) -> (part1 : Eff (PartEff e1) (o1, ctx')) ->
    (part2 :ctx' -> Eff (PartEff e2) o2)
    -> Day
  Both day part1 part2 =
    MkDay day part1 (Just part2)
```

## 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.

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.

```idris
||| Freshness criteria for days
|||
||| A day is fresh compared to another if the day number of the former day is
||| strictly less than the day number of the latter day
|||
||| This ensures that the days list is always in incrimenting sorted order
||| (since we are consing to the front of the list) with no duplicate days
public export
FreshDay : Day -> Day -> Bool
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.

```idris
||| Collect all the days in a given year
public export
record Year where
  constructor MkYear
  year : Nat
  days : FreshList FreshDay Day
%name Year year, year2, year3
```

## Freshness

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`.

```idris
||| Freshness criteria for years
|||
||| A year is fresh compared to another if the year number of the former year is
||| strictly less than the year number of the latter year
|||
||| This ensures that the years list is always in incrimenting sorted order
||| (since we are consing to the front of the list) with no duplicate years
public export
FreshYear : Year -> Year -> Bool
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.

```idris
||| Collect all years
public export
record Advent where
  constructor MkAdvent
  years : FreshList FreshYear Year
%name Advent advent, advent2, advent3
```

## Methods

```idris
namespace Advent
```

### locate

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.

We don't have to worry about potentially encountering duplicates here because of
the freshness restriction.

```idris
  ||| Attempt to locate `Day` entry corresponding to the provided day and year numbers
  export
  locate : (year, day : Nat) -> Advent -> Maybe Day
  locate year day advent = do
    year <- find (\x => x.year == year) advent.years
    find (\x => x.day == day) year.days
```