1 HN user recommended this talk1 month2019–2024score 1
Years with an HN recommendation, 2007–2026
HN points to it as a demonstration of type-directed editing with typed holes, which some see as a likely future of programming.
Edwin Brady, creator of Idris, introduces type-driven development in a dependently typed language. He shows types being written first and programs derived with interactive editing, then extends beyond simple examples to programs that interact with users and networks.
“Something like that is likely the future of programming!” (HN, 2023)
> Basically, your IDE writes more of the code for you. I think this was, in general, a dead end in language research for various reasons, […] I think language researchers would strongly disagree. Something like that is likely the future of programming! For example: [this video] From the video description: > In Idris, types are a first class language construct, meaning that they can be manipulated and computed like any other language construct. It encourages a type-driven style of development, in which programmers give types first and use interactive editing tools to derive programs.
Example of IDE-assisted type-driven programming as the future.
Not OP, but my understanding is that it's a common approach in Idris. Here's the creator of the language deriving the implementation of zipWith without writing any code: [this video] Some other examples include: - Haskell: [link] - Scala: [link] - Agda: [link] I was under the impression that justDoIt comes from Scala, but I can't find a reference for that.
Language creator derives zipWith without writing code.
Thinking in types and type relations sounds to me like Rule 5 taken to its logical conclusion. Types are your data structures, and they guide how you write your functions. Agda[1] and Idris[2] turn this idea into interactive editing with typed holes. You put a "?" in the code and the compiler fills the hole in for you based on the type that it infers for it. Haskell has a less expressive type system but it also has typed holes and Wingman[3] extends the Haskell Language Server to use them for interactive editing. [1] [link] [2] [this video] [3] [link]
Cited as example of interactive editing with typed holes.
Brady has a presentation about Idris where he shows Type-Driven development (where you write code that could typecheck with some holes and you get the compiler to help you figure out the missing types for your "whatever/something" untyped variables) [this video]
Shows type-driven development with holes in Idris.
Damn, this area of programming sounds very interesting, but I'm so so lost in these type compositions... Is it this Idris video you are talking about? [this video] I'm already having troubles following it after 8 lines of type definitions, while matrix transposition in the language of my choice is just `#(apply mapv vector %)` Sorry, I'm not trying to be dismissive, I just want the ergonomics of expressing my intentions to the computer be free of all this boilerplate while leaving compiler a possibility to give me some useful feedback when something might be wrong, are we really not there yet or are there languages aiming to make dependent types practical? You mentioned Coq, but I'm still not being able to find any code examples or some getting started guide in its official documentation...
Video list and Hacker News comment labels from HackerTube (prompted by @karpathy), released under ODC-By 1.0, built on the open-index/hacker-news archive. Hacker News data is provided by Y Combinator; comments remain the work of their authors. Video titles, channel names and thumbnails belong to their creators and are shown via YouTube. HackerTube Watch is an unofficial edition. Data export of 2026-10-31.
Plays via YouTube's privacy-enhanced embed
5 Hacker News comments
From the HN archive; up to 20 kept per video, favoring different commenters. Recommendations first.
Citations, criticism and jokes
Read more