Proposal: Change Alternative law for some and many

[Gershom B]

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