Curry On!
4 HN recommenders · recommended in 5 months, 2019–2023
40:39 · 20K views · Jul 18, 2019
Edwin Brady, creator of Idris, presents Idris 2 and demonstrates type-driven development, where the compiler assists by filling holes and suggesting implementations from types.
Recommended as the best demo of interactive, compiler-assisted dependently typed programming in action.
5 comments from Hacker News
I really like the general idea of bridging the gap between graphical and text-based interfaces, abstracting away the differences and be able to use a mixture of both. In the realm of interactive programming (eg heavily ide assisted), people with some functional and statically typed programming background would be interested in this magnificent talk about idris2: [Edwin Brady - Idris 2 - Type-driven Development of Idris] this video
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
The guessing the implementation part is pretty cool. You can find videos of Edwin Brady showing it off on youtube: this video The book also walks you through lots of examples. The key part is the type needs to constrain the possible implementations down quite a bit.
Not quite what you mean, but still, you might find interesting the talks on how to approach coding in languages like Idris, where the compiler is able to support the editor in type suggestions. this video
> 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.