Type-Driven Development in Idris — Edwin Brady
Why Hacker News recommends it
HN points to it as a demonstration of type-directed editing with typed holes, which some see as a likely future of programming.
What it is
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.
Recommended by 1 HN commenters across 1 different months, 2019 to 2024.
What Hacker News said
Recommends still_grokking · 2023-01 · on “C++ at the End of 2022”
> 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 mrgriffin · 2019-06 · on “Type inference has usability problems”
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 nequo · 2022-11 · on “Type-Signature.com”
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 dietr1ch · 2024-11 · on “Hazel: A live functional programming environment featuring 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]
Critical vlaaad · 2020-05 · on “In Further Praise of Dependent Types”
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 bei