I understand that in terms of the specified applicative operations it wouldn’t work.  

I guess my confusion is that I think of some and many combinators in terms of parser combinators style behavior, where some p can return any positive length list of consecutive values. 

If we were to model these algrbrsically as formal power series 

I’d think of many x = sum_k (x^k / k! ) = exp x

And then some x = many x -1. 
—- because size zero products of x aren’t a valid element 


A lot of expressive power in Haskell comes from being able to use laziness to have the same code work on values that act strict (least fixed point) and those which arent (greatest fixed point). 

 My questions are this 
1) how would this change impact expected behavior of parser combinator libraries using some and many? 
2) what is a calculation I can do today with some and many  that I can’t do with this change?
3) what’s a calculation I can do with some and many only once we have this change ? 


On Fri, Dec 14, 2018 at 12:18 PM David Feuer <david.feuer@gmail.com> wrote:
No, you can't return just a singleton list. If many (Just 3) = Just [3], then
some (Just 3) = liftA2 (:) (Just 3) (Just [3]) = Just [3,3]. But then
many (Just 3) = some (Just 3) <|> pure [] = Just [3,3], a contradiction.
If instead some (Just 3) = Just [3], then many (Just 3) = Just [3] <|> pure [] = Just [3],
which gets us back where we started.

The definitions I gave for Maybe (and also the ones for [], which I haven't mentioned) are equivalent to "lazifying" the defaults in a straightforward manner.

  -- This one is the default
  some v = liftA2 (:) v (many v)

  -- This one is much like the default. But note that (barring non-termination),
  -- isJust (m <|> pure []) == True
  -- So we push the case match under the constructor application:
  many v = Just $
    case some v <|> pure [] of
      Just x -> x

These definitions give the same results as the repeat-based ones I showed before. Are these greatest fixed points? I believe so, but I don't really know enough about domain theory and such to say for sure.

On Fri, Dec 14, 2018 at 10:11 AM Carter Schonwald <carter.schonwald@gmail.com> wrote:
I guess I’m just surprised that some can’t return just a singleton list of x.  Or maybe I’m reading the notation of this discussion wrong.  

On Fri, Dec 14, 2018 at 9:49 AM Carter Schonwald <carter.schonwald@gmail.com> wrote:
Hello!

Am I correct in reading the example definitions you provided as being the greatest fixed points?

On Fri, Dec 14, 2018 at 12:58 AM David Feuer <david.feuer@gmail.com> wrote:
Some of it, for sure. Where Capriotti mentioned "It's a fixpoint, but not the least," this fixes it. Another potentially interesting relaxation would be

   some v >= (:) <$> v <*> many v
   many v >= some v <|> pure []

but that seems considerably more likely to limit practically useful reasoning.

On Fri, Dec 14, 2018 at 12:47 AM Gershom B <gershomb@gmail.com> wrote:
Some interesting prior discussion on the topic. I haven’t worked out how much of what’s discussed there would do better in this setting… https://www.reddit.com/r/haskell/comments/2j8bvl/laws_of_some_and_many/

That said, I think this probably is a good improvement.

-g


On December 14, 2018 at 12:30:52 AM, David Feuer (david.feuer@gmail.com) wrote:

Note: even making liftA2 and (<|>) lazy ends up leading to some bottoms that the proposed definition avoids. I don't honestly understand just why that is.

On Fri, Dec 14, 2018 at 12:22 AM David Feuer <david.feuer@gmail.com> wrote:
With the current law and (default) definitions,

some (x :*: y) = liftA2 (:) (x :*: y) (many (x :*: y))
many (x :*: y) = some (x :*: y) <|> pure []

Since liftA2 is strict in its third argument, and (<|>) is strict in its first argument, some = many = const _|_ regardless of the underlying functors.

On the other hand, with the proposed law and the proposed definitions, the methods will behave well for products if they behave well for the underlying functors.

On Fri, Dec 14, 2018 at 12:12 AM Gershom B <gershomb@gmail.com> wrote:
Can you give an example of where the new definitions and current definitions of functor products would yield different behavior?

-g


On December 14, 2018 at 12:03:32 AM, David Feuer (david.feuer@gmail.com) wrote:

Currently, we document this law:

> If defined, some and many should be the least solutions of the equations:
>
>   some v = (:) <$> v <*> many v
>   many v = some v <|> pure []

This seems a bit too strong. I believe we should weaken "should be the least solutions of" to "should obey". This allows non-bottoming implementations for more types. I would be surprised if the change would meaningfully weaken the value of the law for reasoning about real programs.

For example, we currently require

    some Nothing = Nothing
    some (Just x) = _|_

    many Nothing = Just []
    many (Just x) = _|_

But if we weaken the law, we could instead use

    some Nothing = Nothing
    some (Just x) = Just (repeat x)

    many Nothing = Just []
    many (Just x) = Just (repeat x)

This seems strictly, albeit slightly, more interesting.

More significantly, I think, the instance for functor products can also get much better-defined:

    some (x :*: y) = some x :*: some y
    many (x :*: y) = many x :*: many y

That strikes me as an improvement that may actually be of some practical value.
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries