10

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)

duplode
  • 33,731
  • 7
  • 79
  • 150
user65526
  • 685
  • 6
  • 19
  • It is not garbage, it is simply a list of functions, all map `a`s to `b`s. – Willem Van Onsem Mar 13 '18 at 17:59
  • 2
    I don't know what your question is but `[a -> b] -> [a] -> [b]` is the type of `(<*>)` specialized to the `[]` instance of `Applicative`. – Rein Henrichs Mar 13 '18 at 18:00
  • 3
    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. ;-) – Daniel Wagner Mar 13 '18 at 18:01
  • 1
    @DanielWagner Also probably a coincidence that these coincidences keep popping up all over the place. – Rein Henrichs Mar 13 '18 at 18:01
  • Does the operator `<*>` obey any of the other axioms of normal modal logics? – user65526 Mar 13 '18 at 18:05
  • 1
    [Here are its laws](https://hackage.haskell.org/package/base-4.10.1.0/docs/Control-Applicative.html). – Rein Henrichs Mar 13 '18 at 18:06
  • 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? – user65526 Mar 13 '18 at 18:07
  • 3
    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. – duplode Mar 13 '18 at 19:36
  • 4
    `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. – luqui Mar 13 '18 at 21:25
  • 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. – user65526 Mar 13 '18 at 21:47
  • Known comonads such as nonempty lists of `a`, pairs `(w,a)` would satisfy what, sorry? – user65526 Mar 13 '18 at 21:52
  • 2
    You should definitely read [Getting a Quick Fix on Comonads](https://github.com/kwf/GQFC), which argues for (restricted use of) `ComonadApply` for some modal logic. – dfeuer Mar 13 '18 at 22:20
  • 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 https://math.stackexchange.com/questions/2347437/continuations-in-mathematics-nice-examples 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 -> ⊥) -> ⊥`. – user65526 Mar 13 '18 at 22:35
  • 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. – pigworker Mar 14 '18 at 12:01
  • Ah, sorry, my mistake. It doesn't hold of (5) obviously! – user65526 Mar 14 '18 at 12:09
  • Can anyone think of any other examples of continuations which obey some of the axioms (1)-(5)? – user65526 Mar 14 '18 at 12:10
  • 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. – Jon Purdy Mar 15 '18 at 04:28
  • 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? – user65526 Mar 15 '18 at 09:11
  • Hrm, K, T, S4, S5 are normal... – Stanislav Kralin Mar 18 '18 at 20:53
  • I meant to write "normal", but had non-normal modal logics in my mind, having just read a book on them! – user65526 Mar 19 '18 at 10:11
  • 1
    @DanielWagner `<*>` is the *S* combinator though, not *K*. – Will Ness Oct 03 '18 at 07:25
  • @WillNess Whoops, you're absolutely right! – Daniel Wagner Oct 03 '18 at 12:26

1 Answers1

6

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.

duplode
  • 33,731
  • 7
  • 79
  • 150