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?

  • $\begingroup$ For any $r$ and $\alpha$, try writing down a term in Haskell/STLC of the type $(r \to \alpha) \to \alpha$. Such a term takes in a function $f : r \to \alpha$ and somehow produces a value of $\alpha$, but if you know nothing of this type you cannot produce a value of it (unless you cheat and use Haskell's undefined); likewise, you know nothing about $r$ and so cannot apply $f$ to obtain a value of $\alpha$. Hope this helps ^_^ $\endgroup$ Aug 13, 2020 at 13:06
  • $\begingroup$ @Musa Al-hassy But in the STLC you can form a term of type $(r \to \alpha) \to \alpha$. For example, $\lambda P_{r\to \alpha}. P\,j_{r}$. There is no problem with such a term in the STLC; in fact, Montague used terms of this type to interpret proper names. $\endgroup$
    – user65526
    Aug 13, 2020 at 13:10
  • $\begingroup$ What is your $j_\alpha$, is it a value of type $\alpha$? What if $\alpha$ is the empty set, then it is no longer empty. $\endgroup$ Aug 13, 2020 at 13:11
  • $\begingroup$ In a STLC with an infinite stock of variables and constants of all types, you can always form a term of type $\lambda P_{r\to \alpha}.\, P\, j_{r}$. $\endgroup$
    – user65526
    Aug 13, 2020 at 13:13
  • 1
    $\begingroup$ @Musa Al-hassy This was the original semantics for the STLC, and is explained here by Henkin: jstor.org/stable/2266967?seq=3#metadata_info_tab_contents $\endgroup$
    – user65526
    Aug 13, 2020 at 13:26


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.