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])
I think instead, for one of these languages, the ideal would be opt in should you need it. Dependent types are, by their nature, proof carrying[2], and there are times when you want this, but for a general-purpose programming language, also times that you do not. You can't be total over IO (or any effect for that matter), so, yeah, skip it when arg-parsing, but then opt-in when you're processing your financial transactions or actuating your robot.
LF does not have higher kinded types but it does have dependent types.
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.
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: T) {
dbg!(size_of::<T>());
}
fn main() {
foo(1); // prints 4
foo("bar"); // prints 16
}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.
You don't bolt this functionality on to an existing language; it requires changes to your whole compiler pipeline to be useful.
Useful steps on the road: singleton types (needed to make it easy to represent basic values as types), higher-kinded types (needed to implement functions at the type level), kind polymorphism (needed to be able to reuse the same functions at the type and the value level). Rust is I think getting the first, is gradually implementing little subsets of the second, and is nowhere near the third.
The other thing you need to worry about is how dependent types interact with existing language features. In particular, if not implemented carefully then they may break type inference, and I imagine Rust's lifetime inference might have similar issues.
Dependent Types via macros, in Racket
somewhere near the end of the paper is a table of the macro features used, which gives the impression it was only possible in Racket, but the lack of a common terminology for these things makes it hard to compare other languages' macro systems unless you are deeply familiar with them, so maybe it could be adapted
So yes to all of your questions.
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).
I highly recommend the book. Typing in examples and getting experience collaborating with the compiler on edits is worthwhile. Even if you never use Idris(2) again after reading it, the demos on creating state machine DSLs with contextual invariants will leave a lasting impression.
[1] https://idris2.readthedocs.io/en/latest/typedd/typedd.html
[2] https://github.com/idris-lang/Idris2/tree/master/tests/typed...
Wouldn't that be at odds with static typing?
Types are values, and types can depend on values - so if your protocol tells you you should be getting a string, a string shows up in the type signature.
It is fair to say that functional programming is primrarily in favor of immutable data structures because it is simpler to implement them efficiently in a setting where referential transparency is the default. Mutation (meaning referential intrasparency) is just more complicated, and we need heavier machinery to structure it nicely. We may use linear/substructural types, uniqueness types, regions, etc for this purpose, but here are a number of choices, and the picture is not as clear-cut as with plain pure lambda calculi. Just remember that mutation is not bad by itself, many functional programmers are often happy to speed up production code with mutation, it's just that it is usually more complicated to structure nicely.
Both State- and ST-using code is harder to understand than code that doesn't use them. Immutable semantics are easier to reason about. Of course the implementation of those semantics may involve mutation at some lower level. But ideally we would have a runtime system that could implement immutable semantics with no loss of efficiency compared to implementing those lower-level mutations explicitly in our code.
Even if computers had immutable memory, then you still need to initialize memory regions with constant values and that would be a mutation.
It is possible to protect memory regions from writing, but these regions are still writable by the operating system kernel. And this is purely for safety and not for performance.
(And don't get me started on CPU caches and registers)
> Idris 1 is implemented in Haskell, but that has little (if anything) to do with the difference.
But latter they also go on to say:
> Idris 2 benefits from a robust, well-engineered and optimised run time system, by compiling to Chez Scheme.
I must say I'm slightly confused here. Yes a rewrite might also enable to avoid all the legacy part that might slow down the code, but what is also possible, is that a new language and a new runtime could enable new optimizations that are not possible before. The author did mention Chez's profiling tools help a lot in the rewrite. So I was curious: is it really true, that we cannot attribute some part of the speedup to language differences?
Also I was interested in the rationale behind using Scheme to replace Haskell, but I failed to find some reasoning behind this, anyone can shed some light on this?
The author even says that it's difficult to write C that deals well with the functional style of lots of little functions, and this is a problem Scheme also has and has solved. That's enough rationale to switch to Scheme:
> Generating good C code corresponding to a functional program which might have lots of small (and higher order) definitions is extremely challenging, so it is better to take advantage of someone else's work here.
So Scheme is replacing C, and Idris is replacing Haskell. The goal was self-hosting by writing the compiler in Idris. Chez Scheme is a nice compilation target because it's performant and Scheme is a sugared lambda calculus that goes well together with FP languages.
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.
Please, please Mr.Keep! Let's get Chez unboxed floats!
Or, said differently, what's missing in the language or ecosystem to make it more immediately practical? Could Idris be the successor to Haskell with appropriate support?
If the meager library of third-party and community packages is an important factor or not depends a lot on the domain.
I really wish some powerful corp would pick up Idris and put contributions and/or funding to it.
I would love to be able to write production code in Idris rather than patching together a million Haskell extensions.
Critical info missing.
If you imagine a "cube" of fundamental language features, on one corner is "the simply typed lambda calculus" which you can think of as old-school C. Along each of three edges we add a fundamental language feature: parametric polymorphism (values that depend on their type; think 'C# generics'), type constructors (types that depend on types; something akin to C++ template types like `vector` but not like `std::sort`), and dependent types (types that depend on values; but definitely not restricted like `std::array`; something more like MacroC or `enable_if`).
There's not a lot of good analogies for this stuff in commonly used programming languages because the big languages are really basic (not simple!) compared to the advanced stuff the programming language theorists have gotten up to.
I agree partly; I didn't downvote but I think in this case the downvotes are not that weird; it's quite well known what Idris is in HN circles, but that's not the point; the article has links that tell you (pointing to idris-lang) and google idris edwin brady (which is on top of the article) will get you more than you want to know most likely but at least enough to know what it is. So it is the absolute bare minimum to open an article and pop in; 'what is this?' if it's not in the first line of an article which I think is not great. A little bit more I do expect from this place; like clicking on the article, immediately recognising it as a language (that's clear within seconds of scrolling the article I would say) and then maybe come back with 'what is dependently typed?' or something. But going from opening the article to hitting wikipedia explaining dependently typed languages is ... well, not much more work than doing nothing and just popping 'huh?' in here imho.
Edit: actually, just google 'idris2' and you have in the first line exactly what, who, why etc.
With most computer artifacts, it is hard to tell, prima facie, that they are slow, until somebody makes a faster one. Then the original comes to be recognized as slow (although somebody will still insist it's not that slow). The faster one might still be slow, but that fact remains unknown.
The fact is that almost everything is slow, in the sense that somebody smarter, more experienced, and more diligent could make it faster, often by doing things that the person who wrote the slow version would have found distasteful.