Proposal: Change Alternative law for some and many

[Gershom B]

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