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]](https://files.mastodon.social/media_attachments/files/117/499/196/401/046/436/original/b31841581dd1b970.png)
Oct 25, 2026, 6:31 PMThis last bit of debugging would be going so much easier if I could just figure out why there is a documented module named "Libraries.Utils.Octal" which doesn't actually exist in the standard library. https://mastodon.social/@mcc/117471914682729495
Maybe I should give up and write my own int-to-octal-string function.
Oct 25, 2026, 7:34 PMSo functional programming likes linked lists, and the standard way to build a list in ML derivatives (which includes Idris) is not a ".append" like in C, JS, Rust but newelement::list, i.e., a prepend operation. This means functional programming involves a lot of generating a list then reversing it.
Anyway, what I've figured out is my automated solution search, now that it's finished, *actually* finds solutions which print *the target output, but backward*.
Sigh.
@mcc eager by default I believe, so foldl is probably nicer on your stack.
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
@mcc "A.I." slop or good old fashioned crappy documentation?
Oct 25, 2026, 7:29 PM@fiend_unpleasant It is an auto-generated documentation database in the style of doxygen, I believe based on inline doc comments.
@mcc sometimes SNOC lists are built in
Oct 25, 2026, 7:42 PM@pkhuong https://idris2docs.sinyax.net/data/base/docs/Data.List.html#Data.List.snoc
…hm. Well, next time I write something in Idris I'll consider that
Oct 25, 2026, 7:43 PM@pkhuong Is SNOC an immutable data type? I'd not heard of it
@mcc it's a cons list, but in reverse order (…)
Oct 25, 2026, 8:22 PM@pkhuong so, that implies every forward traversal is hiding a list?
Oct 25, 2026, 7:43 PMOct 25, 2026, 7:47 PM