Pointed [Re: 2014 Applicative => Monad proposal]

[Daniel Peebles]

The objection isn't that Pointed has no self-contained laws or that
typeclasses can't have laws relating them to other classes, but that the
only law relating Pointed to another class (Functor, saying fmap f . pure =
pure . f) is provided by parametricity anyway.

I don't think undefined adds much to the discussion. We're saying that even
in Agda, Pointed (over the Set-like Agda category) doesn't really abstract
over things you want to abstract over. The fact that Set.singleton doesn't
require an ordering is almost an implementation accident. How many other
things are Pointed in a "meaningful" way without being more as well? And
what do you define as meaningful, to exclude Dan's ridiculous instances?


On Sat, May 25, 2013 at 5:52 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> 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 <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/ <http://www2.tcs.ifi.lmu.de/~abel/>
>
> ______________________________**_________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/**mailman/listinfo/libraries<http://www.haskell.org/mailman/listinfo/libraries>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20130526/d2d13322/attachment.htm>