Proposal: Change Alternative law for some and many

Fri Dec 14 17:34:15 UTC 2018

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 at 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 at 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 at 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 at 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 at 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 at 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 at 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 at 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 at 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 at haskell.org
>>>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>>>>
>>>>>>> _______________________________________________
>>>>> Libraries mailing list
>>>>> Libraries at haskell.org
>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>>
>>>>> _______________________________________________
>>>> Libraries mailing list
>>>> Libraries at haskell.org
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>
>>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20181214/fd2f49d6/attachment.html>