192 lines
7.7 KiB
Markdown
192 lines
7.7 KiB
Markdown
|
---
|
|||
|
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}
|