Login
You're viewing the slime.global public feed.
  • mccmcc@mastodon.social
    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…

    💬 1🔄 0⭐ 0

Replies

  • mccmcc@mastodon.social
    Oct 20, 2026, 2:59 AM

    Oh right, I was going to ask a question. Any Idris users awake? Two part question.

    1. idris2docs.sinyax.net/data/con 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?

    💬 2🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:01 AM

    Wait. Wait. Hold on a friggin minute

    Computer

    Enhance

    … this type is assigned female at birth ????

    zooming in on the error message...
    (?a -> ?f ?a) -> ?b
    💬 2🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:17 AM

    Okay. 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)
    Same function but "Eq a" is replaced with "int". Error: "Can't find an implementation for Eq int".
    Same again but "int" is replaced with "Bits64". It says "main,listEq is not covering"
    💬 2🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:20 AM

    At 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.

    💬 2🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:22 AM

    Please 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.

    💬 2🔄 0⭐ 2
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:26 AM

    Also 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. types.pl/@ionchy/1174710916268

    [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.]

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:28 AM

    Hey question if in Idris you feed the |> function into the <| function, like you execute <| |>

    Does it unlock a quantum computing library

    💬 2🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:41 AM

    So. 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"
    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    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.

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:47 AM

    Although 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.

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:51 AM

    The 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.

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:56 AM

    So 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.

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    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.

    💬 2🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 6:27 AM

    I'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.

    Page full of numbers and comma-separated strings of numbers.
    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 6:30 AM

    Treating my "goal" string as an octal number and looking at it in different bases revealed nothing interesting.

    A regular binary search really gets me nowhere. I think: Wait, isn't this math bitwise/logarithmic? I try doing a "binary" search picking midpoints with 10^((log10(a)+log10(b))/2). [block 1 in image above]

    That goes better, but not good enough. I quickly get two *broad* endpoints of my range, but can't reduce it further. [block 2 in image above]

    But then—

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 6:34 AM

    [block 3 in image above] I try looking at my input numbers in octal. I *immediately* realize that the number of printed "digits" in the output is exactly equal to the number of digits in my "A register" number represented as base 8. Hence: My answer will be n where
    octal 1000000000000000 <= n < octal 7777777777777777. 15 digits.

    This is the first concretely useful thing I've worked out so far.

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 6:39 AM

    I'm unsure what to do next. I still think I need to do some kind of directed search, but maybe instead of thinking about magnitude I measure bit similarity and toggle bits one by one. I imagine implementing this in JS and making 48 checkboxes for input bits I can play with. I imagine my linear scan emitting a Unicode bitmap.

    I have until 6 PM tomorrow to meet my one-week deadline.

    I worry I'm going to have to *read* the program and figure out what it's *actually doing*.

    💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 7:18 AM

    Okay. Here's the commented "decomp" of the program I'm executing.

    This is… not so bad. The only particularly "chaotic" step is 2. Critically, all of this math works on only one "octal" digit at a time. Each output "digit" is dependent on a single octal input digit, plus one other, *higher-magnitude* 3-bit slice cmhosen chaotically on step 2.

    This means, I think, if I start with the most-significant digit and work "right", each output digit will "lock" and not change again.

    Register A: [THIS IS THE NUMBER I'M TRYING TO FIND] Register B: 0 Register C: 0 Program: 0 2,4 B = A % 8 1 1,1 B = B xor 1 2 7,5 C = A / (1 << B) 3 1,5 B = B xor 5 [0b101] 4 4,1 B = B xor C 5 5,5 output( B ) 6 0,3 A = A / 8 7 3,0 if ( A > 0 ) goto 0
    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 7:20 AM

    There's a word for this. In cryptanalysis/security. There's a word for a very old type of attack where you're trying to guess a password, but you figure out you can get a confirmation if the first character of the password is correct, so if there are 26 choices for N characters the complexity to guess it is 26*N instead of 26^N. What the heck is that called. The term stopped being used in the 00s because nobody serious has made this mistake since the 1980s.

    💬 5🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • ROTOPE~1 ⭐️rotopenguin@mastodon.social
    Oct 20, 2026, 3:44 AM

    @mcc perl has the "spaceship" operator, it only makes sense that somebody else would have the Cosmic Ark operator

    Image attached toot
    💬 1🔄 1⭐ 0
  • Tim Ch-AI-se (now with bonus spooky) 👻gumnos@bsd.cafe
    Oct 20, 2026, 12:26 PM

    @mcc

    Hah, 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 😁

    💬 0🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 12:56 PM

    @gumnos the other "weeks" in this project have not gone off the rails in quite this way

    💬 0🔄 0⭐ 0
  • typeswitchtypeswitch@gamedev.lgbt
    Oct 20, 2026, 3:34 AM

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

    💬 1🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • jjjjjj@functional.cafe
    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 idris2.readthedocs.io/en/lates

    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.

    💬 1🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • masto UI updatechyionchy@types.pl
    Oct 20, 2026, 3:16 AM

    @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

    💬 2🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0