idris-lang / Idris2

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

Use query-based compiler architecture #2512

Open michaelmesser opened 2 years ago

michaelmesser commented 2 years ago

Summary

A query-based compiler architecture would allow for efficient incremental type checking. Rust-analyzer and Sixty use this approach.

Query-based compilers are structured as follows:

Motivation

A query-based compiler architecture would provide the following benefits:

The proposal

I believe an implementation would be similar to how rust-analyzer and sixty are implemented.

Alternatives considered

Conclusion

A query-based architecture would significantly improve the editor experience on large projects. Unfortunately, rearchitecting the compiler would be a huge and difficult change to implement.

ohad commented 2 years ago

I think the IDE protocol can be used to this effect. The protocol requests can be recorded with dependencies and their responses cached, and a simple compiler state flag can indicate whether the state has changed. If the flag isn't set, we can satisfy a new response from its cavhed answer.

In the future, we can improve the dependency analysis for finer grained change tracking. So working on the IDE protocol can be a shortcut to query based compiler.

This kind of architecture can even be a layer between the client and server, in an external project.

michaelmesser commented 2 years ago

@ohad I think you are describing something significantly different that what I am describing. Can you point to a project that does what you describe so I can better understand?

ohad commented 2 years ago

It's possible that the implementation is significantly different, but since this proposes a major overhaul of the compiler, I think the IDE protocol is a viable alternative that should be considered if it delivers comparable functionality.