Post #2346192

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