I might have misunderstood both comments, but I have the impression the OP was asking about speed of compilation and you're mostly talking about the performance of the compiled code?
I need my answer was focused on runtime performance, thanks for pointing it out. However, They are related for two reasons:
- idris is written in idris so any improvement in the language results in faster compile-times, if more things are annotated with 0 in the compiler, thing will compile faster.
- if some variable is only important at compile-time, the compiler doesn't have to look at it with very much scrutiny. That saves you a lot of time when typechecking
> if some variable is only important at compile-time, the compiler doesn't have to look at it with very much scrutiny. That saves you a lot of time when typechecking
Right, but if some code is annotated with unrestricted multiplicity, but still not actually used anywhere in a function body, does this make compilation of that code slower than if that same code was annotated with zero multiplicity?
