advent/src/Years/Y2015/Day14.md

4 KiB

Year 2015 Day 14

This day provides us an introduction to streams, infinite, lazily generated, collections of data.

module Years.Y2015.Day14

import Data.Primitives.Interpolation

import Control.Eff

import Runner
import Data.String
import Data.List1
import Data.Vect
import Data.Stream
import Decidable.Equality

import Util

Parsing And Datastructures

Collect the aspects defining a reindeer into a record

record Reindeer where
  constructor MkReindeer
  name : String
  speed : Nat
  duration, rest : Nat
Show Reindeer where
  show (MkReindeer name speed duration rest) = 
    "MkReindeer \{name} \{speed} \{duration} \{rest}"

This time around, since the lines describing a reindeer contain a lot of cruft, we'll handle the parsing by converting the input, after splitting it on space characters, to a Vect, and indexing into that Vect.

parseReindeer : Has (Except String) fs =>
  (input : String) -> Eff fs Reindeer
parseReindeer input = do
  parts <- note "Input has wrong size: \{input}" $
    toVect 15 . forget . split (== ' ') . trim $ input
  let name = index 0 parts
  speed <- note "" $
    parsePositive $ index 3 parts
  duration <- note "" $
    parsePositive $ index 6 parts
  rest <- note "" $
    parsePositive $ index 13 parts
  pure $ MkReindeer name speed duration rest

Solver Functions

A stream is an infinite analog of a list, storing an infinite collection of (lazily generated) values.

Streams are defined like:

data Stream' : Type -> Type where
  (::) : a -> Inf (Stream' a) -> Stream' a

Streams are a member of a family of concepts analogous to iterators in imperative languages, the different flavors of colist.

Colists are the codata duals of lists, we'll dig more into to this later, but to provide a high level summary, where data is defined by how it is constructed, codata is defined by how it is destructed. While a list is defined by how you can cons an element x onto a list xs to produce a new list x :: xs, a colist is defined by how you can break down a colist x :: xs into a head x and a tail xs.

Streams are a particular type of colist that has no empty case, breaking down a Stream will always produce an element and another stream, resulting in streams always being infinite in length.

Destructing a Stream by pattern matching is semantically equivalent to calling the next method on an iterator in a language like rust, it produces the element at the head of a stream, and a new stream producing future elements.

We will model are reindeer's future history of locations as a stream, with each element being the position at the time given by the index into the stream, generating it with a pair of mutually recursive functions. The run function adds the speed to current position to produce the next one, and the rest function doesn't modify the position whill still consuming a time step.

distances : Reindeer -> Stream Nat
distances x = run x x.duration 0
  where
    run : (deer : Reindeer) -> (left : Nat) -> (position : Nat) 
     -> Stream Nat
    rest : (deer : Reindeer) -> (left : Nat) -> (position : Nat) 
     -> Stream Nat
    run deer 0 position = rest deer deer.rest position
    run deer (S k) position = position :: run deer k (position + deer.speed)
    rest deer 0 position = run deer deer.duration position
    rest deer (S k) position = position :: rest deer k position

Part Functions

Part 1

Parse the input, generate the position Streams for each reindeer, then index the finish position in each stream.

part1 : Eff (PartEff String) (Nat, ())
part1 = do
  lines <- map (lines) $ askAt "input"
  reindeer <- traverse parseReindeer lines
  debug $ show reindeer
  let dists = map distances reindeer
  let dists_end = map (index 2503) dists
  let max = maxBy compare 0 dists_end
  pure (max, ())
public export
day14 : Day 
day14 = First 14 part1