Proposal: Change Alternative law for some and many

[Carter Schonwald]

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/e9e848fb/attachment.html>