> when I program Haskell, Agda, Isabelle/HOL, or Coq.
That's fair. Although Haskell is a bit of an odd man out in that list, both in terms of its nature and in terms of its typical use case.
> That being said, depending on what sort of functional programming you're doing, a strong background in category theory or meta-programming can enabling (or not).
This is where the analogy between the two books breaks down. When you're using a functional programming language as a proof assistant, category theory can be helpful. But this is far less common than meta-programming.
That's fair. Although Haskell is a bit of an odd man out in that list, both in terms of its nature and in terms of its typical use case.
> That being said, depending on what sort of functional programming you're doing, a strong background in category theory or meta-programming can enabling (or not).
This is where the analogy between the two books breaks down. When you're using a functional programming language as a proof assistant, category theory can be helpful. But this is far less common than meta-programming.
edit: 2nd paragraph.