A Neighborhood of Infinity

submited by
Style Pass
2021-09-23 10:30:06

Modal logics usually have these rules:   f (a -> b) -> f a -> f b (This corresponds to the Applicative class, which may one day be made a superclass of Monad.)   f a -> a Monads do not in general satisfy this. Perhaps comonads or something?

Eeep! The defining property of a functor is this:   fmap :: (a -> b) -> f a -> f b and not   ap :: f (a -> b) -> f a -> f b fmap is definitely not provable in any modal logic.

ashley, OK, I have some spare moments now. I've spent quite a bit of time tinkering round with various axioms of modal logic but as you notice, things have a habit of not quite working out the way you want. There *is* a nice interpretation of □ as something like C/C++'s 'const'. There's a bunch of papers about it and I said something about it here. I've also seen some papers that uses the axiom GL (ie. Loeb's theorem) as a basis for describnig recursive types.

I've been playing around with the axioms to see if either □ or ◊ behave like some well-known Haskell class. Firstly, neither of them are Functors, since you cannot prove either of these even in S5:   (a→b)→(□a→□b)   (a→b)→(◊a→◊b) The second is less obvious than the first, but consider temporal logic: just because 'a' implies 'b' now, and 'a' is sometimes true, it doesn't mean that 'b' is ever true. This is unfortunate, since axioms T and 4 are suggestive of Monads for ◊:   T: a → ◊a   4: ◊◊a → ◊a K on the other hand doesn't look like anything I've seen in Haskell:   K: (◊a → ◊b) → ◊(a → b)

Leave a Comment