Mastodawn

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?

C++Now Mar 24, 2025

C++Now 2025 SESSION ANNOUNCEMENT: Missing (and Future?) C++ Range Concepts by Jonathan Müller

https://schedule.cppnow.org/session/2025/missing-and-future-c-range-concepts/

#algorithms #cpp #genericprogramming

Missing (and Future?) C++ Range Concepts – C++Now Schedule

Hacker News Mar 19, 2025

Implementing Generic Types in C

https://btmc.substack.com/p/implementing-generic-types-in-c

#HackerNews #ImplementingGenericTypes #CProgramming #SoftwareDevelopment #GenericProgramming #TechInsights

Implementing Generic Types in C

There are various ways, but some are better than others.

Burning the Midnight Coffee

Cass Alexandru Dec 11, 2024

I feel like one of the main reason why we haven't worked hard enough to make #genericProgramming ergonomic in practice is bc we usually omit the equations, only feebly clutching free theorems. If we were to stop treating equations as an afterthought we'd quite forcibly need to define objects and maps compositionally, or be doomed to write boilerplate (or write metaprograms (tactics) that write boilerplate) ad nauseam.

Cass Alexandru Dec 11, 2024

programming with explicit recursion is like making a phone waterproof by gluing all its components together. There are so many reasons to separate the business logic of a function from its recursion behavior s.a. scans, (un)folding only to certain depth, combining traversals (via the banana split theorem)… The fact that we're used to this glued-together world makes us overlook all the possible uses of the components. #recursionschemes #genericprogramming