<div dir="ltr"><div dir="auto">Currently, we document this law:<div dir="auto"><br></div><div dir="auto"><div dir="auto">> If defined, some and many should be the least solutions of the equations:</div><div dir="auto">></div><div dir="auto">>   some v = (:) <$> v <*> many v</div><div dir="auto">>   many v = some v <|> pure []</div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><br></div><div dir="auto">For example, we currently require</div><div dir="auto"><br></div><div dir="auto">    some Nothing = Nothing</div><div dir="auto">    some (Just x) = _|_</div><div dir="auto"><br></div><div dir="auto">    many Nothing = Just []</div><div dir="auto">    many (Just x) = _|_</div><div dir="auto"><br></div><div dir="auto">But if we weaken the law, we could instead use</div><div dir="auto"><br></div><div dir="auto">    some Nothing = Nothing</div><div dir="auto">    some (Just x) = Just (repeat x)</div><div dir="auto"><br></div><div dir="auto">    many Nothing = Just []</div><div dir="auto">    many (Just x) = Just (repeat x)</div><div dir="auto"><br></div><div dir="auto">This seems strictly, albeit slightly, more interesting.</div><div dir="auto"><br></div><div dir="auto">More significantly, I think, the instance for functor products can also get much better-defined:</div><div><br></div><div>    some (x :*: y) = some x :*: some y</div><div>    many (x :*: y) = many x :*: many y</div><div><br></div><div>That strikes me as an improvement that may actually be of some practical value.</div></div></div>
</div>