Why is Idris 2 so much faster than Idris 1?
type-driven.org.uk
Why is Idris 2 so much faster than Idris 1?
1–10 of 88 posts
Re: Why is Idris 2 so much faster than Idris 1?
#2What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?
Re: Why is Idris 2 so much faster than Idris 1?
#3What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?
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.
Re: Why is Idris 2 so much faster than Idris 1?
#4What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?
You can implement any language in any language that is Turing complete. Or practically anything with conditionals, looping and recursion.
So yes to all of your questions.
Re: Why is Idris 2 so much faster than Idris 1?
#5I bought the book "Type Driven Development in Idris" and got several chapters in before getting distracted by whatever else. It was enough that I'm now annoyed relatively often that I can't pass types as parameters to be altered during execution. I really think they're onto something brilliant. I need to pick it back up and finish the book.
Re: Why is Idris 2 so much faster than Idris 1?
#6What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?
You can implement any language in any language that is Turing complete. Or practically anything with conditionals, looping and recursion. So yes to all of your questions.
You mean you could write a compiler for Idris (or any other dependent typed language) in a Turing complete language. That’s fine but it’s not a very useful statement.
If you want dependent types IN Rust or Swift then Turing-completeness won’t help you, because neither of them have Turing-complete type checkers. You’d have to modify the compiler for them (and thus change the language itself).
Re: Why is Idris 2 so much faster than Idris 1?
#7What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?
He does it on top of scheme. Have a look at
Re: Why is Idris 2 so much faster than Idris 1?
#8Chez Scheme has an interesting compiler [1] and has also been adopted by Racket [2].
It really cool to see a little used lisp have such a great impact.
[1] https://news.ycombinator.com/item?id=15156027
[2] https://blog.racket-lang.org/2020/02/racket-on-chez-status.h...
Re: Why is Idris 2 so much faster than Idris 1?
#9Earlier quoted context omitted.
You can implement any language in any language that is Turing complete. Or practically anything with conditionals, looping and recursion. So yes to all of your questions.
You mean you could write a compiler for Idris (or any other dependent typed language) in a Turing complete language. That’s fine but it’s not a very useful statement. If you want dependent types IN Rust or Swift then Turing-completeness won’t help you, because neither of them have Turing-complete type checkers. You’d have to modify the compiler for them (and thus change the language itself).
> because neither of them have Turing-complete type checkers
Re: Why is Idris 2 so much faster than Idris 1?
#10What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?
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.
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.