For the academic celebration of Prof. Johan Jeuring's 60:th birthday and the 30th anniversary of the PolyP generic programming framework, Jeremy Gibbons and I revisited the PolyP ideas in a dependently typed (Agda) setting. The result is our paper:

Agda-ventures with PolyP (PDF)

— a chapter in the Festschrift Taalblaat: Festschrift for Johan Jeuring, published in connection with JohanFest, Utrecht, 2025-09-19. The full Festschrift is available on Zenodo.

The GitHub repository contains PolyP30.lagda, a literate Agda file that serves both as the LaTeX source of the paper and as executable Agda code.

At JohanFest, I also gave a talk based on the paper and on our shared work over the decades:
→ Slides (PDF)

The final message of the talk/chapter was the following:

• Programming in this type-driven style feels like a text-based adventure game.
• You are in a hole, with some objects at your disposal, and you have to find a way out.
• You keep getting sent on side-quests.
• Sometimes it feels like you are fighting the typechecker;
• but sometimes it feels like the universe is on your side,
• and the obstacles are magically eliminated.
• In recent years, Johan’s research interests have shifted from programming languages
• to technology-enhanced learning, including ‘serious games’:
• perhaps Johan can see scope for closing the circle by bringing the two back together?

BibTeX

@inproceedings{GibbonsJansson2025_agda-ventures,
  title     = "Agda-ventures with PolyP",
  author    = "Jeremy Gibbons and Patrik Jansson",
  year      = 2025,
  pages     = {21--36},
  booktitle = "Taalblaat: Festschrift for Johan Jeuring",
  editor    = "Alex Gerdes and Hieke Keuning and Wouter Swierstra",
  url       = "https://github.com/DSLsofMath/PolyP30/raw/main/GibbonsJansson_PolyP30.pdf",
  doi       = "10.5281/zenodo.17181794"
}