How Much Is in a Square? Calculating Functional Programs with Squares

Explore a novel geometric approach to functional programming through the lens of "magic squares" in this 30-minute conference presentation from ICFP 2025. Discover how semi-commutative squares serve as a powerful graphical tool for expressing and reasoning about functional programs, with applications spanning logic, database modeling, and formal semantics. Learn how these geometric constructs, where binary relations form the sides and path comparisons define the squares themselves, can compose and provide elegant solutions across multiple domains. Examine free-theorem magic squares and their particularly productive properties, while gaining insights into a generic, induction-free theory for foldr and foldl operations. Understand how this relational approach to teaching functional programming reveals that foldl s = foldr (flip_s) holds under milder conditions than traditionally required, supported by Galois connections theory.