advent of code 2024, day 1, part 1

i don’t think i’m going to get into it this year. maybe this will be the only one i do. but i did this one.

i haven’t done much on quox this year (nothing in the last… six months…), but it’s not abandoned! i promise.

it even has the beginnings of a standard library! which also mostly existed last year too.

load "bool.quox"
load "ordering.quox"
load "list.quox"
load "nat.quox"
load "string.quox"
load "io.quox"

it’s not very big, though, so it doesn’t have line splitting yet. that’s fine though.

def lines : ω.String → List String =
  λ str ⇒ string.split (char.eq char.newline) str

so. let’s actually read the puzzle. blah blah blah… elves… lists of numbers… blah blah… right.

easy, except, oh no. sorting. that’s not very structurally recursive. (reminder: the only recursion is natural numbers)

after thinking about whether i can model accessibility predicates with what i already have for an hour—i don’t think so—i decided to just give up and use insertion sort. that’s structurally recursive. the list isn’t gonna be that long.

currently, the way lists are defined is via vectors, which are what people with dependent type brain call lists of known length. not arrays. sorry it’s not my fault. we get vectors by recursion on our one recursive thing.

def0 Vec : ℕ → Type → Type =
  λ len A ⇒
  case len return Type of {
    zero            ⇒ {nil};
    succ len', Tail ⇒ A × Tail
  };

in a match on a ℕ, there is (optionally) a second variable in the succ case, which is the result of a recursive call. in this case, in a call to Vec 4 ℕ, Tail refers to the result of Vec 3 ℕ (which is ℕ × ℕ × ℕ × {nil}).

types that look {like, this} are enums. values of an enum type look like 'this.

finally, a List A is just a number, paired with a vector of that length.

def0 List : Type → Type = (len : ℕ) × Vec len A

given a definition of a comparison function, it’s possible to insert a value into a vector of length n, getting one of length succ n in return. apart from the excessive annotations (also not done yet: any kind of anything-inference!) and the slightly weird-looking recursive call, this should be pretty normal.

def0 Ordering : Type = {lt, eq, gt}
def0 Compare  : Type → Type = λ A → ω.A → ω.A → Ordering

def insertV :
    0.(A : Type) → ω.(Compare A) → ω.(len : ℕ) →
    ω.A → ω.(Vec len A) → Vec (succ len) A =
  λ A cmp len ⇒
    caseω len return len' ⇒ ω.A → ω.(Vec len' A) → Vec (succ len') A of {
      zero                ⇒ λ x _  ⇒ (x, 'nil);
      succ len', ω.inTail ⇒ λ x xs ⇒
        let0 len : ℕ = succ len'; Res : Type = Vec (succ len) A in
        caseω xs return Res of { (y, ys) ⇒
          case cmp x y return Res of {
            'lt ⇒ (x, y, ys);
            'eq ⇒ (x, y, ys);
            'gt ⇒ (y, inTail x ys)
          }
        }
    }

if you strip away those bits, you essentially get the equivalent of this.

insertV :: (α → α → Ordering) → α → [α] → [α]
insertV cmp x [] = [x]
insertV cmp x (y:ys) = case cmp x y of
  LT → x : y : ys
  EQ → x : y : ys
  GT → y : insertV cmp x ys

to insert into a list, just take the length off and put the new one back on.

def insert : 0.(A : Type) → ω.(Compare A) → ω.A → ω.(List A) → List A =
  λ A cmp x ys ⇒
    letω len = fst ys; elems = snd ys in
    (succ len, insertV A cmp len x elems)

so to inefficiently sort a list, take each element, one by one, and insert it into the right place!

def sort : 0.(A : Type) → ω.(Compare A) → ω.(List A) → List A =
  λ A cmp ⇒ list.foldrω A (List A) (list.Nil A) (insert A cmp)

does it work? let’s write one (1) test.
if it doesn’t, then sort ℕ (λ m n ⇒ nat.compare m n) (5, 1,4,2,5,3,'nil) (probably) won’t reduce to the right thing, and the definition won’t typecheck.

def0 sort-14253 :
      sort ℕ (λ m n ⇒ nat.compare m n) (5, 1,4,2,5,3,'nil)
    ≡ (5, 1,2,3,4,5,'nil) : List ℕ =
  δ _ ⇒ (5, 1,2,3,4,5,'nil)

good enough for me!

next up, symmetric difference. or |x - y|, or whatever you wanna call it. you can do that by recursing on both arguments in lockstep, which luckily is something i added to the stdlib last year. oh and in the compiled output just use scheme’s arithmetic operators instead of going O(n).

#[compile-scheme "(lambda% (m n) (abs (- m n)))"]
def sd : ω.ℕ → ω.ℕ → ℕ =
  nat.elim-pairω (λ _ _ ⇒ ℕ)
    0                  -- |0 - 0|           = 0
    (λ m _ ⇒ succ m)   -- |succ m - 0|      = succ m
    (λ n _ ⇒ succ n)   -- |0 - succ n|      = succ n
    (λ _ _ d ⇒ d)      -- |succ m - succ n| = |m - n|

def0 sd-6-3 : sd 6 3 ≡ 3 : ℕ = δ _ ⇒ 3
def0 sd-3-6 : sd 3 6 ≡ 3 : ℕ = δ _ ⇒ 3

now the annoying part. chopping up lines. break it on whitespace, then on non-whitespace, and convert the first and third parts to numbers.

def number-pair : ω.String → ℕ × ℕ =
  λ str ⇒
    letω a_bc = string.break char.ws? str;
         a = fst a_bc; bc = snd a_bc;
         c = snd (string.span char.ws? bc) in
    (string.to-ℕ-or-0 a, string.to-ℕ-or-0 c)

and the main function. boy i wish i had some do notation right now..! one day.

#[main]
def part1 : IO True =
  io.bindω String True (io.read-fileω "1.txt") (λ str ⇒
    letω pairs = list.mapω String (ℕ × ℕ) number-pair (lines str);
         lists = list.unzip ℕ ℕ pairs;
         sortℕ = sort ℕ (λ m n ⇒ nat.compare m n);
         as = sortℕ (fst lists); bs = sortℕ (snd lists);
         diffs = list.zip-with-uneven ℕ ℕ ℕ sd as bs;
    in
    io.dump ℕ (list.sum diffs))

after taking almost four entire seconds to compile, it… works. after i add another compile-scheme thing to the stdlib’s nat.compare, anyway.

i had other things to do today so i didn’t get around to even looking at part two. bye mlem