In the paper "Agda-ventures with PolyP" Jeremy Gibbons (@jer_gib) and I revisit PolyP in a literate Agda setting — combining executable code, theory, and reflection on three decades of generic programming. It is part of a Festschrift gifted to Johan Jeuring at the academic celebration of his 60th birthday.
📖 Blog post: https://patrikja.owlstown.net/posts/4693
📄 Paper: https://github.com/DSLsofMath/PolyP30/raw/main/GibbonsJansson_PolyP30.pdf
💬 Festschrift DOI: 10.5281/zenodo.17181794
#Agda #FunctionalProgramming #GenericProgramming #Haskell #TypeTheory
Final words from the paper/talk:
* 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?
