3 ms·

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

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

dwohnitmok 5y ago
> 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?