wrt. defunctionalization, another resource that requires only basic understanding of functional programming (lambdas and ADTs) and equational reasoning to under

wrt. defunctionalization, another resource that requires only basic understanding of functional programming (lambdas and ADTs) and equational reasoning to understand it is lecture 4 of [0]. The procedure is quite straightforward if approached from a program derivation standpoint; first convert the program into CPS (see end of lecture 1). That is, solve the equation `progCont e k = k (prog e)` given prog. Then convert the closures into first-order structures by identifying the free variables they capture and deriving the closure-free version. I really like Bartosz's blog post on defunctionalization and Freyd's theorem[1]. It's probably better to understand Freyd's theorem in the usual categorical presentation as Bartosz dualizes many things (because instead of a huge product of all environments we have a huge coproduct of possible environments, then select the "best"/"minimal" one using some universal cone as opposed to a maximal product). Truly, defunctionalization is one of those things that can satisfy curiosity on many levels of abstraction from assembly to categories. [0] http://www.cs.nott.ac.uk/~pszjlh/pcalc.html http://www.cs.nott.ac.uk/~pszjlh/pcalc.html [1] https://bartoszmilewski.com/2020/08/03/defunctionalization-and-freyds-theorem/ https://bartoszmilewski.com/2020/08/03/defunctionalization-a...