jwaldmann

The implementation is literally (?) from (e.g.,) Cormen, Leiserson, Rivest: Introduction to Algorithms, Section 23.5 (ninth edition), and O(vertices + edges) is optimal. So this is about the hidden constant...

> ... All the nesting and unnesting of closures, required only to make it typecheck, (half jokingly) then fix GHC, instead of uglifying the code ... what are the real-life...

> it will involve changing every function, does it? transparent conversion between old and proposed new representation seems to me like the perfect use case for a pattern synonym -...

> ... performance problems with pattern synonyms that's what I meant: the proposed transformation may serve as a test case for GHC's inliner.

> I like to have that function in order to initialize a range as start set for a prime sieve. Really - und what do you need that prime sieve...

NB - this is how I install stdlib from scratch, automatically (in CI). it is a formalisation of what's already in the cited guide. ``` - wget https://github.com/agda/agda-stdlib/archive/refs/tags/v${STDLIB}.tar.gz - tar...

> This needs investigation. well then investigate it. follow hints at https://agda.readthedocs.io/en/stable/tools/performance.html what does the profile show? does this change with Agda version? I am interested in this topic (generally)...