
On 12/31/11 8:18 AM, Yves Parès wrote:
Thanks for the explanation on free monads, it's interesting.
But still, I maintain my previous view. I could clarify that by saying that (e.g. for Maybe) we could separate it in two types, Maybe itself and its monad:
-- The plain Maybe type data Maybe a = Just a | Nothing
-- The MaybeMonad newtype MaybeMonad a = MM ( () -> Maybe a )
That's what using Maybe as a monad semantically means, doesn't it?
Well, to take the category-theoretic perspective, a "value" or "element" of X is simply defined to be any morphism from the terminal object into X. Thus, saying "x \in X" or "x :: X" is just another way to say x : 1 -> X. The unit type isn't quite terminal because it has two values, but it's close enough to get the idea. If unit truly had only one value, then ()->Y is at least (isomorphic to) a subobject of Y, and almost surely isomorphic to (all of) Y. All of this is just by the definition of what a terminal object is; nothing about monads anywhere. Also note that (X ->) forms a monad for any X. But that's a separate issue. -- Live well, ~wren