wren ng thornton wren at freegeek.org
Mon Jan 9 11:16:03 CET 2012

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
>
> -- The plain Maybe type
> data Maybe a = Just a | Nothing
>
> 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