Post #3277067
2025-08-24 20:36 UTC
@moonchild@social.applied-langua.ge @corbin@defcon.social I'm still booting up from sleep but I think it's https://en.wikipedia.org/wiki/Defunctionalization. See also section 2.3 (page 13) of https://www.brics.dk/RS/01/23/BRICS-RS-01-23.pdf. Danvy in that example restricts himself to pairs where the component types are the same, but that's because he's using ML and doesn't have dependent types.
Replies (1)
-
@pervognsen@mastodon.social 2025-08-25 00:45
@moonchild@social.applied-langua.ge @corbin@defcon.social Looks like there's this on defunctionalization in dependent type theory: https://arxiv.org/pdf/2304.04574. They also mention in the introduction that GADTs are sufficient for defunctionalizing non-dependent but polymorphic function types, referencing this paper: https://dl.acm.org/doi/10.1145/964001.964009.