My previous few posts have been about cartesian closed categories (CCCs). In From Haskell to hardware via cartesian closed categories, I gave a brief motivation: typed lambda expressions and the CCC vocabulary are equally expressive, but have different strengths:
- In Haskell, the CCC vocabulary is overloadable and so can be interpreted more flexibly than lambda and application.
- Lambda expressions are friendlier for human programmers to write and read.
By automatically translating lambda expressions to CCC form (as in Overloading lambda), I hope to get the best of both options.
An interpretation I’m especially keen on—and the one that inspired this series of posts—is circuits, as described in this post.