haskellmodal-logic

Interesting operators in Haskell that obey modal axioms

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 https://math.stackexchange.com/questions/2347437/continuations-in-mathematics-nice-examples 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 https://www.sciencedirect.com/science/article/pii/S0890540197926274 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)

Solution

  • Preliminary note: I apologise for spending a good chunk of this answer talking about Propositional Lax Logic, a topic you are very familiar with and not too interested in as far as this question is concerned. In any case, I do feel this theme is worthy of broader exposure -- and thanks for making me aware of it!

    The modal operator in propositional lax logic (PLL) is the Curry-Howard counterpart of Monad type constructors. Note the correspondence between its axioms...

    DT: x -> D x
D4: D (D x) -> D x
DF: (x -> y) -> D x -> D y

    ... and the types of return, join and fmap, respectively.

    There are a number of papers by Valeria de Paiva discussing intuitionistic modal logics and, in particular, PLL. The remarks about PLL here are largely based on Alechina et. al., Categorical and Kripke Semantics for Constructive S4 Modal Logic (2001). Interestingly, that paper makes a case for the PLL being less weird than it might seem at first (cf. Fairtlough and Mendler, Propositional Lax Logic (1997): "As a modal logic it is special because it features a single modal operator [...] that has a flavour both of possibility and necessity"). Starting with CS4, a version of intuitionistic S4 without distribution of possibility over disjunction...

    B stands for box, and D for diamond

BK: B (x -> y) -> (B x -> B y)
BT: B x -> x
B4: B x -> B (B x)

DK: B (x -> y) -> (D x -> D y)
DT: x -> D x
D4: B (B x) -> B x

    ... and adding x -> B x to it causes B to become trivial (or, in Haskell parlance, Identity), simplifying the logic to PLL. That being so, PLL can be regarded as a special case of a variant of intuitionistic S4. Furthermore, it frames PLL's D as a possibility-like operator. That is intuitively appealing if we take D as the counterpart to Haskell Monads, which often do have a possibility flavour (consider Maybe Integer -- "There might be an Integer here" -- or IO Integer -- "I will get an Integer when the program is executed").

    A few other possibilities: