[ performance ] rewrite-free concatMap

[gallais]

Simply removing rewrites took me down from a user time of ~1m8s to ~54s when running make test. The (small) code duplication in scan is a bit annoying.

We could have a core unindexed data structure and then only export pseudo-constructors with the right phantom arguments. Not sure it is worth it yet though.

A more principled solution would of course be to make sure the backend gets rid of the code corresponding to rewrites altogether!

[gallais]

Surprisingly, playing the same game with choiceMap (introducing an AltSame constructor and using it to remove the need for a rewrite) leads to a slower lexer.

[ziman]

Does this happen because the proofs are not erased properly or is there really overhead from calling replace?

[gallais]

I am not sure where to look to answer that question. My assumption was that the rewrites were kept as they are elaborated into auxiliary definitions AFAIU. But I only have a very limited understanding of Idris' architecture so far so this may be completely wrong.

[ziman]

You can run Idris1 with --dumpcases cases.idr and then look at the code generated for Text.Lexer.concatMap.

BTW, TT* replaces every call of f x with x if f can be shown to be an identity at runtime after erasure. This compiles away various things like weaken : Fin n -> Fin (S n) or replace : x = y -> p x -> p y. Maybe we could adapt this trick for Idris2 if identities turn out to be a bottleneck, but my bet would be on (non-)erasure of proofs rather than the identity overhead.

I'll have a look.

[ziman]

Looks like the easiest way is to put --dumpcases in idris.ipkg. The generated code looks pretty efficient to me, there don't seem to be any traces of proofs.

Text.Lexer.Core.concatMap {arg_0} {arg_1} {arg_2} {arg_3} =
    case ({arg_3}) of 
    | Prelude.List.::({in_4}, {in_5}) =>
            Text.Lexer.Core.SeqEmpty(
              {arg_2}({in_4}),
              Text.Lexer.Core.concatMap(____, ____, {arg_2}, {in_5})
            )
    | Prelude.List.Nil() => Text.Lexer.Core.Empty()

I realised that Idris already has removal of replace, anyway.

[ziman]

Could it be the extra singleton case that improves performance by avoiding one Seq?

[edwinb]

It's slightly surprising because I'd expect the rewrite to be inlined - as long as the proofs are erased - and therefore free! But there could be places where proofs are left around - I have been finding in my self hosting experiments that some things are not as trivial to remove as I expected.