Login
You're viewing the mastodon.tn public feed.
  • Oct 24, 2026, 8:27 PM

    Tolerable, but odd: Although I'm pretty sure I've successfully used the | operator for bitwise OR in actual Idris code, in the *REPL* I can only access bitwise OR by writing it as (.|.)

    No other sequence of characters works. Not `|`, not `.|.`

    ME: Hey I wanna do bitwise arithmetic

    IDRIS2: Okay, first draw me a picture of a butt.

    ME: …

    IDRIS2: Come on man, do it

    errors for
|
.|.
(.|.)
2 | 1

success for

(.|.) 2 1
    💬 4🔄 0⭐ 0

Replies

  • Oct 24, 2026, 8:28 PM

    I bet Kurt Vonnegut would have been really good at this language

    💬 2🔄 0⭐ 0
  • Oct 24, 2026, 8:42 PM

    An important thing I should probably note at this point: I perceive that I blew through the "my first Haskell program" puzzle with relative ease and then got bogged down something awful in the "my first Idris program" puzzle, and you'd probably get that same sense reading these threads. *But* it's possible that rather than this reflecting on Idris, it's only downstream from me picking puzzle 7 for Haskell and puzzle 17 for Idris and 17 being ~6 times as hard as 7. mastodon.functional.computer/@

    💬 2🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • Oct 24, 2026, 8:43 PM

    @mcc i would say that this challenge seems uniquely structured not to play to idris' strengths in particular, even.

    💬 0🔄 0⭐ 0
  • Oct 24, 2026, 8:45 PM

    @dysfun It actually is super suited to *some* immutable language because it involves a lot of forking decision trees. What language that should have been, I don't know. Definitely, if there's some kind of math idris is really natural at, it's not bit math.

    💬 1🔄 0⭐ 0
  • craboperand@todon.nl
    Oct 24, 2026, 10:25 PM

    @mcc @dysfun I haven't looked at the actual problem but "forking decision trees" sounds like the exact specialty of Prolog

    💬 1🔄 0⭐ 0
  • Oct 24, 2026, 10:27 PM

    @operand @dysfun the terms of the challenge is 25 languages i've never written a program in before. and i've written Prolog before.

    i think i have a couple logic languages on my candidates list. i'd like to learn kanren someday. i've tried a couple times and always go "ah! that makes sense! … how do i use it?"

    💬 1🔄 0⭐ 0
  • craboperand@todon.nl
    Oct 24, 2026, 10:38 PM

    @mcc @dysfun huh, i ddin't know about kanren even though Clojure's builtin logic programming is based on it and I used to teach a class that uses it. That's pretty cool.

    💬 0🔄 0⭐ 0
  • Oct 24, 2026, 9:05 PM

    @mcc i've been learning Haskell this past week (partially inspired by this thread) and now i have the itch to test this by doing this particular challenge in Haskell

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