hackertube.io

Edwin Brady - Idris 2 - Type-driven Development of Idris

Curry On! · talk · Watch on YouTube

Programming language designFunctional programmingLogic & formal methods

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.

Why Hacker News recommends it

Recommended as the best demo of interactive, compiler-assisted dependently typed programming in action.

  • 4 people recommended it
  • 4 different months
  • 1 strong recommendations
  • first 2019, last 2023

What HN commenters said

  1. “would be interested in this magnificent talk about idris2”

    Talk on interactive, compiler-assisted development with Idris 2.

    lapinot, 2020-03 · Strong recommendation · in “CLUI: Building a Graphical Command Line”

  2. “Watch Edwin Brady's demo of Idris 2 [2] to see this form of interactive development in action.”

    Demo of interactive type-driven development with Idris hole filling.

    chongli, 2019-08 · Recommendation · in “Dependent Haskell Is the Future (2018)”

  3. “you might find interesting the talks on how to approach coding in languages like Idris”

    Shows compiler-assisted editing with type suggestions in Idris.

    pjmlp, 2022-01 · Recommendation · in “It's not what programming languages do, it's what they shepherd you to (2020)”

  4. “You can find videos of Edwin Brady showing it off on youtube”

    Edwin Brady demonstrates Idris guessing implementations from types.

    adamgordonbell, 2023-01 · Recommendation · in “Idris: A Language for Type-Driven Development”

Excerpts from Hacker News comments, linked to the originals. Summaries and labels were written by a language model from those comments.

Topics: idris 2, type-driven development, dependent types, edwin brady, interactive programming

Also recommended by the same people