Proposal: Change Alternative law for some and many

[David Feuer]

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