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)