Mark Snyder muddsnyder at yahoo.com
Mon Apr 12 16:27:31 EDT 2010

```>From: Conor McBride <conor at strictlypositive.org>
>Sent: Mon, April 12, 2010 5:34:05 AM
>
>Hi
>
>(Redirecting to cafe, for general chat.)
>
>On 12 Apr 2010, at 01:39, Mark Snyder wrote:
>
> Hello,
>>
>>     I'm wondering what the correct terminology is for the extra functions that we define with monads.  For instance, >State has get and put, Reader has ask and local, etc.  Is there a good name for these?
>
>Yes. Indeed, quite a lot of energy has been expended on the matter.
>It's worth checking out work by Plotkin and others on "Algebraic
>like Dan Piponi and Heinrich Apfelmus).
>

Thanks!  I wasn't aware of that work.  It certainly does split things up nicely, I hadn't really thought of looking at them as two distinct groups of functionality.  It also clears things up in my mind to look at them as the maximum-arity functions and seeing whether any arguments are computations, or whether the function just constructs a computation.
>This work distinguishes two kinds of "extra function": operations
>(e.g. get, put, ask, throwError, etc) and control operators (local,
>catchError, etc).
>
>*Operations* have types like
>
>  s1 -> ... sn -> M t
>
>where the s's and t are thought of as "value" types, and M is yer
>monad. You can think of M as describing an "impure capability",
>permitting impure functions on values. You might even imagine
>specifying M's collection of operations by a signature, with this
>
>  sig M where
>    f s1 ... sn :: t
>
>Note that I'm careful to mark with :: where the inputs stop and
>the outputs start, as higher-order functions make this ambiguous.
>
>For example
>
>  sig State s where
>    get :: s
>    put s :: ()
>
>
>  sig Maybe where
>    throw :: a
>
>Many popular monads can be characterized exactly by the signature
>of their operations and the equational theory those operations
>must obey (e.g. laws like  put s >> get >>= f == put s >> f s).
>The point of these monads is to deliver the capability specified
>by the operations and equations. The similiarity between the
>signatures above and the typeclasses often declared to support
>
>Note that every (set of) signature(s) induces a datatype of
>command-response trees whose nodes are labelled with a choice
>of operation and inputs, whose edges are labelled with outputs,
>and whose leaves carry return values. Such a tree represents
>a "client strategy" for interacting with a server which offers the
>capability, at each step selecting an operation to perform and
>explaining how to continue as a function of the value returned.
>The equational theory of the operations induces an equivalence
>on strategies. Command-response trees up to operational
>equivalence give the most general implementation of the specified
>monad: return makes leaves, >>= pastes trees together, and each
>operation creates a node. The monad comes from its operations!
>
>But what of local, catchError, and other such things? These are
>*control operators*, and they operate on "computations", with
>types often involving resembling
>
>   a -> (b -> M c) -> M d
>
>Typically, the job of a control operator is to make local changes
>to the meaning of the operations in M's signature. A case in
>point is "local", whose job is to change the meaning of "ask".
>Similarly, catchError can be thought of as offering a local
>exception.
>
>Old LISPheads (like me!) might think of operations as EXPRs and
>control operators as FEXPRs. Haskell does a neat job of hiding
>the distinction between the two, but it may be conceptually
>helpful to dig it out a bit. Control operators don't give
>rise to nodes in command-response trees; rather, they act as
>tree transformers, building new strategies from old.
>
>I could start a pantomime about why operations are heroes and
>control operators are villains, but I won't. But I will suggest
>that characterising monads in terms of the operations and/or
>control operators they support is a useful (and increasingly
>modular) way to manage effects in programming. After all,
>most end-user applications effectively equip a bunch of
>user-operations with a semantics in terms of system-operations.
>
>All the best
>
>Conor

So in this line of thought, where we have the operations and the control operators, I guess my original question wasn't aware of the distinction, and was looking for a name for all of them combined.  In Haskell (specifically in the mtl), we see them lumped together into the typeclass.  If we are talking about an implementation, is it good practice to try and use the most theoretically correct language, even if an implementation diverges somewhat while getting things done?  I.e., should they be referred to as the operations and control operators, or more simply as the "type-class-provided functions"?  I like the idea of trying to use more formal names, but I don't want to be implying that an implementation is an exact representation of the underlying concept.   For instance, the functional dependency in the mtl library is seen as an implementation choice, and I think some people prefer versions without the dependency.  In what sense is it fair to say that
Control.Monad.State _is_ a monad, as opposed to saying that it _represents_ a monad?  Maybe it  just suffices to say the (e.g. MonadState) typeclass represents the operations and control operators.

Thanks for shining a light on the question!

~Mark

-------------- next part --------------
An HTML attachment was scrubbed...