Edwin Brady - Idris 2 - Type-driven Development of Idris

Every single one of your claims is addressed by the programming language Idris [1], which has dependent types. This is not to say that Idris is the only dependently typed language which solves these issues, only that it exists as a counterexample to your claims. 1. Idris does not have type inference at the top level, but it does infer types within the body of functions. It can even disambiguate identically-named functions with different types, something Haskell cannot do. Moreover, Idris (and other dependently typed languages) can perform implementation inference , something which is much more powerful and useful to the programmer than type inference. It lets you work interactively with the Idris compiler whereby you specify a type and Idris creates a skeleton of the function for you, filled with holes that you replace with expressions. You can ask Idris what the type of a hole is and it will helpfully tell you the types of all other identifiers in scope. You can even ask Idris to attempt to fill in the hole for you, something it can usually do when there is only one possible expression with that type (occurs extremely often in practice). Watch Edwin Brady's demo of Idris 2 [2] to see this form of interactive development in action. Note that although Idris 2 isn't finished yet, a great deal of these examples (such as zip) work in Idris 1.3.2 (the current release). 2. Idris lets you specify your program gradually. When problems arise, you can refine your types and Idris will g

> Right, but then you can't multi-thread merge() Not sure If I understand what you mean. It would be both possible to call "merge" in parallel or to implement merge to do the work in parallel as well. > Or else, you say that it's immutable, and when some thread changes the state, it produces a new map3, and the old one doesn't change. But then you have the problem of getting all the other threads updated to see the new version of map3. Yes, but this "problem" is exactly the beauty of this style of programming. It forces you to make your data-flows explicit and hence easy to discover, understand and manipulate/change by other developers. > And, by the way, I've worked on that router for TV stations. Modeling that matrix in a way that invalid states are unrepresentable is, um, extremely non-trivial... I'm not saying it is trivial. But it is possible and depending on the programming language it is actually surprisingly easy. Not only that, with a good typesystem, you not only prevent invalid state from occurring, you even get a lot of support from your IDE due to the extra information it has. Here's an example how that can look like for matrices and functions to manipulate them (like transpose): [this video] The syntax might be alien to you, but I hope it still shows what's possible at compile-time before even running the program with modern languages today.