The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

Robert Peszek (2) [Avatar] Offline
#1
Quoting 10.2.2:
"You now have an implementation of myReverse that runs in linear time,
because it traverses the list once to build the SnocList view and then traverses
the SnocList view once to build the reversed list."

It looks to me that in Idris example (`snocListHelp`)
we have a linear cost proof at each step causing overall quadratic cost.
Few timing experiments with my code seem to confirm that.

Is there some mechanism to exclude runtime proof cost?
I want to clarify my understanding of this,
does the book mean linear excluding proofs, or Idris can somehow replace the proofs
with something like believe-me at runtime?

I could not find answer for this, sorry if I missed it.