Oct 20, 2026, 2:13 PMSo here's what I did. I changed my linear scan so instead of just counting up from 0, it takes a list of numbers from STDIN. This allowed me to make a file containing a batch of numbers I want to check all at once (which I filter through perl -e 'while (<>) { last unless /\d/; $_ = oct($_); print "$_\n"; }', since I never figured out how to access the documented octal support library in Idris). This lets me test every leftmost digit, every one-right-of-leftmost digit, etc…
Oct 20, 2026, 2:17 PM…I can test as many candidate numbers as I want at once and see the results in bulk. I do this to (see images above) find the correct digit one octal at a time left to right, each octal input digit matching one more digit in the output list.
This works great until my number suddenly "forks". On the 8th (1-indexed) digit, either 1 or 5 produces a matching result. So after that point, instead of testing 8 at a go I'm testing 16, simultaneously testing "world 1" and "world 5".
Oct 20, 2026, 2:20 PMThis isn't so bad either except the forking *continues*; I'm quickly testing 3 parallel worlds, then one dies off. I basically manage until I hit digit 14 of 16, which turns out to have **six** different next options. I sort of do my best from there and eventually find a number: 165523097481149 (octal 4550533133267675).
It's wrong. It's too high. There are apparently multiple correct solutions, and AOC guy (so says the problem solution) wants the *lowest*. Which I fumbled.
Oct 20, 2026, 2:22 PMNow that I've done the process by hand, though, I have a pretty good understanding of what it looks like, so now I'm in a much better position to automate this process, with the automation presumably not making whatever mistake my fallable human brain made to miss the true-lowest possibility.
I now believe I *could* finish this puzzle by my self-imposed deadline, but maybe I won't, since I got 1.5 hours of sleep last night and I'm leaving to go to the doctor. Uh… now.
Oct 20, 2026, 9:08 PMOkay. I have the architecture for the search program that will find my "part 2" solution clearly in mind, I am certain it will work, I have the "type-driven development" scaffold of it written down in a file, and this is just me commemorating that I *could have* finished this in the next ~2 hours before I hit the one week anniversary of this thread but I decided it was more important to lay down and sleep.
Oct 21, 2026, 12:23 AMAlright. Idris question. Do you just have like… a for loop. Hiding in this language somewhere. Yes I know how to do a loop with recursion. But you've already *got* monads/"do" and sometimes it's just true that the most semantically efficient way to communicate something is "for i in 1 to 8" or whatever. You seem to have range() . I think so anyway. I've thought I found things in the stdlib before and been wrong. https://idris2docs.sinyax.net/data/papers/docs/Data.Enumerate.html#Data.Enumerate.Enumerator
You didn't document "if" so maye you didn't document "for"
Oct 21, 2026, 1:16 AMIf this were scheme or ocaml I'm pretty sure I could do what i'm doing with zip or other pointfree combinators but unfortunately Idris's most Haskell-like quality is the documentation believes that giving the type of a function is sufficient for a reader to understand what it is the arguments do
Oct 21, 2026, 1:55 PMCurrently drowning in a never-ending chain of writing basic "case" or "if" statements and getting unintelligible errors like "expected =>" on a => or "expected end of expression". Trying to not run to Mastodon for help on every one. Did encounter one thing that seems so actionable I'm considering filing it:
Why are members of the sequence "0..7" not Fin 8?
![let new = for [0..7] (\i => shiftL (the Bits64 1) (cast i))
"cast i" is highlighted saying that i (0..7) is an integer and "cast i" needs a Fin 64](https://files.mastodon.social/media_attachments/files/117/479/226/319/701/575/original/3558a17cd05a3caf.png)
Looks like you work with the program 2,4,1,1,7,5,1,5,4,1,5,5,0,3,3,0 for which 0o4550533133267675 actually is a solution.
But AOC (https://adventofcode.com/2024/day/17/input) uses the program 2,4,1,2,7,5,1,7,4,4,0,3,5,5,3,0
Oct 20, 2026, 3:55 PM@hcschuetz first off, I'd appreciate answers being behind spoiler tags!
Second off every AOC participant gets individualized inputs specifically to prevent answer sharing like this.
@mcc
I hope my previous post didn't spoiler too much. After all you already had this number.
And thanks for the hint about individualized inputs. Wasn't aware of this.
@mcc there's a for and for_ function in the prelude. the difference is that for_ doesn't care about the output from traversing the data structure (returns m () for a monad m) but for does (like map with side effects). probably for_ is what you want. https://idris2docs.sinyax.net/data/prelude/docs/Prelude.Interfaces.html#Prelude.Interfaces.for_
also you can do range comprehensions [ 1 .. 8 ] to get a range list: https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#list-comprehensions
so it should be something like,
for_ [ 1 .. 8 ] $ \i => do
... something with i ...
Oct 21, 2026, 2:29 AM@typeswitch hey that rules, thank you
Oct 21, 2026, 3:13 AM@mcc @typeswitch there's a meme in Haskell, "it's always `traverse`", because `traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)` is useful for a lot of different things with the right choices of `f` and `t`. (in this case `f = IO`, `t = List`, and `for_ xs f = void (traverse f xs)`)
Oct 21, 2026, 3:22 AM@zmz @typeswitch gonna be honest i'd never encountered traverse before this project but i got *really* excited when i started to understand it. i'm still not sure i understand it
Oct 21, 2026, 4:11 AM@mcc @typeswitch `traverse` performs some effect on each element of a structure in some canonical traversal order. The flexibility comes from the fact that it's parameterized over both the structure (the Traversable) and the the effect (the Applicative) (excuse the Haskell instead of Idris, but it should be similar)
@mcc because i doesn't know anything about what list was given, all it knows is that it's an Integer
you probably want
allFins 8 for all the numbers in Fin 8iterateN to apply (fun x => shiftL x FZ) on l eight times and collect the intermediate results in a list@mcc maybe using https://idris2docs.sinyax.net/data/prelude/docs/Prelude.Interfaces.html#Prelude.Interfaces.for like for [1..8] (\i => ...)
(the list comprehension syntax is noted here https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#list-comprehensions although it's unclear whether the endpoints are inclusive lol)
@mcc as it happens that page is also where if is documented
Oct 21, 2026, 3:10 AM@ionchy thank you much