#StackBounty: #lambda-calculus #type-theory #category-theory (Co)-monads and terminating implementations

Bounty: 50

The bounty above should read ‘I would like to know whether the example I discuss is a com-monad and why (why not).’

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):

  1. Co-unit $;;;; mathbb{M} alpha to alpha$
  2. 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?

Get this bounty!!!

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.