[lang_agnostic]

Hi there,

I'm a phd student working on Idris and I used to work with Edwin on this, if you want more info or want to see more practical applications of idris2, Dependent types, or QTT, here are a couple links:

- idris2 is written in idris2 so that's a good example of a big program using dependent types https://github.com/idris-lang/Idris2

- we have some very interesting libraries in the works: https://github.com/idris-lang/Idris2/wiki/Libraries

- my own projects in idris include a purely declarative server library where you give the API and the server is completely implemented and instantiated from your description https://gitlab.com/avidela/recombine

[dwohnitmok]

I'm curious if you have any insight into what a realistic lower limit to Idris compile time speed looks like. Right now even moderately sized Idris programs can be quite slow to compile, slower than even other dependently-typed languages (see e.g. https://github.com/AndrasKovacs/smalltt). How much of this is intrinsic to Idris' language design and how much of it is due to lack of optimization in the implementation?

[lang_agnostic]

I reckon we can get the raw performance quite low, but it might be a challenging environment to program in, the ergonomics of programming linear types aren't figured out and it would involve a lot of memory management. While safe, reasoning about memory can be quite hard, just like anyone learning how to handle the borrow checked in rust can tell you.

It's currently one of my project to use QTT to statically enforce performance invariants and optimisations, currently I am looking at partial evaluation of programs and explicit annotations to control which parts need to be partially evaluated and which parts need to remain Unevaluated.

Regarding the benchmarks there are two things to address to make them go faster:

- the idris parser is actually pretty slow so we should get working on that

- the examples use explicit runtime bindings for type parameters which force the types to be allocated and available at runtime, which destroys the performance of some programs (stlc notably)

It's not expected to write idris code in that way since linearity annotations also allow you to _remove_ values from the runtime and make dependent programs go faster, if you were to be concerned about runtime performance you would use _runtime erased_ type variables instead of _runtime relevant_ variables. Some of this is due to the foreign nature of QTT, and we should do a better job at teaching how to use it for performance.

On the other hand someone could argue "if idris is that smart can't it warn/perform those optimisations automatically?" And maybe that's the way to go, but we need more eyes and brain looking at the problem and coming up with prototype solutions to make progress. idris is still a small project so we don't have enough people working on it to implement those smart features

[anentropic]

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?

[lang_agnostic]

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]

> 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?

[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.