[dwohnitmok]

Oh fascinating. Are you saying that multiplicity annotations can affect compile time speed (in particular giving a laxer multiplicity than what is required)?

[lang_agnostic]

Yes. Multiplicity 0 removes the value from the runtime avoiding allocations and garbage collection. That particularly handy for type-level indices and type-level programs in general.

Technically speaking multiplicity 1 (linear variable) can be subject to arbitrary inclining though it's not implemented in the compiler.

I'm working on other multiplicities that could allow you to describe which values are "compile-time" available, and therefore subject to optimisations

[dwohnitmok]

> Multiplicity 0 removes the value from the runtime avoiding allocations and garbage collection.

Does this apply even for compile-time evaluation? I'm not sure of the specifics of how Idris does compile-time evaluation vs runtime evaluation.