|
One important thing Rust and Haskell have in similar is the nearly complete absence of an endeavour to unify things. As more fancy type system features get added, both languages become quite complex, thus increasing the learning curve and compiler complexity. This is quite aptly expressed by the recent paper on dependent types [1]: > Previous versions of Haskell, based on System Fω , had a simple kind system with a few kinds (, → * and so on). Unfortunately, this was insufficient for kind polymorphism. Thus, recent versions of Haskell were extended to support kind polymorphism, which required extending the core language as well. Indeed, System FC↑ [30] was proposed to support, among other things, kind polymorphism. However, System FC↑ separates expressions into terms, types and kinds, which complicates both the implementation and future extensions. Later in the paper, they show how some of the most recent "fancy" features of Haskell can be achieved in a more economic framework based on first-class types. Unfortunately, systems programming (as in C/C++) puts strict constraints on a programming language, and currently it's not quite clear what's the best way to integrate dependent types with systems programming. In the coming years, I expect to see some forms of castrated dependent types tuned for systems programming (e.g., types dependent only on indices). [1] https://www.researchgate.net/publication/308960209_Unified_S... |
Dependent types dispense with the phase separation between compile-time and run-time code, which is inherent to system languages. So you can easily have dependent types in a systems language as part of compile-time evaluation, but not really as a general feature. It would work quite similar to the "program extraction" feature in current dependent-language implementations, which does enable improved type checking because you can express arbitrary proofs and check them reliably as part of compilation.