advent-of-code-day-one.idr

import Data.Vect
import Data.Nat.DivMod

-- rotates a vector's elements.  Note that from the type signature,
-- you can't rotate more than the length of the vector
rotate : (n : Nat) -> Vect (n + m) a -> Vect (n + m) a
-- {m} captures m, which is an implicit parameter - we'll need it for a proof below
rotate {m} n xs =
    let newSuffix = take n xs
        newPrefix = drop n xs
    -- we're taking a tail of elements and sticking it onto a new head,
    -- but we need to convince Idris that gives us a value of the proper
    -- type (ie. it preserves the length of the vector).  Adding a vector
    -- of m items (newPrefix) to one of n items (newSuffix) gives us
    -- a Vect (m + n) a, so we need to tell Idris that this is usable
    -- as a Vect (n + m) a using the commutative property
    in rewrite plusCommutative n m in newPrefix ++ newSuffix

-- this is the implementation for the first part of the day 1 problem
-- Vect (S n) a just means that our argument must not be empty
f : (Num a, Eq a) => Vect (S n) a -> a
f digits =
    let next_digits = rotate 1 digits -- just move the first element to the back
        -- the (_ ** matching_digits) is a dependent pair - filter on Vects in
        -- Idris returns a dependent pair because we sometimes need to track the
        -- length of the Vect.  In this case, I just throw it away because I'm
        -- just going to sum up the values anyway
        (_ ** matching_digits) = filter (uncurry (==)) $ zip digits next_digits
    in sum $ map fst $ matching_digits

-- A proof data type to track whether or not a Nat (natural number) is
-- even - the only possible inhabitant of this type (MkEven)
-- results in an Even (even number)
data Even : (n : Nat) -> Type where
  MkEven : (n : Nat) -> Even (mult n 2)

-- Proof that Even (odd number) is impossible - the type Even (S (mult n 2)) is
-- uninhabitable, because we can't create a (MkEven n) to give us an Even (mult n 2)
oddIsOdd : Even (S (mult n 2)) -> Void
oddIsOdd _ impossible

-- Decider function to determine whether or not a value is even.  If you're not
-- familiar with Idris, this might seem odd - why not return a boolean or a Maybe?
-- Well, it's because Dec values provide either proof that a property holds, or
-- a contradiction to show that it doesn't.  These proofs and contradictions are
-- based on the structure of the data, which allows the compiler to perform its
-- black magic.
total
isEven : (n : Nat) -> Dec (Even n)
isEven n =
    let (MkDivMod q r prf) = divMod n 1 -- the second operand is the divisor minus 1 to prevent you from being able to divide by zero
    in case r of
      Z => Yes $ MkEven q
      (S Z) => No $ oddIsOdd
      _ => assert_unreachable -- Sorry, this is sloppy! I *know* that the remainder of n / 2 is either 0 or 1, but Idris doesn't,
                              -- and I'm too lazy to convince it otherwise right now

-- Proof that n * 2 = n + n - will come in handy below
nPlusNEqualsNTimesTwo : (n : Nat) -> (mult n 2) = (plus n n)
nPlusNEqualsNTimesTwo n =
    -- Refl is just proof that x = x - I could probably golf this proof down a little
    -- more, but this works fine.  Basically we use the commutative property of multiplication
    -- and the fact that 0 is the additive identity to make the proof work
    rewrite multCommutative n 2 in rewrite sym $ plusZeroRightNeutral n in Refl

-- implementation for the second part of day 1
-- Contrast with function `f`: it takes a proof (prf) that the length of the
-- input vector is even.  This is why we don't need to say Vect (S n) a
-- here - the Even n proof is more useful for our purposes
g : (Num a, Eq a) => Vect n a -> {auto prf: Even n} -> a
-- The {prf=...} syntax destructures the implicit proof parameter so we know
-- what half of n is - you might think "why not just n / 2?", but we need to
-- rely on the structure of the MkEven value to be able to help Idris out
g {prf=MkEven half_n} digits =
    -- For some reason, I needed to use `the` to cast the rewrite to make
    -- Idris happy
    let digits' = the (Vect (plus half_n half_n) _) $
        -- just tells Idris that a `Vect (half_n * 2) a` is the same as a `Vect (half_n + half_n) a`...
                    rewrite sym $ nPlusNEqualsNTimesTwo half_n in digits
        -- ...which allows us to call rotate
        next_digits = rotate half_n $ digits'
        (_ ** matching_digits) = filter (uncurry (==)) $ zip digits' next_digits
    in sum $ map fst $ matching_digits