[Haskell-cafe] Splitting off many/some from Alternative

[Ross Paterson]

On Thu, Dec 15, 2011 at 02:19:34AM +0000, Gregory Crosswhite wrote:
> On Dec 15, 2011, at 12:03 PM, Ross Paterson wrote:
> 
>     The current definition says that some and many should be the least
>     solutions of the equations
> 
>        some v = (:) <$> v <*> many v
>        many v = some v <|> pure []
> 
>     We could relax that to just requiring that they satisfy these equations
>     (which I think is what John wants).  In that case there would be another
>     possible definition for Maybe:
> 
>        some Nothing = Nothing
>        some (Just x) = Just (repeat x)
> 
>        many Nothing = Just []
>        many (Just x) = Just (repeat x)
> 
> That is a really good idea!  In fact, this behavior was exactly what my
> intuition had at first suggested to me that these methods should do.
> 
> But the part that still confuses me is:  why are these not considered the
> "least" solutions of the equations?

It has to do with the termination partial ordering -- the least solutions
give a denotational description that's equivalent to what recursion computes.

In this case, the least solutions are

	some Nothing = Nothing
	some (Just x) = _|_

	many Nothing = Just []
	many (Just x) = _|_

It's easy to verify that these are solutions, and that they're less
defined than the versions above.