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