Pointed [Re: 2014 Applicative => Monad proposal]

[Andreas Abel]

Pointed f  alone does not give you any guarantees, you cannot exclude 
weird definitions like the one given by you or just

   point a = undefined

which is even worse, because it does not even give you non-emptyness of 
(f a).

But there are many useful type classes that cannot give you guarantees 
by themselves.  Consider Show and Read (used as printer and parser for 
abstract syntax).  Nothing prevents you to define show to print the 
empty string or Nietzsche quotes.  The defect becomes apparant only in 
the presence of Read, when laws like

    read . show == id

fail.  I don't suppose that every type class must unfold its full 
meaning by itself.

Thanks for suggesting MonoidOver, but I do not see any more laws coming 
from that than from Pointed + Monoid.  As long as you cannot take apart 
a monoid element into its atoms, you cannot state that embed does what 
you want.

Anyway, I think Pointed is useful, but its uses are not so frequent that 
it must be in base.  It is very little work to define the class and the 
instances one needs, so I can continue to do so if I need it.

On the other hand, in category theory Pointed is a standard notion, so 
it would make sense to push this piece of vocabulary.  Also, I see the 
singleton list constructor (:[]) quite often, and "point" would be more 
readable than this.

Yet, it seems that there is no majority for Pointed, so discussing this 
much longer is pointless.

On 25.05.13 5:33 PM, Dan Doel wrote:
> On Fri, May 24, 2013 at 2:15 PM, Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto:andreas.abel at ifi.lmu.de>> wrote:
>
>     Pointed is a superclass of Applicative, taking the role of pure, but
>     not related to Functor.  I do not see the problem.
>
>
> The problem is: what is a Pointed? It's just anything with kind * -> *
> for which you can write a function with that type. Is the following a
> good definition, for instance?
>
>      newtype Foo a = Foo ((a -> a -> a) -> a -> a)
>
>      instance Pointed Foo where
>        point x = Foo $ \m -> m x
>
> How about this:
>
>      newtype Bar r a = Bar (a -> r)
>
>      instance Monoid m => Pointed (Bar m) where
>        point _ = Bar $ const mempty
>
> (Bar m is even a monoid for monoids m).
>
> In particular...
>
> John Wiegley wrote:
>  > (in order to limit the scope of what must be reasoned about)
>
> Pointed is pretty bad for this. Or, maybe, it's good: there's nothing to
> reason about, because there's nothing you can reason about. It just does
> _something_ unspecified. Hopefully something that is good for combining
> with some other type class.
>
> I've reluctantly come around to the Apply/Bind classes (despite them
> having bad names), because they actually follow the way people typically
> build up structure in algebra. Rarely do you see people defining 'a
> monoid is a pointed set equipped with an associative binary operation
> that uses the point as an identity.' It's much more likely that you see,
> 'a monoid is a semigroup with an identity for the binary operation.' I
> suspect that's even how many people would like to see the hierarchy at
> this point: Semigroup m => Monoid m. And not Default m => Monoid m,
> because Default is just ad-hoc nonsense (even if it's sometimes useful).
>
> To answer your original question, perhaps a somewhat better way of
> characterizing the problem is probably talking about 'monoids m over
> type a'. Perhaps something like:
>
>      class Monoid m => MonoidOver a m | m -> a where
>        embed :: a -> m
>
> which expresses that m is expected to be generated (as a monoid) by a in
> some way. Then maybe you can say something about how it interacts with
> the Monoid operations, which seems preferable to me to, "the operation
> of this class does anything, except if the type is also a monoid, or if
> it's also a monad...."
>
> Anyhow, I'm -1 on Pointed, in case anyone couldn't tell.
>
> -- Dan

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/