Proposal: Applicative => Monad: Call for consensus

[roconnor at theorem.ca]

On Tue, 4 Jan 2011, Iavor Diatchki wrote:

> Hello, I am also skeptical about the need to add "join" to the monad 
> class.  My reasoning is that I doubt that one can define an instance 
> where "join" and "bind" perform differently, so we are just adding 
> overhead, both cognitive (because the Monad class get more complex) and 
> resource-wise (because dictionaries need to carry an additional method).

In my completion monad, "join" is more efficent than "bind id"

Here are the functions (see Chapter 10 of <http://r6.ca/thesis.pdf>):

return a = \eps -> a
fmap f x = \eps -> f (x ((modulus f eps)/2))
join x   = \eps -> x (eps/2) (eps/2)
bind f x = join (fmap f x)

Now look at the value of "bind id x"

bind id x = join (fmap id x)
           = \eps -> (fmap id x) (eps/2) (eps/2)
           = \eps -> id (x ((modulus id (eps/2)/2)) (eps/2)
           = \eps -> id (x ((id (eps/2)/2)) (eps/2)  -- modulus id = id
           = \eps -> x (eps/4) (eps/2)

compared with

join x    = \eps -> x (eps/2) (eps/2)

The two results are equivalent under the equivalence relation for 
completion type:

     x == y iff forall eps1 eps2. |(x eps1) - (y eps2)| <= eps1 + eps2.

but the direct definition of join is more efficent than the definition 
using bind id.

(as an aside, one would think (or at least I thought) that one could define
    fmap f x = \eps -> f (x (modulus f eps))
and then join and bind id would be equivalent.  But it turns out that this 
definition of fmap doesn't work in general.  See the paragraph after 
Definition 10.14 on page 71 of my thesis for a counterexample.)

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''