Suppose we set $ \mathbb{M} \alpha := r \to \alpha$ , where $ r$ is some fixed type, and $ \alpha$ an arbitrary type, of the STLC (Simply-Typed Lambda Calculus)
Suppose we want to define a co-monad, which contains Co-unit and Co-join, with the following types (where $ \mathbb{M}$ binds more tightly than $ \to$ and $ \mathbb{M}$ is as stated above):
- Co-unit $ \;\;\;\; \mathbb{M} \alpha \to \alpha$
- Co-join $ \;\;\;\;\mathbb{M}\mathbb{M} \alpha \to \mathbb{M} \alpha$
I have been told that this will not work and that we could not create a co-monad in this way, since there is no terminating implementation for the type $ (e \to a) \to a$ .
But in the pure STLC all terms are "terminating"(i.e, reductions always lead to a (unique) normal form). So I don’t understand how this comment can be relevant in the case of the STLC.
Is there some link between (co)-monads and terminating implementations? Or is this just about creating a co-monad in Haskell?
Why would we not be able to construct a co-monad in the way described above?
