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.