Post #2346191
2026-04-27 06:54 UTC
@dpiponi@mathstodon.xyz From this perspective, what this aspect of modern algebra gives you is not the efficient or partially evaluated residual program, but a normalised representation from which you can generate the residual program, making sure you have taken into account all of the statically available information.
Replies (1)
-
@ohad@mathstodon.xyz 2026-04-27 07:03
@dpiponi@mathstodon.xyz And indeed, recognising your efficient implementation implements the universal property, the algebraic perspective gives you an interface for sound and complete partial evaluators, in tandem with the specification for what theory they are sound and complete for. If you're lucky, you can use this interface to compose partial evaluators.