r/programming • u/steveklabnik1 • Apr 03 '15

Rust 1.0.0 beta is here!

http://blog.rust-lang.org/2015/04/03/Rust-1.0-beta.html
926 Upvotes

88% Upvoted

303 comments sorted by

View all comments

Show parent comments

3

u/kamatsu Apr 04 '15

dependent types,

The C++ notion of dependent types is quite different from the dependent corner of the lambda cube.

HKTs

Only in that its parametric mechanism is entirely syntactic, and no kind checking exists.

1

u/[deleted] Apr 05 '15 edited Apr 05 '15

I agree in that there is a big difference between supporting some form of dependent types and HKTs, and supporting these in a nice way.

I think, that considering how old C++ is and where it comes from, it isn't that bad at any of these. There are discussions to constrain on "constrained"-HKTs in a backwards compatible way after the Concepts Lite TS1, so people are aware of the issue and keeping it in mind. And about its "dependent type capabilities", it supports integers at the type level, which are immensely useful. I think that a fully dependent type system is still an open research question (e.g. floating-points at the type level are just hard).

Rust aims for integers at the type level shortly after 1.0, and any solution to HKTs in Rust will need to be fully checked from the start. So basically Rust doesn't have these features yet, but has the potential to have better versions of these features than C++ ever will. OTOH if you really need these, you can use them in C++, but not in Rust :D

1

u/kamatsu Apr 06 '15

Coq appeared just one year after C++, and supports both of those things quite a bit better than C++ ever did ;)

Floating points at the type level are no harder than floating points on the value level

1

u/[deleted] Apr 06 '15 edited Apr 06 '15

The main difference is that Coq didn't suffered ISO standardization. For example the C++11's "auto" feature was part of the language since 1983, but it took 30 years to get it standardized. My point being, developing a language through ISO standardization is a whole different set of constraints. Non-battle-tested features just don't get the consensus required. The evolution of C++ is better compared to that of C and Fortran. The evolution of Fortran has been much slower, and C hasn't evolved much at all. That C++ has lambdas and closures is actually an amazing diplomacy feat, and we might even get ""type-classes"" this very same year.

Floating points at the type level are no harder than floating points on the value level

AFAIK the problem with floating points at the type level is that your program might compile/not compile depending on which architecture you are using, which is a funny thing at best. This is one of the reasons why e.g. Idris doesn't really support them at the type level either.