Year 2015 Day 3

This day provides a gentle introduction to mutual blocks and mutually recursive functions.

import Data.SortedSet
import Data.String

import Util

Parsing and data structures

We'll do parsing a little more properly this time, turning the input into a list of movement commands

data Movement = North | East | South | West

We need an effectful operation to parse a single char into a movement. We'll pattern match on the char, and include a catch-all case that throws an error in the event of an invalid char

parseMovement : Has (Except String) fs => (x : Char) -> Eff fs Movement
parseMovement '^' = pure North
parseMovement '>' = pure East
parseMovement 'v' = pure South
parseMovement '<' = pure West
parseMovement x = throw "Invalid Movement: \{show x}"

We also need to be able to translate a Movement into a vector of length one pointing in the given direction in coordinate space. Somewhat arbitrarily, we chose 'North' to be positive x and 'East' to be positive y.

vector : Movement -> (Integer, Integer)
vector North = (1, 0)
vector East = (0, 1)
vector South = (-1, 0)
vector West = (0, -1)

Solver functions

Visited houses

This is a pretty simple task, we are just applying the movements to our current position, and adding our current position to the set of visited locations, so we'll handle this with a normal tail recursive function.

To keep the api nice, we wont ask for the set or the starting location in the top-level function, and instead have the top level function initialize the set and location before passing control to the inner tail-recursive variant.

Because the starting location gets a present, we'll add our location to the set before performing the movement, so we will need to add our final location to the set in the recursive base case.

visitedLocations : List Movement -> SortedSet (Integer, Integer)
visitedLocations xs = visitor xs empty (0, 0)
  where
  visitor : (moves : List Movement) -> (set : SortedSet (Integer, Integer))
    -> (location : (Integer, Integer)) -> SortedSet (Integer, Integer)
  visitor [] set location = insert location set
  visitor (x :: xs) set location = 
    visitor xs (insert location set) (location >+< vector x)

Robo Santa

This one gets a bit more interesting, we'll adopt the same tail recursive approach, but instead use a mutual block and two mutually recursive functions to handle the alternation between santa and robo santa. The visitSanta function will pass control to visitRobo after executing its movement, and vise versa.

We'll want to insert both present deliverer's locations in the recursive base case, this may result in a duplicate location, but that's okay because SortedSet will only hold at most one of each item inserted into it.

In idris, there is a general requirement that values be defined before their use, a common feature of dependently typed languages, resulting from the fact that just having the type signature of a function/value alone is not always enough to perform type checking, as functions can appear as part of types, requiring evaluation of the function and making automatic dependency analysis effectively impossible.

Inside a mutual block, elaboration behaves differently, elaborating types first and then values in separate passes. This restricts what you can do a little, but enables mutually recursive functions.

visitedLocations' : List Movement -> SortedSet (Integer, Integer)
visitedLocations' xs = visitSanta xs empty (0, 0) (0, 0)
  where 
  mutual
    visitSanta : (moves : List Movement) -> (set : SortedSet (Integer, Integer))
      -> (santa, robo : (Integer, Integer)) -> SortedSet (Integer, Integer)
    visitSanta [] set santa robo = insert santa . insert robo $ set
    visitSanta (x :: xs) set santa robo = 
      visitRobo xs (insert santa set) (santa >+< vector x) robo

    visitRobo : (moves : List Movement) -> (set : SortedSet (Integer, Integer))
      -> (santa, robo : (Integer, Integer)) -> SortedSet (Integer, Integer)
    visitRobo [] set santa robo = insert santa . insert robo $ set
    visitRobo (x :: xs) set santa robo =
      visitSanta xs (insert robo set) santa (robo >+< vector x)

Part Functions

Part 1

Similar to the previous day, we get our input, unpack it, and traverse our effectful movement parsing function over it, before feeding that into our solving function.

part1 : Eff (PartEff String) (Nat, List Movement)
part1 = do
  input <- map (unpack . trim) $ askAt "input"
  movements <- traverse parseMovement input
  let locations = visitedLocations movements
  pure (length locations, movements)

Part 2

Same as Part 1, but with a different solving function

part2 : (movements : List Movement) -> Eff (PartEff String) Nat
part2 movements = do
  let locations = visitedLocations' movements
  pure . length $ locations