IMO, it would be easy to create a new dependently typed language with on a subset of the Rust or Swift syntax.
Here's a tutorial written by an Idris contributor.
http://davidchristiansen.dk/tutorials/nbe/
Following the guide, you can build a dependently typed language with Racket syntax in two hours.
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.
Comments
IMO, it would be easy to create a new dependently typed language with on a subset of the Rust or Swift syntax. Here's a tutorial written by an Idris contributor. http://davidchristiansen.dk/tutorials/nbe/ Following the guide, you can build a dependently typed language with Racket syntax in two hours.
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.