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 https://stackoverflow.com/questions/2583337/strictly-positive-in-agda. 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](https://www.encyclopediaofmath.org/index.php/Sahlqvist_theorem) in modal logic, where consequents must always be positive.

They also appear in the [Modal μ-calculus](https://en.wikipedia.org/wiki/Modal_%CE%BC-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](https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem).

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

> I think I first encountered the notion of positive and negative positions in an error message in Agda. Something like https://stackoverflow.com/questions/2583337/strictly-positive-in-agda. 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](https://www.encyclopediaofmath.org/index.php/Sahlqvist_theorem) in modal logic, where consequents must always be positive.

They also appear in the [Modal μ-calculus](https://en.wikipedia.org/wiki/Modal_%CE%BC-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](https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem).

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