Joel Sjögren: Great job! These solutions are absolutely correct.

> I think I first encountered the notion of positive and negative positions in an error message in Agda. Something like There is an air of fundamentality about it. Or maybe it's just part of our boolean culture.

I'd say these notions are fundamental.

I first encountered them in the [Sahlqvist Theorem]( in modal logic, where consequents must always be positive.

They also appear in the [Modal μ-calculus]( Here you can only construct \\(\mu x. \phi(x)\\) if \\(\phi\\) is positive. In fact, in the modal-\\(\mu\\) calculus positive formulae express _monotone maps_ on power set algebra of the possible worlds in Kripke model. In this setting \\(\mu x. \phi(x)\\) expresses the fixed point of \\(\phi\\) as a monotone map, and it is well defined as a consequence of the [Knaster-Tarski theorem](

John Baez has a discussion of monotone maps in his thread [Lecture 4 - Chapter 1: Galois Connections]( For anyone interested, I'll move this discussion over there (since it's not really about Haskell)...