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 requiresome Nothing = Nothingsome (Just x) = _|_many Nothing = Just []many (Just x) = _|_But if we weaken the law, we could instead usesome Nothing = Nothingsome (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 ymany (x :*: y) = many x :*: many yThat 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