blog/posts/aoc2024.md

---
title: advent of code 2024, day 1, part 1
date: 2024-12-02
tags: [computer, quox. the language, december adventure]
summary: don't expect me to do the whole thing okay
...

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…)]{.note}, but it's not abandoned! i promise.

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

```quox
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.

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

:::aside
**what does ω mean?**
quox has linear types, which means that by default, each argument to a function, both sites of a pair, etc., have to be used exactly once in each code path. for function arguments that need to be uses more flexibly than that (more than once, a statically-unknown number of times, or whatever), they can be marked `ω` like above. the function passed to `string.split` also has the type `ω.Char → Bool`. it wouldn't be very useful if testing a character also consumed it: then you wouldn't be able to put it in the string.

obviously this is not a very _ergonomic_ design. at some point i want to have something that fills the same role as rust's borrowed values, but that is not yet the case. so right now there are _lots_ of `ω`s.
:::


so. let's actually read [the puzzle][aoc1]. blah blah blah… elves… lists of numbers… blah blah… right.

- list of pairs of numbers
- [(read the string representation into actual numbers)]{.note}
- unzip the pairs into two lists of numbers
- sort each list
- find the difference between each corresponding element in the sorted lists and sum them

[aoc1]: https://adventofcode.com/2024/day/1

:::{.aside .floating .right}
one of the bits of detritus in the growing stdlib is half an implementation of merge sort. the half that's possible.
:::

easy, except, oh no. __sorting__. that's not very structurally recursive. [(reminder: the only recursion is natural numbers)]{.note}

after thinking about whether i can model [`@accessibility predicates@`][acc] 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.

[acc]: https://github.com/agda/agda-stdlib/blob/master/src/Induction/WellFounded.agda#L40-L43


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.

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

:::{.figure .floating .right .shaped .nobg}
<img src=aoc2024/succ.png style='height: 1.5em'>
:::

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.

```quox
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.

```quox
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.

```haskell
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.

```quox
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!

```quox
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.

```quox
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).

```quox
#[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.

```quox
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.

```quox
#[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 [<img src=/images/qt.svg alt=mlem class=emoji><img src=/images/qt.svg alt='' class=emoji><img src=/images/qt.svg alt='' class=emoji>]{.emojiseq}