Pointed [Re: 2014 Applicative => Monad proposal]

[Andreas Abel]

You cannot expect much from point.  It could give you the empty
collection, a singleton, or multiple copies of the same element.

foldMap point could give you the unit of the monoid, if point is 
implemented "badly".  Tough luck.

Laws only arise with other operations, e.g. in Applicative or Monad.

However: I guess if you had something like "natural functors"

   Foundational, compositional (co)datatypes for higher-order 
logic—Category theory applied to theorem proving
Dmitriy Traytel, Andrei Popescu, and J. C. B. In 27th Annual IEEE 
Symposium on Logic in Computer Science (LICS 2012), pp. 596–605, IEEE, 
2012.

or "set-based functors" (Peter Aczel)

   A Predicative Strong Normalisation Proof for a λ-calculus with 
Interleaving Inductive Types
     Thorsten Altenkirch and Andreas Abel (2000)
     Types for Proofs and Programs, International Workshop, TYPES '99
     Lökeberg, Sweden, June 1999. LNCS 1956. ©Springer-Verlag

(good name lacking still) like

   class SetBased f where
     urelements :: f a -> [a]

then you would expect

   urelements (point a) = [a]

But unfortunately, for fs beyond collections, urelements is not computable:

   urelements :: (r -> a) -> [a]
   urelements f = "union x:r. f x"

Still this might serve as a (non-testable) specification of point.

You throwing in some thoughts,
Andreas


On 24.05.2013 19:56, Edward A Kmett wrote:
> This is precisely the situation I am referring to when I mention ad
> hoc casewise reasoning.
>
> What laws say that 'foldMap point' does anything useful? Given just
> the type signature what reasoning can you do?
>
> Without knowing the particular instances involved, you get nothing.
>
> With Set you get a glued together Set, but Maybe is going to try to
> smash together the elements under the Maybe with some extra
> Semigr^H^H^H^H^H^HMonoid.
>
> Pointed requires ad hoc reasoning for virtually every use case. The
> only law you can state for it is a free theorem for its type.
>
> On the other hand with classes like Apply or Bind you get access to
> lots of useful semigroup-like structures you can still reason about
> in general, not in particular, including things that can't be made
> Applicative/Monadic. (e.g. IntMap).
>
> On May 24, 2013, at 1:02 PM, Andreas Abel <andreas.abel at ifi.lmu.de>
> wrote:
>
>> I do not use Pointed a lot, but a situation where it comes natural
>> is when I want to emit elements into a collection f.  Then I need
>>
>> Pointed f    -- to emit a single element Monoid (f a) -- to join
>> two collections
>>
>> Using Applicative or Monad is overdoing it.
>>
>> Maybe you have a better suggestion how to organize my task which I
>> have not considered yet...
>>
>> Cheers, Andreas
>>
>> On 24.05.2013 17:28, Roman Cheplyaka wrote:
>>> I completely agree with Edward here.
>>>
>>> * Edward Kmett <ekmett at gmail.com> [2013-05-24 11:20:51-0400]
>>>> For the record I'm actually -1 on including Pointed.
>>>>
>>>> My experience is that there are very few uses for the class
>>>> that permit you to reason about your code without one-off ad
>>>> hoc reasoning based on the particular instance you are given.
>>>> Now, the Apply and Bind classes on the other hand... =) Though,
>>>> to be fair, I couldn't seriously propose including either of
>>>> those, either. Even I can't be bothered to instantiate them
>>>> all the time!
>>>>
>>>> -Edward
>>>>
>>>>
>>>> On Fri, May 24, 2013 at 11:13 AM, Andreas Abel
>>>> <andreas.abel at ifi.lmu.de>wrote:
>>>>
>>>>> +1 AMP +1 MINIMAL +1 Pointed in base
>>
>> -- 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/
>


-- 
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/