Proposal: Change Alternative law for some and many
David Feuer
david.feuer at gmail.com
Fri Dec 14 05:03:01 UTC 2018
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20181214/5840c801/attachment.html>
More information about the Libraries
mailing list