Proposal: Change Alternative law for some and many

[David Feuer]

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20181214/f7c53066/attachment.html>