7.6 KiB
Table of Contents
- Unified interface for any day from any year
- Effectful Parts
- The
DayRecord - The
YearRecord - The
AdventRecord
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.
module Runner
import Control.Eff
import Structures.Dependent.FreshList
%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.
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.
||| 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, WriterL "log" String, 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.
||| 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.
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.'
||| 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.
||| 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 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 Days 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 Days have the same day number.
||| 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 Days into a single Fresh List for the year, and is mostly just a simple container.
||| 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 Days are stored in a FreshList in Year, Years 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.
||| 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 Years in much the same way that Year collects a number of days, sorting the Years in a FreshList to provide API defensiveness.
||| Collect all years
public export
record Advent where
constructor MkAdvent
years : FreshList FreshYear Year
%name Advent advent, advent2, advent3
Methods
namespace Advent
locate
This is a utility function that searches the FreshList of Years 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.
||| 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