Edwin Brady - Idris 2 - Type-driven Development of Idris
Why Hacker News recommends it
Recommended as the best demo of interactive, compiler-assisted dependently typed programming in action.
What it is
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 by 4 HN commenters across 4 different months, 2019 to 2023.
What Hacker News said
Strong rec lapinot · 2020-03 · on “CLUI: Building a Graphical Command Line”
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]
Recommends chongli · 2019-08 · on “Dependent Haskell Is the Future (2018)”
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
Recommends pjmlp · 2022-01 · on “It's not what programming languages do, it's what they shepherd you to (2020)”
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]
Recommends adamgordonbell · 2023-01 · on “Idris: A Language for Type-Driven Development”
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.
Cites valenterry · 2021-06 · on “Immutability is not enough (2016)”
> 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 st