Re: Where does the term monad come from?

[Thorsten Altenkirch <txa@Cs.Nott.AC.UK>]

Hi Steve,

thank you for addressing the other part of my question.

> There was also a second part to the question:
>
>>
>> Btw, I frequently encounter monads in a categories of functors which
>> are not endofunctors. An example are finite dimensional vectorspaces
>> which can be constructed via a monoid in the category of functors
>> FinSet -> Set, here I is the embedding and (x) can be constructed
>> from
>> the left kan extension and composition.
>> The unit is given by the Kronecker delta and join can be constructed
>> from Matrix multiplication. Should one call these beasts monads as
>> well? Is there a good reference for this type of construction?
>
> The category of functors from FinSet to Set is equivalent to the
> category
> of endofunctors of Set which preserve filtered colimits: such
> endofunctors
> are usually called finitary. Thus a monoid in [FinSet,Set] with
> respect to
> this tensor product is the same thing as a monad on Set whose
> endofunctor
> part is finitary: this is called a finitary monad.
>
> These finitary monads on Set are equivalent to Lawvere theories and
> so in
> turn to (finitary, single-sorted) varieties.
>
> Finitary monads can also be considered on other base categories than
> Set,
> especially on locally finitely presentable ones.
>
> It is true that vector spaces are the algebras for a finitary monad
> on Set.
> There is no need to restrict to finite-dimensional vector spaces; in
> fact it
> is not true that there is a monad on Set whose algebras are the
> finite-dimensional vector spaces.

I am not sure I completely understand your comments. I guess it may be
helpful to be more precise:

F : FinSet -> Set
F A = Real -> A

together with:

>

eta_A : A -> F A
eta a = \ b . if a=b then 1 else 0

(>>=) : F A -> (A -> F B) -> F B
v >>= f = \ b. \Sigma a:A.(v a)*(f a b)

My notation is inspired by functional programming and naturally as a
Computer Scientist I am interested in the constructive content of
theorems. This construction only works if the input is decidable
(needed for eta) and if we can define Sigma (this certainly works if A
is finite).

I can see how to lift F to a functor on Sets by using a Kan extension
(left ?). In my terminology it may be something like

F' : Set -> Set
F' X = Sigma A:FinSet. A -> X x F A

I suspect my eta and >>= give then rise to a monad on Set? However, I
don't see how to do this if the vector spaces are not finite.

Btw, I only used this as an example. My question was rather wether
people have studied monoids in categories of functors which are not
endofunctors. I believe this notion is useful in functional
programming and Type Theory as a natural generalisation of the notion
of a monad.

Cheers,
Thorsten


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.