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.
Why Hacker News points people here: HN points to it as a demonstration of type-directed editing with typed holes, which some see as a likely future of programming.
“Something like that is likely the future of programming!”HN comment, 2023
“Something like that is likely the future of programming!”
Example of IDE-assisted type-driven programming as the future.
Full comment
> 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.
Cites itmrgriffinJun 2019
“Here's the creator of the language deriving the implementation of zipWith without writing any code”
Language creator derives zipWith without writing code.
Full comment
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.
Cites itnequoNov 2022
Cited as example of interactive editing with typed holes.
Full comment
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
Cites itdietr1chNov 2024
“Brady has a presentation about Idris where he shows Type-Driven development”
Shows type-driven development with holes in Idris.
Full comment
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
CriticalvlaaadMay 2020
“I'm already having troubles following it after 8 lines of type definitions”
Full comment
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...
