11–20 of 88 posts
Chez 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...
Please, please Mr.Keep! Let's get Chez unboxed floats!
What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?
A second feature that I think is needed is a way to go between types and values which I don’t think rust or swift can do.
Two fundamental dependent types are the dependent sum and dependent product. The dependent product is the type of a function whose output type depends on its input value. This is a generalisation of the product type: the product type (a,b) is like the dependent product type (x:{1,2}) -> T x where T 1 = a and T 2 = b.
The dependent sum type consists of a tag value of some type and a value whose type depends on the tag. For example a vector of arbitrary length Of floats could be written with a type something like:
Sum(n:Nat)(Vec n Float)
(2,[1,2])
What 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 definitely add dependent types to Rust, but I see at least the following problems.
1. Rust compile times and dependent typing compile times are both really long. Combining the two sounds like it'd be unacceptably long.
2. Rust promises full type erasure when you're not using "dyn". Predictably erasing dependent types seems to be a hard problem. Heck, even ergonomically giving low-level control over the layout of a dependent sum sounds hard.
3. Dependent types give you a whole bunch of new ways to do things that you can already do in Rust, which is probably a bad thing.
I think "bolt-on" approaches, as Hoare logic is to imperative pseudocode, or SPARK is to Ada, are something that Rust could easily employ, which are more well-tested, and would solve all of the use cases of dependent types in industry.
What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?
But it is not easy to plug dependent types to existing compilers of Rust or Swift. In general, a dependently typed language is not Turing-complete so that the type checking (which now requires running programs) is decidable. That means you have to rule out features like general recursion and arbitrary loops. That could mean reconnecting the wires in the existing compiler. From an engineering aspect, it should be easier to plug dependent types on a functional programming language, e.g., dependent Haskell, than imperative languages.
Earlier quoted context omitted.
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 https://sdleffler.github.io/RustTypeSystemTuringComplete/
Earlier quoted context omitted.
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.
What is possible and what is practical are two different things.
Earlier quoted context omitted.
> because neither of them have Turing-complete type checkers https://sdleffler.github.io/RustTypeSystemTuringComplete/
That's almost certainly a bug. At any rate, a proper language with dependent types does not have a Turing-complete type checker and that's what makes it magical. You get incredible power without having to worry about non-termination in your type checker.
Apparently Haskell has some restrictions that make typeclasses decidable (if -XUndecidableInstances is not set), but Rust has no such mechanism other than numeric iteration limits.
Chez 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...
Chez, together with the commercial lisps, is among the best dynamic language systems there are. Apart from the unboxed floats me ruined by another sibling posts, it produces really good code.
In my tests it has been ever so slightly faster than sbcl when the code does not depend excessively on spending time in the standard library. SBCL's standard library has had a lot more optimization work done on the individual function level (I'm looking at you, isqrt). Most of the difference in my case can be erased by the new SBCL block optimization though, which chez does on the module level.
What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?
Dependent types are a language feature, simply adding two types --- the dependent product / exponential / function type, and the dependent sum / product / tuple type. You can definitely add dependent types to Rust, but I see at least the following problems. 1. Rust compile times and dependent typing compile times are both really long. Combining the two sounds like it'd be unacceptably long. 2. Rust promises full type…
I don't know if "type erasure" is the accurate term to use with the generic-specialization scheme that Rust uses; one can trivially write a generic Rust function that demonstrates that types, while inaccessible at runtime, still semantically affect the generated code:
use std::mem::size_of;
fn foo(t: T) {
dbg!(size_of::());
}
fn main() {
foo(1); // prints 4
foo("bar"); // prints 16
}Earlier quoted context omitted.
Dependent types are a language feature, simply adding two types --- the dependent product / exponential / function type, and the dependent sum / product / tuple type. You can definitely add dependent types to Rust, but I see at least the following problems. 1. Rust compile times and dependent typing compile times are both really long. Combining the two sounds like it'd be unacceptably long. 2. Rust promises full type…
> Rust promises full type erasure when you're not using "dyn" I don't know if "type erasure" is the accurate term to use with the generic-specialization scheme that Rust uses; one can trivially write a generic Rust function that demonstrates that types, while inaccessible at runtime, still semantically affect the generated code: use std::mem::size_of; fn foo (t: T) { dbg!(size_of:: ()); } fn main() { foo(1); // print…
Equivalent C++ code (admittedly, C++ templates aren't really generics) would have enough information to shove literal 4 and 16 into the binary there.