HackerTube.dev

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

Curry On! · 19.5K views · 2019-07-18 · 40:39

Open on YouTube ↗

If playback is restricted in your region, try opening the original video. Use Mark watched to add it to your marked videos.

Overview

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.

On Hacker News

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

Recommended by 4 HN people across 4 months · HN mentions 2019–2023

Topics

Programming language designFunctional programmingLogic & formal methods
Search by tags
idris 2type-driven developmentdependent typesedwin bradyinteractive programming

What people said

lapinot · 2020-03 · Strong recommendation

I really like the general idea of bridging the gap between graphical and text-based interfaces, abstracting away the differences and be able to use a mixture of both. In the realm of interactive programming (eg heavily ide assisted), people with some functional and statically typed programming background would be interested in this magnificent talk about idris2: [Edwin Brady - Idris 2 - Type-driven Development of Idris] [VIDEO]

Read the original HN comment ↗
adamgordonbell · 2023-01 · Recommendation

The guessing the implementation part is pretty cool. You can find videos of Edwin Brady showing it off on youtube: [VIDEO] The book also walks you through lots of examples. The key part is the type needs to constrain the possible implementations down quite a bit.

Read the original HN comment ↗
pjmlp · 2022-01 · Recommendation

Not quite what you mean, but still, you might find interesting the talks on how to approach coding in languages like Idris, where the compiler is able to support the editor in type suggestions. [VIDEO]

Read the original HN comment ↗

Sources

Video by Curry On!, played through YouTube.

Data and selection notes

HN summaries and labels may contain AI errors. HN dates refer to discussions, not video publication.

HN Library: HackerTube export (2026-10-31) and open-index/hacker-news. Upstream summaries and classifications may contain AI errors.

Views, duration and playback status refresh separately from the published catalog. When an update fails, existing data remains visible.

Selection checks
  • SaaS & AI candidates: Topic keywords do not match
  • Editor-approved picks: Editorial review is required

Rule matches identify candidates. They do not guarantee video quality or financial results.

About the library and its sources