Post #3277068

@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.