Interesting operators in Haskell that obey modal axioms

user65526 Source

I was just looking at the type of map :: (a -> b) -> [a] -> [b] and just the shape of this function made me wonder whether we could see the list forming operator [ ] as obeying various axioms common to normal modal logics (e.g, T, S4, S5, B), since we seem to have at least the K-axiom of normal modal logics, with [(a -> b)] -> [a] -> [b].

This leads to my question: are there familiar, interesting operators or functors in Haskell which have the syntax of modal operators of a certain kind, and which obey the axioms common to normal modal logics (i.e, K, T, S4, S5 and B)?

This question can be sharpened and made more specific. Consider an operator L, and its dual M. Now the question becomes: are there any familiar, interesting operators in Haskell with some of the following properties:

(1) L(a -> b) -> La -> Lb

(2) La -> a

(3) Ma -> L(M a)

(4) La -> L(L a)

(5) a -> L(M a)

It would be very interesting to see some nice examples.

I've thought of a potential example, but it would be good to know whether I am correct: the double negation translation with L as not not and M as not. This translation takes every formula a to its double negation translation (a -> ⊥) -> ⊥ and, crucially, validates axioms (1)-(4), but not axiom (5). I asked a question here and it seems the double negation translation can be simulated via the continuation monad, the endofunctor taking every formula a to its double negation translation (a -> ⊥) -> ⊥. There Derek Elkins notes the existence of a couple of double negation translations corresponding, via the Curry-Howard isomorphism, to different continuation-passing style transforms, e.g. Kolmogorov's corresponds to the call-by-name CPS transform.

Perhaps there are other operations that can be done in the continuation monad via Haskell which can validate axioms (1)-(5).

(And just to eliminate one example: there are clear relations between so-called Lax logic and Monads in Haskell, with the return operation obeying the laws of the modal operator of this logic (which is an endofunctor). I am not interested so much in those examples, but in examples of Haskell operators which obey some of the axioms of modal operators in classical normal modal logics)



comments powered by Disqus