Well, I am studying Haskell Monads. When I read the Wikibook Category theory article, I found that the signature of monad morphisms looks pretty like tautologies in logic, but you need to convert M a
to ~~A
, here ~
is the logic negation.
return :: a -> M a -- Map to tautology A => ~~A, double negation introduction
(>>=) :: M a -> (a -> M b) -> M b -- Map to tautology ~~A => (A => ~~B) => ~~B
the other operations is also tautologies:
fmap :: (a -> b) -> M a -> M b -- Map to (A => B) -> (~~A => ~~B)
join :: M (M a) -> M a -- Map to ~~(~~A) => ~~A
It's also understood that according to the fact that the Curry-Howard correspondence of normal functional languages is the intuitive logic, not classical logic, so we cannot expect a tautology like ~~A => A
can have a correspondence.
But I am thinking of something else. Why the Monad can only relate to a double negation? what is the correspondence of single negation? This lead me to the following class definition:
class Nomad n where
rfmap :: (a -> b) -> n b -> n a
dneg :: a -> n (n a)
return :: Nomad n => a -> n (n a)
return = dneg
(>>=) :: Nomad n => n (n a) -> (a -> n (n b)) -> n (n b)
x >>= f = rfmap dneg $ rfmap (rfmap f) x
Here I defined a concept called "Nomad", and it supports two operations (both related to a logic axiom in intuitive logic). Notice the name "rfmap" means the fact that its signature is similar to functor's fmap
, but the order of a
and b
are reversed in result. Now I can re-define the Monad operations with them, with replace M a
to n (n a)
.
So now let's go to the question part. The fact that Monad is a concept from category theory seems to mean that my "Nomad" is also a category theory concept. So what is it? Is it useful? Are there any papers or research results exists in this topic?
rfmap
is an operation on contravariant functors. – shachafNomad
looks like half of aMonad
, sincen (n a)
is a well definedMonad
. – Earth Engine