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
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@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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries