Login
You're viewing the mastodon.tn public feed.
  • mccmcc@mastodon.social
    Oct 24, 2026, 8:28 PM

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

    💬 2🔄 0⭐ 0

Replies

  • mccmcc@mastodon.social
    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/@

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

    Remember my feral list equality function that turned out to be unnecessary? Well it's back, and it compiles now, and is actually useful. This would probably look more satisfying as code if the first three clauses returned "=> True => False => False" but I actually do need the asserts.

    I think…if I write a function that converts a list of octal digits into a number possessing those octal digits…the program will just work. I think it will work on the first try. Unless I forgot a "reverse". Or two

    -- True if two Lists are equal up to first n elements listPrefixEq : Eq a => Nat -> List a -> List a -> IO Bool listPrefixEq n a b = do if n == 0 then pure True else case (a, b) of ([], []) => die "Matching prefix, both lists exhausted with \{show n} left" (_, []) => die "Matching prefix, right list exhausted with \{show n} left" ([], _) => die "Matching prefix, left list exhausted with \{show n} left" (a1::ar, b1::br) => if a1 == b1 then listPrefixEq (minus n 1) ar br else pure False
    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 25, 2026, 2:31 AM

    …wait a minute. Isn't what I want just foldl with `λ x y = (x << 3) | y`?

    export octal_fold: Bits64 -> Bits64 -> Bits64
    octal_fold a b = (.|.) (shiftL a 3) b

    So I just plug that in and…

    … what?

    (This one went away if I cast [1,2,3,4] to List Bits64 but I can still be annoyed about it. By the way, OCaml likes foldl and Haskell likes foldr, right? Which one does Idris2 prefer?)

    Main> foldl octal_fold 0 [1,2,3,4] Error: Ambiguous elaboration (on the array 1,2,3,4). Possible results: [1, 2, 3, 4] [1, 2, 3, 4]
    💬 2🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • gaytabasedysfun@treehouse.systems
    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
  • mccmcc@mastodon.social
    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
  • mccmcc@mastodon.social
    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
  • Sophie of Ratsnake Gamesratsnakegames@mastodon.social
    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
  • Cadentarix29@tech.lgbt
    Oct 25, 2026, 2:46 AM

    @mcc the foldl vs foldr thing is mostly about strict vs lazy. Foldl is better strict and foldr is better lazy. That's why foldl is better in OCaml and foldr is better in Haskell (except Haskell also has foldl' which is a strict foldl). As Idris is strict by default I believe foldl would be preferable

    💬 0🔄 2⭐ 1