Type-Driven Development in Idris — Edwin Brady

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

> 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.

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

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...

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.