Proposal: Change Alternative law for some and many

[Carter Schonwald]

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