3
$\begingroup$

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?

Improve this question
$\endgroup$
18
  • $\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$
    – Musa Al-hassy
    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$
    – Musa Al-hassy
    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

0

Reset to default

Your Answer

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