Re: Pointed [Re: 2014 Applicative => Monad proposal]

24 May 2013

      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 
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  [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
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@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@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/