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)
@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