Oct 19, 2026, 4:19 PMMy program:
Runs a simulation over time in the IO monad, calling "putStr" and "die" as appropriate. If I were in an imperative language, I'd just change those to append to an array and throw an exception.
But monads are "programmable semicolons", right? So I should be able to have one program parameterized over a monad, a "submit value" function, and a "early terminate" function. I should be able to emulate array.push_back() and throw. The monad just handles it.
Oct 19, 2026, 4:26 PMI mean, also I could just rewrite the program without a monad at all. I could do normal recursive techniques, accumulate my values in an accumulator, and terminate early with Either. But I already know how to do that, so it's not interesting. What's interesting is doing something I couldn't do, or couldn't do easily, without Haskell/Idris.
So I guess my question for Idris users is:
Do I "write my own monad"? Or is "IO" adequate for "emulate mutable state in the form of one accumulator list"?
Oct 19, 2026, 4:36 PM(Also, if you're wondering: The reason to not just accumulate in a list and then print it at the end is that some of the inputs to this program will result in *infinite runtime*, and in that case the best case is to write the updates to STDOUT as I go so I can introspect what is happening in the debug mode.)
Oct 20, 2026, 12:22 AMCurrent status: accumulating a list using value::rest and then having to reverse it at the end. oh geez these are real Ocaml hours here
Hey, did I see at some point Idris has a List variant in the standard library which is optimized for fast tail insertion somehow? Did I imagine that?
Oct 20, 2026, 2:28 AMRight up until the last minute this language is giving me a cornucopia of "this thing I did before has stopped working suddenly and the error message doesn't hint why"
Here, a very simple "case" statement fails, because… because the variable I assigned to wasn't used. I was sincerely not sure if I was confused about the (seemingly undocumented) whitespace rules again. No, I just needed to use the result. But I wanted to write the expression before I tried to use it. Silly me!
Oct 20, 2026, 2:49 AMAlright. Any Idris users awake?
I want to compare two lists. That's easy to implement recursively, and I THINK it's implementable with zipWith tho docs remain… vague ( https://idris2docs.sinyax.net/data/base/docs/Data.Zippable.html#Data.Zippable.zipWith what does zip do if the lists are of unequal length?)
…but! It *sounds* like something the standard library would have. And indeed I find a Interface-satisfying function exists in in Data.List.Equalities…
…but I can't import that.
I type this post, and the explanation jumps out.
Oct 20, 2026, 2:52 AM…it's in contrib. List equality isn't in the "prelude" (default) or "base" (despite the name, not default; you have to specifically import base).
The doc doesn't *say* it's in contrib. But the *url slug* says it's in contrib. I only notice this when pasting the url into this compose box.
…Also, while writing this thread, I got Idris2 maintainers begging me not to use anything in contrib because that's all stuff that's GOING to be spun out into its own library but hasn't been yet. So, uh…
Oct 20, 2026, 2:59 AMOh right, I was going to ask a question. Any Idris users awake? Two part question.
1. https://idris2docs.sinyax.net/data/contrib/docs/Data.List.Equalities.html#Data.List.Equalities.consCong2 Do I understand write that if I can import the package containing this symbol, a == b and a /= b on `List int` will magically work?
2. Is it surprising that I changed my ipkg to say "depends = base, contrib" and despite this, "import Data.List.Equalities" fails in the Idris executable, and succeeds in the LSP? And also list1==list2 still fails with the mystery (?a->?f?a->?b error?
Oct 20, 2026, 3:01 AMWait. Wait. Hold on a friggin minute
Computer
Enhance
… this type is assigned female at birth ????
Oct 20, 2026, 3:17 AMOkay. Whatever. Whatever!! At this point I go on tilt. I can't decode this documentation, I can't figure out why `idris2 -o` ignores my ipkg and `pack exec` fails without printing error messages. I know SML/NJ! I write my own list-equality helper. It takes seconds.
…oh wait, it's not letting me use the Eq interface. Odd. Fine, I'll compare ints.
…oh, there's… no such thing as… equality on ints. fine. Fine! I wanted Bits64s anyway. I—
OH COME ON HOW IS THAT NOT A COVERING FUNCTION??
![-- True if two Lists are equal
listEq : List (Eq a) -> List (Eq a) -> Bool
listEq a b =
case (a, b) of
([], []) => True
(_::[], []) => False
([], _::[]) => False
(a1::ar, b1::br) =>
if a1==b1 then
listEq ar br
else False
It fails with: Can't find an implementation for Eq (Eq a)](https://files.mastodon.social/media_attachments/files/117/471/049/684/037/001/original/c92ffad76cd42b39.png)
Oct 20, 2026, 3:20 AMAt about this point a very nice types.pl user replies to point out that the reason my original == code, with Data.List.Equalities, did not work was because I mixed up |> and <|. Again.
…I…
I'm frustrated. At this point. I'm not concentrating well. I'm trying not to mention "COVID-19 post-viral syndrome" in this thread, or how much Benadryl I'm on.
Okay. Okay. It works now. As long as I run "pack exec". Which means I am now banned from getting error messages in the command line. Okay. Fine.
Oct 20, 2026, 3:22 AMPlease excuse me for my unprofessional outburst. With regard to whether my "listEq" implementation was a covering function. Although I'm still right.
EDIT: Im wrong. I was given a counterexample. I think what I should have matched in cases two and three was (_, []) and ([], _); since the case ([], []) was already excluded, those patterns can only match "lists of 1 or more items" in the _ positions, and it will work. I did not test it.
Oct 20, 2026, 3:26 AMAlso this… this is correct. This is absolutely correct. The problem was my |> / <| mixup, not which modules I had imported, and I don't have any need whatsoever for contrib, so I'm out of `pack` jail now. Okay. Alright. That's good. Okay. https://types.pl/@ionchy/117471091626868051
[QRT inset not provided because of the Mastodon 5 GUI reset dropping tomorrow. I've switched to masto-fe and can no longer quote boost.]
Oct 20, 2026, 3:28 AMHey question if in Idris you feed the |> function into the <| function, like you execute <| |>
Does it unlock a quantum computing library
Oct 20, 2026, 3:41 AMSo. The story so far: In part 1, I made an emulator for a gross ass mini CPU. I'm given a program for it. In part 2, AOC guy informs me this program is SUPPOSED to be a quine, but it has a bug; the initial "register A" value is wrong. I need to find the A that reproduces the program. So I run the program in a loop, incrementing A each time until the program output equals its own code. I know this works; it works on the sample.
But on my *assigned*program… well…
![lots of lines like "Success 15943678 [5, 0, 7, 7, 1, 1, 1, 3] eq? True"](https://files.mastodon.social/media_attachments/files/117/471/145/171/189/637/original/b89ed1a7654a51f8.png)
Oct 20, 2026, 3:44 AM(Ignore the "eq? True" there, I forgot a "not", it's repeating until it prints False).
I didn't finish my program, as of this second. I didn't get around to implementing the code to recover after invalid-program or infinite-loop failures (but that's ok, because it appears those failures never never happen on the program input). I have it printing output on every line, and STDOUT is *definitely* slowing me down.
Looking at the output, it's clear I don't need any of that.
Oct 20, 2026, 3:47 AMAlthough there are many programs this "cpu" COULD execute, the AOC guy clearly designed it to run this one program, or variants on this one program. The program is clearly expressing some function. You can like… *see*, the relationship between input (A value) and output (printed list). It's not linear, or smooth, but it's close. It's hard to express from a screenshot. I can see the output string herky-jerky growing as A linearly increases.
Oct 20, 2026, 3:51 AMThe instruction set consists of a function that divides A by two, and a bunch of XOR ops. There's a jump function that jumps if A is nonzero. Implication: A is like a sort of logarithmic counter; the program whittles away dividing repeatedly by two until A hits zero. It's very clear the number of output digits scales linearly with the number of digits in A.
This means a linear scan is out. After running a pretty long time, my output has 8 digits. My target string has 16.
Oct 20, 2026, 3:56 AMSo even if I'm more efficient and am not waiting on STDOUT, I can't (shouldn't?) count up to 16 digits by hand.
However, I'm *mostly* sure I can do something like a binary search. The XORs mean the output isn't smoothly increasing, but it's increasing on average, so a binary search will get me into the neighborhood, and maybe that'll identify a block of, I dunno, a thousand or a hundred "A" values that I can linearly scan and find my result.
…tomorrow.
Oct 20, 2026, 6:21 AM…okay. I am *completely certain* the correct answer is somewhere between 35,184,372,088,831 and 281,474,976,710,656, noninclusive.
Oct 20, 2026, 6:27 AMI'm laying in bed. I think about how the values in the input/output lists are all in the range 0-7, and wonder if the AOC taskmaster wants us to be thinking of them as an octal number.
I think about "comparing" lists. I realize I don't know which end to compare from. I make a decision. I get up and start doing a *manual* binary search. Why not?
I quickly find the numbers don't behave the way I hoped. Most numbers I pick turn into long strings of 4s, for some reason.
But.
@mcc The most educational approach is probably to do it all three ways:
1. normal recursive techniques
2. IO monad imperative program
3. Roll your own monad encapsulating the boilerplate from (1) that hopefully shows that the structure from (2) is not tied to IO, but to accumulating some state in the background and having some kind of unwind opration.
Folks will tell you to use monad transformers or effect frameworks. But I don't think that's nearly as educational as doing (1) and (3).
@mcc Monad transformers, effect handler libraries etc all solve the "I'm tired of writing boilerplate monads by hand" problem that you don't have yet. After like the 5th or 6th time you have to do the same return and bind implementation, it might be worth a look. But tbh it's diminishing returns and just endless endless navel-gazing
Oct 19, 2026, 4:39 PM@lambdageek It is good thinking! One thing of note is that I need some kind of pause/resume feature ANYWAY, so that if one of my runs takes "too long" https://mastodon.social/@mcc/117468548012596862 I can come back to it later.
One option would be to write the "normal recursive"/OCaml version first because I'm certain i can finish it within my time limit, and I can return latre and do the more-complex version without time pressure and AFTER reading, like, a book or three about this.
@mcc Good news: coroutines are also a monad.
Bad news: I'm not sure there's a good way to arrive at the coroutines monad in a natural way from how you'd write the "normally", unless you just write all your code in continuation-passing style by default.
Also in this case doing the "IO monad imperative program" version is probably going to be a dead end because I think refactoring it out into a pause/resume version is not going to be very natural.
Oct 19, 2026, 4:54 PM@lambdageek "coroutines are also a monad"
Oh, I am *so* happy to hear that.
And I think I was unclear, the halt/resume version is something I believe I can implement with Either. Like, I can implement that without even changing the program much using only features that exist in OCaml.
Oct 19, 2026, 4:55 PM@lambdageek Hm, I wonder if anyone in functional space has implemented the Amb monad with multithreading.
@mcc
The length of the expected output list is known. So the program might die if this length is exceeded by the output list.
Yes, this feels hacky, but somehow you need to solve the halting problem.
And if you're at it, you could of course break an evaluation as soon as the output is not a prefix of the expected output.
So the CPU might keep the list of "expected remaining output" and "consume" it upon fitting output.
Oct 19, 2026, 6:40 PM@hcschuetz Hey, that's a good optimization. And it did occur to me another potential optimization is to cache previously seen states (only 4 registers; not so hard) and abort if i detect a loop. However I think I could still run in a *very* long loop using only loops and slowly modifying one of the registers in a non-repeating or increasing fashion. It would be hard, given the operators, but not out of the question.
Oct 20, 2026, 3:12 AM@mcc brb constructing a gender that's conditional on other people's gender. Requiring a gender fixed point to deduce
@mcc really
@mcc perl has the "spaceship" operator, it only makes sense that somebody else would have the Cosmic Ark operator
Oct 20, 2026, 12:26 PMHah, I dropped into the thread with @rotopenguin's post, expecting some light-hearted programming-language humor, not some "Epic trials of MCC" thread with 1.414×10⁴ posts 😆
You have a great deal more fortitude for this adventure than I would ever have, but it sounds like you're having fun and learning stuff which is the important bit 😁
Oct 20, 2026, 12:56 PM@gumnos the other "weeks" in this project have not gone off the rails in quite this way
@mcc what about listEq [] [1,2] or listEq [1,2] []. these are not handled in the case blocks above. (the left hand side of the two False cases is not general enough).
also it couldn't find Eq int because int is not Int (need to capitalize type names, lowercase types are type variables)
Oct 20, 2026, 3:36 AM@typeswitch Thank you very much.
Oct 20, 2026, 3:24 AM@jannem I think the language is mostly used in academic contexts
Oct 20, 2026, 5:57 AM@mcc Disregarding my previous promise to know what I am talking about:
For your code that starts with
listEq : List (Eq a) -> List (Eq a) -> Bool
I think the interface restriction needs to be written like this:
listEq : Eq a => List a -> List a -> Bool
For your specialized integer code, I think you need to capitalize your int as Int or maybe Integer (so List int should be List Int)
Both these suggestions based on what I skimmed at https://idris2.readthedocs.io/en/latest/tutorial/interfaces.html
As for the covering, I don't know.
I really like following you Idris 2 adventure, I wish to learn it myself some day.
I remember my intense struggles and frustration when learning Haskell a long while ago.
Oct 20, 2026, 6:19 AM@jjj Oh… oh that sounds right
@mcc well the list equality comparison seems to have worked since it says the thing with the red squiggle has type Bool
it's expecting something of type (?a -> ?f ?a) -> ?b so that's just what (|>) takes as the second argument, but why do you have that there anyway? pure (list1 == list2) should be enough
Oct 20, 2026, 3:21 AM@ionchy Thank you very much.
I got addicted to @@ back in the SML/NJ days…
@mcc also if you want boolean equality on lists (==) should just work without importing anything because it's provided by the Eq typeclass https://idris2docs.sinyax.net/data/prelude/docs/Prelude.Types.src.html#line391 so if a has an Eq typeclass then so does List a automatically
Oct 20, 2026, 3:26 AM@ionchy Okay, that's great. Thanks again.
@mcc Based on what I can see of your program, I think the issue is with `|>`, since that's reverse function application: that is to say, `5 |> show` is effectively sugar for `show 5`. That means you're trying to take the result of `output == cpu.prog`, which is `Bool`, and apply it as a function to the value `pure`, as though you wrote `(output == cpu.prog) pure`.
Again, I can only see what's not obscured, but with those assumptions, I think you might just want `pure (output == cpu.prog)`?
Oct 20, 2026, 3:21 AM@aysamanra You are absolutely correct.