Conversation

Notices

1. Embed this notice
   mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:32 JST mcc

   #BabelOfCode 2024
   Week 11, Puzzle 17
   Language: Idris

   PREV WEEK: https://mastodon.social/@mcc/114582208242623432
   RULES: https://mastodon.social/@mcc/113676228091546556
   PUZZLE TEXT: https://adventofcode.com/2024/day/17

   Now getting extreme with "puzzles out of order". Here's the problem. The AOC author *really* likes puzzles involving 2D arrays. It makes sense. They're easy to visualize as either ASCII art or PNGs. They're a rich space for "simulations". But some languages are better at them than others.

   So for Idris week, I pick the "build a CPU" puzzle.

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:27 JST mcc

     in reply to

     27 hours after beginning this thread, I successfully write my first line of Idris code. (It's opts <- getArgs). Now I just need to figure out how to get an item out of a list.

     There's a better looking options parser in the standard "contrib" library, but I can't figure out how to get it out. I decide to dip a toe in the idris Zulip.

     https://idris-lang.zulipchat.com/#narrow/channel/556789-help/topic/Newb.20questions.3A.20confused.20about.20importing.20packages/with/631826383

     Among the deficiencies in the tutorials: They describe how to find third party libraries, but not how/where the stdlib is used/documented…

     GreenSkyOverMe (Monika) repeated this.
   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:27 JST mcc

     in reply to

     Tried to write my second line of Idris. Disaster.

     It's highlighting "=>" and giving the error "Expected '=>'". Don't know how to proceed.

     Part of the problem is Idris has elaborately documented its upgrades from Haskell, but the tutorials kinda handwave the basic stuff. In ML I'd expect to deconstruct a one-element list like [x] or like x::nil. In Idris I… I don't know. Maybe if I sleep and reread all the docs.

     Also, I'm missing how I, inside of a do, "abort the do block/program with error"

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:28 JST mcc

     in reply to

     After some poking, it turns out that installing Idris2 in Racket mode, then uninstalling with the given instructions, then re-installing in Chez mode, leaves the system in an inconsistent state where it sometimes uses Racket and sometimes doesn't work at all. I need to stress I have various community members and maintainers in my mentions trying to help me and they're being very nice. They give me hand-surgery to perform on a TOML file. It ixes it. Compiling takes 1.4s instead of over 2 minutes.

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:28 JST mcc

     in reply to

     Furthermore, it appears that in addition to the two tutorials I mention above, the ones linked from the regular Idris website, there is a third, secret tutorial, and this one explains how to actually execute a piece of code, explains why readline isn't working right in the idris2 repl, etc. https://codeberg.org/jjl/tutorials/src/branch/main/00-setup.md

     I guess I can move on now. Hopefully there aren't more nasty surprises lurking in my toml configuration file (presumably lying in wait to blow up if I attempt to configure an LSP).

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:28 JST mcc

     in reply to

     So Sublime Text doesn't have an Idris LSP package-- only an Idris syntax highlighting package.

     But it turns out if I `pack install-app idris2-lsp, then in Sublime go to Package Settings -> LSP -> Server Configurations

     {
     "idris2-lsp": {
     "enabled": true,
     "command": ["/home/mcc/.local/bin/idris2-lsp"], // Update the PATH
     "selector": "source.idris"
     }
     }

     It just like… magically works. I have type-on-hover now. As long as I create a .lidr file with idris2 --init.

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:29 JST mcc

     in reply to

     Among the things not mentioned in either Idris tutorial

     - What file extension is used for Idris files? (it's .idr)

     - How do you execute an idris file?

     Running idris2 puts you at a REPL. Running "idris2 src/puzzle.idr" churns a long time, creates a series of utterly baffling files in a build/ subdirectory, then drops you at the same repl. "-c" does this then quits; but it still does nothing useful.

     One tutorial implies "pack -o hello exec src/puzzle.idr" will do something; this hangs forever

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:29 JST mcc

     in reply to

     I understand true LISP heads are comfortable just spending all their time in a REPL forever. I am not a true LISP head. I'm an ocaml poser.

     I *think* the mysterious "pack" command, while hanging, created in the mysterious "build" subdirectory a "hello.rkt" file that wouldn't have been there otherwise. I remember someone saying idris works by transpiling itself to a "backend" lang, so maybe I'm supposed to figure out the non-hanging args to "pack", transpile, then execute the rkt file in racket.

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:29 JST mcc

     in reply to

     *Rubbing eyes* okay, so

     idris2's command line --help lists a "-o <file>" flag, which "specifies output file". Output file for what? Apparently this actually means "build an executable, put it in ./build/exec [path non-negotiable], and name it <file>".

     I run this. I run it in `time`. It does create a runnable Linux executable.

     It takes it one minute and fifty-three seconds to compile the program:

     main : IO ()
     main = putStrLn "Help"

     During which time I sincerely could not tell if it had hung

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:29 JST mcc

     in reply to

     So after a brief conversation with Idris2 maintainers

     - Idris can run on top of either "Racket" or "Chez". I went with Racket because I thought it was the fast one. This is no longer true. The maintainers expect Chez to be a little faster. In fact it's hundreds of times faster. This surprises the maintainers.

     - Additionally, in Debian, Chez takes up 10% the disk space of Racket.

     After what I'd consider a somewhat unfriendly uninstall procedure, I re-install idris2, atop Chez.

     It doesn't work

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:30 JST mcc

     in reply to

     Okay important question

     I have a vague sense Haskell has "monads" and Idris has "applicatives". Idris in fact seems to have both— https://idris2.readthedocs.io/en/latest/tutorial/interfaces.html#idiom-brackets

     If I say "do" I've made a monad and if I say "[| … |]" (ugh, ocaml at its worst) that's an applicative. Difference isn't clear. If I just write monads and ignore [||] in my learning-Idris program am I Missing Out?

     I still don't know what an Effect is. I thought it was the Effect Monad but the Idris manual talks like applicatives are Effects.

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:30 JST mcc

     in reply to

     Okay so the important things seem to be this comment

     https://social.treehouse.systems/@dysfun/117441025783295712

     the second screenshot (the terminal shot) attached to this post

     and this comment

     https://mastodon.social/@porglezomp/117441075637749928

     I still don't understand it, but I think I'm closer to understanding it than I have been ever in the last 25 years. Just gotta think about those type signatures. And in the meantime I don't *have* to understand it, I can just use do notation and worry later about which Math Things my code corresponds to.

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:31 JST mcc

     in reply to

     So.

     I install Racket. Wow! Racket takes up a lot of space! I guess I'll need this for week 14 anyway.

     I install "pack", Idris's dedicated package manager. I guess I don't get to be happy Idris uses an existing package manager anymore. Installation for the Idris package manager is "curl to bash". The bash script clones a git repo. There is weeping and gnashing of teeth. There is no way I will remember to uninstall this thing or remove it from my bashrc files when this project's done. Whatever.

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:31 JST mcc

     in reply to

     Anyway! Idris! I'm in!

     Idris is a "dependent types" language. "Dependent types" are the thing your favorite language doesn't have that prevents you from having that feature you wished it had but it doesn't. A running gag in Rust is every desirable but missing feature would be possible with dependent types. DT means a type can contain a value, or do ops on values, for example a function that adds an array of length N to an array of length M and produces an array M+N. Like Ada, but… … … better?

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:31 JST mcc

     in reply to

     For some reason Idris has two tutorials.

     https://idris2.readthedocs.io/en/latest/tutorial/index.html
     https://idris-community.github.io/idris2-tutorial/

     Reading how they describe their types, I wonder if the CPU emulator puzzle was the wrong choice for this language. Something with arrays might've better exercised Idris' capabilities?

     First thing that catches my eye; it has an "infix" sugar like ML. But then they say:

     "Functions, data constructors, and type constructors may all be given infix operators as names."

     TYPE CONSTRUCTORS MAY BE INFIX

     HECK YES

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:31 JST mcc

     in reply to

     Unsorted thoughts

     "Holes are useful." is a funny sentence to see in a manual

     "where" and "let" seem redundant

     > Nested record fields can be accessed using the dot notation:
     >
     > x.a.b.c
     > map (.a.b.c) xs

     …Haha heck nice, that was the feature I was proudest of in Emily

     "multiplicity 0" (calculated/erased at compile time) and "multiplicity 1" (linear typing) sound like things I VERY MUCH want in a programming language, though the ergonomics around it are a little alien to me, a C/Rust girl

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:32 JST mcc

     in reply to

     Idris is "Haskell, but more so". Haskell is "ML, but more so". I have always liked ML. I have never liked Haskell (although when I tried it again for this thread series, I enjoyed it more than I expected). I have always suspected I might like Idris more than Haskell. Maybe the awkward concepts in Haskell aren't *awkward* just *incomplete*. Maybe another language could complete them.

     Conveniently, Idris installs itself through the Haskell package manager, which I already installed for week 7!

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:32 JST mcc

     in reply to

     Inconveniently the Haskell package manager doesn't fricking work.

     What… I don't understand what this very long error message is telling me. Do I need to upgrade Cabal? Do I need to downgrade Cabal? Is some existing package I have selected in a version incompatible with Idris? I can literally blow away my entire set of installed Haskell packages, I don't mind. Would that help? :(

     EDIT: A six year old Google Groups comment reveals the secret is to pass cabal the flag "--allow-newer". Terrifying

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Thursday, 15-Oct-2026 14:28:32 JST mcc

     in reply to

     More updates.
     - Passing --allow-newer, perhaps unsurprisingly since.
     - I look closer to the tutorial. It links a github.
     - The github is archived.
     - I back ALL the way out. Instead of searching "idris tutorial" I go to the Idris home page. I then discover
     - I have been looking at the Idris 1 tutorial. Idris 1 is discontinued. New thing is Idris 2.
     - Idris has a totally different tutorial and is now deployed via Racket instead of Haskell (?!??)
     - I have been, apparently, barking up a dead tree.

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:27 JST mcc

     in reply to

     I'm really struggling with my docs for this language being two "tutorials" I'm juggling constantly.

     I have a

     case operand of
     0 => 0
     1 => 1
     2 => 2
     3 => 3
     ...

     I would like this to be

     case operand of
     0 | 1 | 2 | 3 => operand
     ...

     neither | nor repeating => is allowed here. Both tutorials skim the definition of a "pattern".

     Is there like a … language spec I could be reading here to get *exact* syntax? A BNF? Maybe the source is just readable. Should I read the source?

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:27 JST mcc

     in reply to

     I'm keeping a list of "issues to file on idris2 when I am done with this project" and HOO BOY am I ever filing this one (second time hitting)

     GreenSkyOverMe (Monika) repeated this.
   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:27 JST mcc

     in reply to

     Okay so I'm probably sounding like a broken record at this point but.

     I want to xor two numbers. I find an "xor" in Data.Bits.

     https://idris2docs.sinyax.net/data/base/docs/Data.Bits.html#Data.Bits.xor

     Doc says xor is "Fixity Declaration: infixl operator, level 6". I guess that means it's an infix operator. Wrong. 📎1

     xor a b => right

     Apparently… infixl means… "infix left"? So not infix?

     *A frustration is I feel like I can't interpret docs without having other docs open.*

     Oh, also Nat doesn't conform to the Bits interface. So I'm stuck. 📎2

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:28 JST mcc

     in reply to

     Was trying to figure out how you destructure a record type in Idris and the answer turned out to be that you use *the constructor function* on the left hand side of a =. I am both impressed and frightened.

     (…because it seems to imply this language has reversible computations when it doesn't quite, this is just a pinch of sugar.)

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:28 JST mcc

     in reply to

     Update NOPE I did not in fact find the "index into a list" function. Because the index into a list function only exists if you can provide a proof that the index is less than the length of the list. Wait, but I don't know the length of the list? I was hoping the standard library would take care of that for me.

     Experimentally, I try calling the inBounds function. It… something weird happens. It returns a "dec". Frustratingly, one of the types that isn't linked to its definition in the docs (1/2)

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:28 JST mcc

     in reply to

     But per :doc it appears to be a predicate function. I *think* I don't call inBounds, I think I somehow *define* inBounds.

     I think my options are:

     1. Ignore "index"; write my own index that manually skims the list & returns an Either

     2. Convert my list to a Vector, somehow, with its length as a generic parameter, somehow, and then when reading from the list test if my index (input from file; out of my control) is less than that generic-parameter length.

     2 sounds better, but harder *_*
     
     (2/2)

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:28 JST mcc

     in reply to

     A proof that the natural (ip+1) is in bounds for array a is not a proof that the natural (ip) is in bounds for array a.

     :(

     :(

     :( :( :(

     EDIT: [sad rageface ok face] ok https://tiny.tilde.website/@crazazy/117458043829746469

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:29 JST mcc

     in reply to

     Hey question, does Idris have an equivalent of Ocaml |>

     (I think this was "@@" in SML/NJ? And possibly $ in Haskell?)

     EDIT: Yes… ha ha ha… yes! https://social.treehouse.systems/@dysfun/117457314797528981

     EDIT 2: In all the programming languages we write myself I just use ":" for this. It's that important to me. Nobody else I talk to ever seems to think this is good syntax

     EDIT 3: Wait it isn't working

     EDIT 4: Oh wait I asked the wrong question to start with. It's <| not |>

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:29 JST mcc

     in reply to

     Haha what

     https://idris2docs.sinyax.net/data/prelude/docs/Prelude.Basics.html#Prelude.Basics.the

     I'm not sure whether I understand it, but I love it

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:29 JST mcc

     in reply to

     You know you're using a functional programming language when you read through a module documentation containing about fifty functions trying to find the one that lets you look up a list member by index, and do not find it

     https://idris2docs.sinyax.net/data/base/docs/Data.List.html

     (I found two functions for getting the list index given a value, but did not find the function for getting a value given a list index. Not sure if my eyes glazed past it or if it's somewhere surprising in the Prelude)

     EDIT: I think it's "index"

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:30 JST mcc

     in reply to

     Idris question

     Does this language have a "map_left" or "map_right". Like Rust map/map_err ( https://idris2docs.sinyax.net/data/base/docs/Data.Either.html#Data.Either.eitherMapFusion ). I want to do a transformation on a Either, but I want to apply the transformation iff it is Right. I think I could write this myself if I had the mastery required to do… the things I'm already failing at. I notice there's an "eitherMapFusion" https://idris2docs.sinyax.net/data/base/docs/Data.Either.html#Data.Either.lefts with no human-readable documentation and a baffling type. https://idris2docs.sinyax.net/data/base/docs/Data.Either.html#Data.Either.eitherMapFusion

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:30 JST mcc

     in reply to

     adsfkjdsglkjfdgljag

     https://github.com/mcclure/aoc2024/blob/d15c57397feea3bcdec11182c61dd00610181bc4/17-01-cpu/src/puzzle.idr

     After *three* days, I have written a 65-line program that parses a very simple text file in a very simple way in Idris, which is the *prerequisite* to *starting* the puzzle I was hoping to finish within the week. And I was only able to achieve this much through massive personalized help. I will now time myself trying to write an equivalent program in Perl:

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:30 JST mcc

     in reply to

     perl -e 'open(FH, $ARGV[0]) or die "No file"; ($a,$b,$c) = map {(chomp && scalar(/^[^ ]+ [^ ]+ (\d+)/ or die "Invalid register: $_"), $1)[1]} (scalar <FH>, scalar <FH>, scalar <FH>); <FH>; $program = <FH>; chomp $program; @program = split(/,/,$program); undef $program; close(FH); print "$a, $b, $c, program length " . +@program . "\n"' data/sample-4,6,3,5,6,3,5,2,1,0.txt

     That took 12 minutes. 3 minutes to write the program and 8 minutes to debug it (It didn't work because I forgot "scalar".)

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:30 JST mcc

     in reply to

     Now, a thing of note— I'm not coming in Idris "the expected way". The expected way would probably be to read through both those tutorials fully, The Conor McBride lecture notes on applicative programming, spend lots of time in the repl making sure I fully understand the Concepts, and then probably use a combinator parser library out of the Idris libraries list instead of hacking it with split(" ") and split (","). Probably it's unusual to just roll up to the compiler and go "I'MA DO TEXT IO NOW"

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:31 JST mcc

     in reply to

     2. It reeeeeallly bothers me that I'm using Either for error handling because it is not semantic. I'd like success to be Ok and failure to be Err. If I kept using Idris, how hard would it be for me to make an interchangeable Result version of Either with different names?

     3. My code used a `map`. Therefore in order to bubble up errors, I need a way to "terminate" a map early. It turns out this exists and it's called "traverse". It furthermore turns out TRAVERSE TREATS LEFT AS ERROR

     (CONT'D)

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:31 JST mcc

     in reply to

     AND RIGHT AS SUCCESS. SO ONE (1) FUNCTION SWAPS FAILURE/SUCCESS BETWEEN LEFT AND RIGHT. I'm not asking for help here I'm just annoyed

     4. Here's the point I actually need help: As you can see from "z_error.txt" in the above-linked gist, traverse can't operate on a List1.

     …what?!

     …what's even the point of higher-order functions over interfaces¹ then :( :( :(

     I'm stuck. What should I do here? Write a function to convert List1 to List? List1 *is* a superset of List…

     ¹ "Typeclasses"

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:31 JST mcc

     in reply to

     Answers to above questions

     2. It turns out in Idris Left semantically means `Error` and Right semantically means `Ok`. Every standard library function follows this convention.

     3. See 2

     1. Just `do` when the return type is Either and any <- that attempts to assign Left auto-aborts. Like every line has an implicit ?. Awkward compared to ?, but better than nothing.

     4. The actual error was ") in wrong place"— hard for any compiler to explain. Correct ) gives better error. Also: Data.List1.forget

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:31 JST mcc

     in reply to

     Idris is a "Right-Wing" programming language; any utterance of a Left idea results in immediate termination

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:32 JST mcc

     in reply to

     RE: https://mastodon.social/@mcc/117451514800968529

     So my understanding of haskell "monads" is that they're really just very fancy syntactic sugar for wrapping each line of code in some kind of transformation. Usually the monad is "IO" because the transformation is a magic "wait for external input".

     It seems like I ought to be able to use a monad to do wrapping similar to Rust Result<>?, and not have to go all the way to IO, and still have a pure function. Someone said Either is a monad.

     Someone says, "you can use error"—EDIT: No,that's Haskell

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:32 JST mcc

     in reply to

     Okay. So. The consensus from Idris users is to manually bubble the errors up using Either, like I'm a barbaric Rust user or something. I hit several problems.

     https://gist.github.com/mcclure/a7498deb38a0ff082d09294169c39aeb

     1. Either and Maybe are monads. I've been told this since 2010. That implies I should be able to "do" them. I should have some way of rigging stuff so that, when a operation fails, "aborting" it like ? in Rust. Instead like chaining case statements like I'm a barbaric Ocaml user. Am I missing something?

     (CONT'D)

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:33 JST mcc

     in reply to

     Okay so I *think* I managed to fix the "monad" errors in this, and I'm proud of that

     https://gist.github.com/mcclure/8c6baaa09dd8c94c0c7787b367e00ee8

     But I am utterly defeated by the error "Mismatch between: AsList (strCons ?_ ?str) and List1 String." (a later error gives this as "Mismatch between: List ?a and List1 String."). I thought ? meant there was a hole. But I didn't write any holes

     Hey is there a builtin "dispose" function in Idris. Like _ -> () if I want to end my do block with a value but I'm not ready to do with anything

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:33 JST mcc

     in reply to

     *Rubbing eyes* okay. Okay.

     So what I wanted is a List String. "split", the string function, returns a List1 String. I assumed the 1 was "noise". Using this language, I find a lot of "noise" in the messages and docs.

     No, it was very important.

     So to construct or deconstruct a list in a post-LISP FP language, you use :: , right? Everyone knows that. Right before I went to bed last night, I got a message saying I needed to use ::: , not :: . I literally assumed this was wrong. No, It was right.

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:33 JST mcc

     in reply to

     What I *should* have done, when the split doc said List1, is look up what that was. I mean, I did, and it said a List1 is just a List with at least one element. That sounded normal to me. Idris is all about the dependent types thing, right? So logically this should just be a List with some constraint on it. I assumed it would work like a List.

     No, it's different. To interact with it you have to import Data.List1, then use ::: instead of :: .The [a,b] sugar will not work.

     I… hm. Hrm. Hmrmrmhf

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:33 JST mcc

     in reply to

     One thing that concerns me: What if, for some reason I can't currently guess, I needed a List which is dependently typed to have at least 26 elements? Would I define a List26, and assign it :::: , and hope it doesn't conflict with someone else's List4 which also defined a :::: ? Starts feeling weird

     Anyway, now onto the next problem: DYING IS A SIDE EFFECT. WHAT DO YOU MEAN DYING IS A SIDE EFFECT. LIKE OK IT IS BUT I SHOULD BE ABLE TO DIE ANYTIME I WANT. I'M NOT ALLOWED TO DIE WITHOUT A MONAD??

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:34 JST mcc

     in reply to

     …did this compiler just *apologize* to me

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:34 JST mcc

     in reply to

     A big problem I'm having, and I can't tell if this is a problem with Sublime Text or a problem with idris, is that if there is even on error anywhere in the program the LSP will not do type inference on anything in the program at all. Which makes sense if you think about it because if there's an error it can't infer types. But also kind of HURTS, A LOT because normally the way I'd resolve a typing error is by mousing over each variable in the expression to see what its type is and if I expect it

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:35 JST mcc

     in reply to

     RE: https://social.treehouse.systems/@dysfun/117447164214916123

     OK so this is great but also, it speaks to what I perceive as a "missing low-end" in the Idris docs— like, if I want a high-end library for doing command-line argument parsing I can find that in seconds in the well-curated third-party libraries list and install it via Pack, but if I want to know the name, package and type signature of the "getArgs" function in the standard library this is shockingly much harder.

     Maybe :doc will help some now that I know about it.

     https://mastodon.social/@dysfun@treehouse.systems/117447164251188241

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:35 JST mcc

     in reply to

     Oh no oh no oh no. it's my least favorite friend from OCaml— Spooky Type Action at a Distance

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:35 JST mcc

     in reply to

     Now, note, even I think I'm "doing this wrong"— what I would have *wanted* to do is put that big do block inside of a helper function that returns a string, and then have my actual app processing be a pure function that takes the string returned as and passes that through lines ("lines" splits a string on newline) and then does all the other operating. Maybe if I do that it will magically go away? Also I don't know what the "pure"s do and included them bc I copypasted from someone else's code.

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:35 JST mcc

     in reply to

     Okay for a moment there I thought I was going to have an opportunity to use a "fold" (people who understand functional programming but are not themselves primarily functional programmers become very excited whenever they get an excuse to use "fold") but then I found a way to do it with just map and I was like awwwww

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:36 JST mcc

     in reply to

     I am struggling with making sense of this language's standard library.

     The attached code works. It takes a filepath as argument and prints the contents.

     But

     - If instead of System.File.ReadWrite I use Control.App.FileIO, nine kinds of hell erupt

     - I can't figure out how to turn the FileError (Left x)https://idris-lang.org/Idris2/base/docs/System.File.Error.html#System.File.Error.FileError into… ANYTHING. I can't get that "Show FileError" to do anything in the repl. "import" in the repl fails

     - In general, I can't search prelude/base for a symbol by name?

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:36 JST mcc

     in reply to

     Moreover, I don't want to put the file contents into a string. I want to parse them in a very simple way— verify text "Register A:" at start of line one, parse comma-separated list, move on to line two etc. I don't know how to get "here's a list of string ops" "here's a list of file ops". I find this https://idris-community.github.io/idris2-tutorial/Tutorial/IO/Files.html it's explaining concepts of applicatives and I want to know what operations exist for simple parsing of strings. I don't know what "go" does or where to look it up.

   • Embed this notice
     mcc (mcc@mastodon.social)'s status on Sunday, 18-Oct-2026 06:38:37 JST mcc

     in reply to

     Okay making some progress with help from Mastodonites but

     *gestures at below screenshots*

     Why