Why is Idris 2 so much faster than Idris 1?

Re:Why is Idris 2 so much faster than Idris 1? by krapht on Monday May 25, 2020 @04:06PM (#23304415)

I'm not sure that this question even makes sense. It's like asking: "What language features are needed in order to implement a borrow checker?"

You don't bolt this functionality on to an existing language; it requires changes to your whole compiler pipeline to be useful.

[ Parent | on HN ]

Re:Why is Idris 2 so much faster than Idris 1? by drcode on Monday May 25, 2020 @04:25PM (#23304577)

Don't be so certain, some languages allow a lot of flexibility within libraries. For instance, Clojure has an excellent library implementing Go-style channels with green threads (core.async) all built without any modifications to the core system.

[ Parent | on HN ]

Re:Why is Idris 2 so much faster than Idris 1? by krapht on Monday May 25, 2020 @04:46PM (#23304790)

Sure. Linear types and borrow checking is possible in Lisp too, but I wouldn't take that as evidence that it's super easy to make Clojure behave like Rust.

What is possible and what is practical are two different things.

[ Parent | on HN ]

Re:Why is Idris 2 so much faster than Idris 1? by zelphirkalt on Tuesday May 26, 2020 @03:49AM (#23308468)

Good point, Lispy languages with sufficiently powerful macro systems can do this. This is part of the reason, why no language committee deciding on backwards compatible changes to the language is needed to develop such a library.

I don't know enough to say whether this would be possible in Rust.

[ Parent | on HN ]