---
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}
:::
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 [
]{.emojiseq}