u/cypherx(λx.x x) (λx.x x)in r/compsci • Recommends
Conor McBride: Agda-curious? (ICFP 2012 keynote)
0:00 / 0:00
ICFP 2012 Monday keynote. Conor McBride: Agda-curious?
Malcolm Wallace
884 subscribers • 15 videos on Hallway
- Recommended by 2 people: 2 in engineering communities.
- Presented by Conor McBride
Advanced. Deep dive for people who know the field.
5.3K views14 years ago2 recommendations
Programming languagesComputer scienceFunctional programmingLanguage design and type systemsComputation and complexity
Conor McBride delivers a keynote on Agda, demonstrating interactive programming with holes and dependent types.
ICFP 2012 Monday keynote. Conor McBride: Agda-curious?Why it's here
2 people recommend thisWhat people say. Recommended as an excellent introduction to Agda and interactive programming with holes.
Moments people linked to
u/aseippin r/haskell • Recommends
On “GHC HEAD now features Agda-like Holes”
Yes. Conor McBride recently did an Agda intro at ICFP. The video is here (4m30s): link to this video
Watch from that point. The quality isn't great, but in the example, the little green highlighted bit is a hole. In Agda, holes are represented by `{!!}`, and when you run the typechecker on a program with holes, it runs, and when it's done unifying all non-holes, you get dropped into the 'goal view' where you can interactively work with the holes, one by one. You essentially interactively can fill out those holes. So this is something that really happens *during* type-checking (the line of compile/runtime is blurred a bit in this domain, anyway.)
As you can see, Conor can create a hole, then use Agda…