Books. Some books on my shelf covering these topics:
"Type Theory and Functional Programming" by Simon Thompson (PDF available via quick search)
First 120 pages of "Type Theory and Formal Proof" by Rob Nederpelt / Herman Geuvers
For some early stuff on dependent types (also covered in the above), check out "Intuitionistic Type Theory" by Per Martin-Lof
"Computation and Reasoning: A Type Theory for Computer Science" by Zhaouhui Luo
"Type-Driven Development with Idris" by Edwin Brady
"Gentle Introduction to Dependent Types with Idris" by Boro Sitnikovski
"Types and Programming Languages" by Pierce
"Practical Foundations for Programming Languages" by Robert Harper (or any of his YouTube videos re/Type Theory)
"The Little Typer" by Friedman and Christiansen
"Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy" by David Corfield (just took this one to OBX North Carolina to enjoy on my beach vacation last week! Got some salt water in those pages. Also speaks to Category Theory.)
For Category Theory:
"The Joy of Abstraction" (2023) by Euginia Cheng
"Basic Category Theory for Computer Scientists" by Benjamin C. Pierce
"Conceptual Mathematics: A first introduction to categories" by Lawvere and Schanuel
"Categories for the Working Philosopher" by Landry
Okay, but then you'd show that 1/-1=-1, 1/-0.5=-2, 1/-0.25=-4, etc. The closer you get to 0, the more negative the number. Then you just wouldn't accept that if you actually got to 0 in your progression, it is anything besides negative infinity. And then you've shown that negative infinity is equal to infinity.
I do this too in some apps. Very near exactly how you show it.
How do you enforce required fields in the data model? By eliminating the possibility of null values, you eliminate the possibility of not-null constraints in the data model. I end up having to enforce these types of (non-complex) constraints outside the relational model. A missing row is not detectable in the same way as a null column value.
It's been on my list of things to explore for a while... the relationship between defunctionalization, continuations, and "Algebraic Effects".
The reason... I like seeing how different languages handle asynchronous code vs synchronous code. F# has their way, C# has theirs, JavaScript async/await, colored functions, Project Loom, co-routines, React Fibers, etc. I'm intrigued that a language that has built-in algebraic effects can do async wihtout any other changes to the language (as if async and sync were the same).
Is there any relation to defunctionalization for this kind of stuff?
The Reynolds paper is one of my favorites. It was re-typeset in 1998 making it a lot easier to follow the math [0]. It's fun to compare it to a copy of the original from 1972 [1].
Philip Wadler had this to say about the paper: "Certain papers change your life. McCarthy's 'Recursive Functions of Symbolic Expressions and their Computation by Machine (Part I)' (1960) changed mine, and so did Landin's 'The Next 700 Programming Languages' (1966). And I remember the moment, halfway through my graduate career, when Guy Steele handed me Reynolds's 'Definitional Interpreters for Higher-Order Programming Languages' (1972)."[2] This is how I discovered it I believe.
The paper is exceedingly approachable. It was so well written that I immediately purchased a used copy of Reynolds' book on programming languages (which I did not have as easy time with compared to the paper - and still remains unfinished on my bookshelf).
When they republished the paper in 1998, Reynolds wrote about how the paper came to be [3], and I believe about the discoveries of continuations [4].
I recently implemented Reynold's meta-circular interpreter in TypeScript and serialized the abstract syntax into JSON. Coincidentally, a few days later I saw a post on HN something about "executable JSON" or some such "programming language" that the creator was very proud of making it into a product of sorts. (found it... JSON Logic: https://news.ycombinator.com/item?id=27306263). Queue Greenspun's tenth rule. I chuckled as I looked at the JSON Logic syntax knowing that a little Reynold's interpreter with its AST serialized to JSON is infinitely more powerful and extensible (allowing higher-order functions and such). I highly recommend anyone reading this to write the 50 or so lines of TypeScript necessary to implement Reynold's meta-circular interpreter (EXTREMELY EASY and nearly identical line-for-line to the 1998 paper, only in TypeScript instead of lambda calculus).
The continuous aggregates portion of this blog (along with the breakdown of Transition, Combine, and Final Functions) reminded me of "A Theory of Changes for Higher-Order Languages: Incrementalizing Lambda-Calculi by Static Differentiation" (Giarrusso et. al.) [0].
Particularly the part of getting logically-consistent results via different routes of computation. David Kohn says this in the blog post: "But, you have to have in-depth (and sometimes rather arcane) knowledge about each aggregate’s internals to know which ones meet the above criteria – and therefore, which ones you can re-aggregate."
I think Giarrusso addresses the internal requirements in a precise mathematical manner (though I may be wrong). Giarrusso Section 2.1 is the specific area I'm thinking, particularly Definition 2.1 and then later the discussion of the abelian group where certain binary operations must be commutative and associative. Giarrusso Equation 1 in the introducton defines externally what it means to be logically consistent.
Also, Giarrusso talks about "Self-Maintainability" where updating the continuous result only needs to look at the changes to the input. What was obvious to me from reading Giarrusso was that something simple like "AVG" is not self-maintainable unless you keep the intermediate state (sum and count) seperately. Kohn's distinction of Transition Function, Combine Function, and Final Function - together with Giarrusso's abelian group and change structure - is kind of a big deal in making arbitrary functions "continuous"-capable while being "self-maintainable".
I can see designing a [data] structure that adheres to the specific algabraic laws defined by Giarrusso's abelian group along with the 3 functions from Kohn (missing from Giarrusso). You can then feed this structure to a function that spits out two new functions for you: a normal function that can be used to calculate a result, and it's "continuous" version which only needs change to the inputs. For example, "avg()" and "avg_continuous()" can be automatically derived from a data structure of algebraically well-behaved operations.
Plus this would have a really cool Category Theory diagram for it!
David: absolutely love the animated gifs and pictures. Very well written indeed.
> I was always in awe of the lake size battery they created.
This is exactly the feeling I had when visiting the Seneca Pumped Storage Generating Station that I mentioned in one of my other comments that I just posted before seeing your post. Truly awe inspiring. (Links provided in my other comment). Do go visit one of these!
Years ago I visited the Seneca Pumped Storage Generating Station [0] reservoir in person. It's a massive man-made lake on the top of a small mountain in Pennsylvania, USA.
They pump water up to it at night (when there is excess energy in the power grid), and let the water out in the day when the demand for energy is high (turning some turbines on its way down).
Prior to visiting I had an intellectual understanding of the concept of pumped storage [1], but I have to admit that it's one heck of an experience when you see it up close and personal. My thoughts standing at the edge of this massively perfect-circle deep lake full of water: "somebody built that... and it's one BIG BATTERY".
If you get a chance to visit one of these, I highly recommend it!
I recently watched a video [0] that contrasted all of the OO Design Patterns with Functional Programming equivalents. After reading about how this author wants to make "glue" code "first class" and how the Unix pipe operator is an example of single-character-glue-code, my thoughts immediately went to the aforementioned video presentation. Perhaps my "glue code" is simply gold-old "function composition"?
[Edit] Spoiler alert: each of the design patterns reviewed and contrasted in the video I mentioned seemed to "disappear" in FP since the equivalent is simply to use functions and/or function composition. Recently transitioning from C# to F# for my .NET Core projects, I felt the "glue code" the author mentions disappear in a similar manner with greatly-reduced code bloat.
I think numbers are wonderful and cool abstract thingies. We grow up being taught them (in my case Arabic numerals in base 10) and they become such part of our being that we start to think that we know what “5” is. Then I was introduced to Roman Numerals. Didn’t like those much. That one taught me that 4 is more related to 5 than it is 3. Then some of us learn a base 2 number system or base 16 number system and for a brief moment we question whether we actually knew what “5” was. And then we may learn about Peano and the successor(s…) of zero. Did we really know what “5” was then? What is five-ness really? Perhaps fiveness is a set within a set within a set…
Every interaction our human minds have with fiveness is with a representation or encoding of 5. With each new representation, I’ve experienced fiveness slightly differently.
But I like computers and math. For me, the best to experience oneness with the fiveness is through computation with Lambda Calculus and Church Numerals. Very fond of that encoding.
I recently used "Arcsecond" JavaScript Parser Combinator library to output some abstract syntax based on John Reynold's "Definitional interpreters for higher-order programming languages".
It's based on Haskell's Parsec parser combinator library, and is zero-dependency.
I was convinced to give it a try based on watching the author's YouTube videos "Parser Combinators From Scratch" on "Low Level JavaScript". Enjoyable series - recommended.
I found the first 6 chapters of "Type Theory and Formal Proof" to be amazing for covering the beginning math behind Type Theory. The authors (Nederpelt and Geuvers) don't gloss over assumptions and they build things up step by step. I didn't study this in university but have picked up many books along the way. I'm usually quite lost within the first 10 or 20 pages until picking up Type Theory and Formal Proof. This one took me somewhere between 100 to 200 pages before getting lost. They cover the entire lambda cube.
But then I was able to re-start Thompson's "Type Theory and Functional Programming" and it was clear that I started to understand a lot of it.
If you enjoy the nostalgia of older books like me, then pick up an original copy of "Intuitionistic Type Theory" edited by Per Martin-Löf.
"Type Theory and Functional Programming" by Simon Thompson (PDF available via quick search)
First 120 pages of "Type Theory and Formal Proof" by Rob Nederpelt / Herman Geuvers
For some early stuff on dependent types (also covered in the above), check out "Intuitionistic Type Theory" by Per Martin-Lof
"Computation and Reasoning: A Type Theory for Computer Science" by Zhaouhui Luo
"Type-Driven Development with Idris" by Edwin Brady
"Gentle Introduction to Dependent Types with Idris" by Boro Sitnikovski
"Types and Programming Languages" by Pierce
"Practical Foundations for Programming Languages" by Robert Harper (or any of his YouTube videos re/Type Theory)
"The Little Typer" by Friedman and Christiansen
"Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy" by David Corfield (just took this one to OBX North Carolina to enjoy on my beach vacation last week! Got some salt water in those pages. Also speaks to Category Theory.)
For Category Theory:
"The Joy of Abstraction" (2023) by Euginia Cheng
"Basic Category Theory for Computer Scientists" by Benjamin C. Pierce
"Conceptual Mathematics: A first introduction to categories" by Lawvere and Schanuel
"Categories for the Working Philosopher" by Landry