Proposal: Change Alternative law for some and many

[David Feuer]

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