Interesting operators in Haskell that obey modal axioms

Question

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)

Ginny

It is not garbage, it is simply a list of functions, all map as to bs. – Someway

I don't know what your question is but [a -> b] -> [a] -> [b] is the type of (<*>) specialized to the [] instance of Applicative. – Keck

We have (<*>) :: [a -> b] -> [a] -> [b], and also for the "function modality" we have (<*>) :: (e -> (a -> b)) -> (e -> a) -> (e -> b) which is the well-known K combinator. Probably just coincidence that they share the K name, though. ;-) – Wheat

@DanielWagner Also probably a coincidence that these coincidences keep popping up all over the place. – Keck

Does the operator <*> obey any of the other axioms of normal modal logics? – Ginny

Here are its laws. – Keck

Do other operators in Haskell obey other axioms common to normal modal logics. For example the T axiom, the S4 axiom and the S5 axiom, etc? – Ginny

On the "too broad" close votes: FWIW, I don't feel this question should be closed. It is phrased in a rather speculative way (likely due to the OP's unfamiliarity with Haskell, which was mentioned in the original revision of the question); however, at its core there is a fairly reasonable question about whether the functor classes have something to do with modal operators. – Tetrafluoroethylene

L sure as heck looks like a comonad, not sure what a corresponding M would be offhand. But e.g. known comonads such as nonempty lists of a, pairs (w,a) would satisfy. – Mimeograph

Ah, so extract is like (2) above (the T-axiom in modal logic), duplicate is like (4) (the S4 axiom). A simple example of an operator for (3) would take M to denote False and L to denote Truth, and this interpretation (obviously) works for some of the other examples. – Ginny

Known comonads such as nonempty lists of a, pairs (w,a) would satisfy what, sorry? – Ginny

You should definitely read Getting a Quick Fix on Comonads, which argues for (restricted use of) ComonadApply for some modal logic. – Gunas

Very interesting indeed! However, it still does not help with axioms (3) and (5) in my question. I've thought of a potential example: the double negation translation with L as not not and M as not validates all the axioms above. I asked this question here math.stackexchange.com/questions/2347437/… in which I argued the double negation translation was an example of the continuation monad. The endofunctor in this case would take every formula a to its double negation translation (a -> ⊥) -> ⊥. – Ginny

Are you sure about (5)? If L is not.not and M is not, that would give a -> not (not (not a)) which seems a touch disturbing. – Stern

Ah, sorry, my mistake. It doesn't hold of (5) obviously! – Ginny

Can anyone think of any other examples of continuations which obey some of the axioms (1)-(5)? – Ginny

Yeah, echoing what people have said already, my first impression here is that M ≈ Monad and L ≈ ComonadApply (#1: (Applicative f) => f (a -> b) -> f a -> f b; #2: extract :: (Comonad f) => f a -> a; #4: duplicate :: (Comonad f) => f a -> f (f a)) or possibly MonadTrans (#3: lift :: (MonadTrans t, Monad m) => m a -> t (m a); #5: instance (MonadTrans t, Monad m) => Monad (t m) where return :: a -> t (m a)). But I’ve only really worked with epistemic modal logic (□ = “known to be true”, ◇ = “not known to be false”), not too familiar with modal logic in general. – Rambert

Comonads obey the T axiom (my (1)), the S4 axiom (my (4)). Do comonads obey the K axiom (my (1))? That is, does (Applicative f) => f (a -> b) -> f a -> f b when f is a comonad? If it does, then a Comonadic operator behaves syntatically like the necessity operator of S4 modal logic (the modal logic intertranslatable with intuitionistic logic via Godel's famous translation). Do monad transformers obey any of the other axioms I listed in my question? – Ginny

Hrm, K, T, S4, S5 are normal... – Attenuation

I meant to write "normal", but had non-normal modal logics in my mind, having just read a book on them! – Ginny

@DanielWagner <*> is the S combinator though, not K. – Zippy

@WillNess Whoops, you're absolutely right! – Wheat

Answer 1

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:

• At a glance, it seems the symmetrical move of making D trivial leads us to something very much like ComonadApply. I say "very much like" largely due to the functorial strength of Haskell Functors, the matter being that x /\ B y -> B (x /\ y) is an awkward thing to have if you are looking for a conventional necessity modality.

• Kenneth Foner's Functional Pearl: Getting a Quick Fix on Comonads (thanks to dfeuer for the reference) works towards expressing intuitionistic K4 in Haskell, covering some of the difficulties along the way (including the functorial strength issue mentioned above).

• Matt Parsons' Distributed Modal Logic offers a Haskell-oriented presentation of intuitionistc S5 and an interpretation of it, originally by Tom Murphy VII, in terms of distributed computing: B x as a x-producing computation that can be run anywhere on a network, and D x as an address to a x somewhere on it.

• Temporal logics can be related via Curry-Howard to functional reactive programming (FRP). Suggestions of jumping-off points include de Paiva and Eades III, Constructive Temporal Logic, Categorically (2017), as well as this blog post by Philip Schuster alongside this interesting /r/haskell thread about it.

Tetrafluoroethylene