search

idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.51k stars 374 forks source link

Performance improvement with compiling Nats and Fins? #1306

Open andrevidela opened 3 years ago

andrevidela commented 3 years ago

Recently I've started playing with proofs using large nats and Fins. While the programs outputed are fast thanks to the optimisation of Nat to int, the compiling time is very long even for very simple programs.

This is not a proposal but a question: What are the ways we can improve the time of compilation when evaluating terms that we know optimise into a more efficient runtime representation?

I know that some flavours of lisp allow to update the definition of a function at runtime. Would it be possible to do the same for Nat and + when type-checking on scheme?

There are reports of similar issues but no plan in order to reach a resolution, see #16 and #1182

ohad commented 3 years ago

We could use an optimised representation for Nats and Fins internally, cashing in on the fact that their constructors have at most 1 argument, and so an open natural number is of the form S^n t with t a non-canonical open natural number, and similarly for Fin.

It would require a bespoke treatment of Nats and Fins. I'm guessing it would make the type-checker hairier.

I think there's a general thing we could do, allowing the users to view data structures as more efficient runtime and compile time implementations, but we'll need to make several research breakthroughs in generic metaprogramming first.