Your definition of monads is wrong. It has nothing to do with join, their time of evaluation or 'imperative vs functional reasoning' lol.
Here are the monadic laws proven with the Promise definitions from above - in js.
// pure :: a -> m aconstpure=v=>Promise.resolve(v);// (>>=) :: m a -> (a -> m b) -> m b constbind=ma=>a2mb=>ma.then(a2mb);// monadic laws// 1. left identity - pure a >>= f ≡ f aconstf=v=>pure(v+1);bind(pure(1))(f)// == f(1) ✔// 2. right identity - m >>= pure ≡ mconstm=pure(1);bind(m)(pure)// == m ✔// 3. associativity - (m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)constm=pure(1);constf=v=>pure(v+1);constg=v=>pure(v*2);bind(bind(m)(f))(g)// == pure(4) ✔bind(m)(x=>bind(f(x))(g))// == pure(4) ✔
You're also wrong about the fact that the promises don't evaluate to the representation of an effect first. Of course they do. The point in time the underlying implementation decides to consume that value has no significance whatsoever. As I said - you're mixing up concepts, don't understand monads and likely don't understand Promises either.
This is the first time I've heard that monads have nothing to do with the join operation. You should share this revolutionary insight with the mathematics community.
Regarding the "proof" of the monadic laws above, unfortunately the laws don't hold for the definitions given (the proof-by-single-example notwithstanding). In fact, the definitions are not even well-typed.
Conveniently, to disprove something requires only a single counterexample:
// Function composition// :: a -> aconstid=x=>x// :: (b -> c) -> (a -> b) -> a -> cconstcompose=f=>g=>x=>f(g(x))// A pair of operations witnessing that a particular type constructor forms a monad// :: type Monad m = { pure: a -> m a, bind: m a -> (a -> m b) -> m b }// The associativity law satisfied by any monad// :: Monad m -> [m Int, m Int]consttestAssociativity=({pure,bind})=>{// Some selected inputs// :: m Intconstmx=pure(42)// :: a -> m (m a)constf=compose(pure)(pure)// :: m a -> m aconstg=ma=>bind(ma)(pure)// associativity:// (mx >>= f) >>= g// ===// mx >>= \x -> f x >>= g// :: m Intconstml=bind(bind(mx)(f))(g)// :: m Intconstmr=bind(mx)(x=>bind(f(x))(g))return[ml,mr]}// The array monad// :: Monad Arrayconstarray={pure:v=>[v],bind:ma=>a2mb=>ma.reduce((p,a)=>[...p,...a2mb(a)],[])}// Is it really a monad?const[a1,a2]=testAssociativity(array)console.log(a1)console.log(a2)// The promise "monad"// :: Monad Promiseconstpromise={pure:v=>Promise.resolve(v),bind:ma=>a2mb=>ma.then(a2mb)}// Is it really a monad?const[p1,p2]=testAssociativity(promise)p1.then(x=>{console.log(x)})p2.then(x=>{console.log(x)})
I'd like to have discussed how the word "monad" refers to a particular kind of endofunctor with join and pure natural transformations, but I really have to take a break from this conversation. I don't mind discussing things with people I disagree with, but the complete lack of manners displayed in your comments goes poorly with your total ignorance of the subject.
For further actions, you may consider blocking this person and/or reporting abuse
We're a place where coders share, stay up-to-date and grow their careers.
Your definition of monads is wrong. It has nothing to do with
join
, their time of evaluation or 'imperative vs functional reasoning' lol.Here are the monadic laws proven with the Promise definitions from above - in js.
You're also wrong about the fact that the promises don't evaluate to the representation of an effect first. Of course they do. The point in time the underlying implementation decides to consume that value has no significance whatsoever. As I said - you're mixing up concepts, don't understand monads and likely don't understand Promises either.
This is the first time I've heard that monads have nothing to do with the join operation. You should share this revolutionary insight with the mathematics community.
Regarding the "proof" of the monadic laws above, unfortunately the laws don't hold for the definitions given (the proof-by-single-example notwithstanding). In fact, the definitions are not even well-typed.
Conveniently, to disprove something requires only a single counterexample:
I'd like to have discussed how the word "monad" refers to a particular kind of endofunctor with
join
andpure
natural transformations, but I really have to take a break from this conversation. I don't mind discussing things with people I disagree with, but the complete lack of manners displayed in your comments goes poorly with your total ignorance of the subject.