#StackBounty: #lambda-calculus #category-theory What's the internal language of the opposite of a Cartesian closed category?

Bounty: 100

I have heard the simply typed lambda calculus is the internal language of Cartesian closed categories.

What’s the internal language of the opposite type of category?

The rules dual to currying and uncurrying are:

mathrm{mal} : mathrm{Hom}(b, a + c) to mathrm{Hom}(b vdash a, c) \
mathrm{try} : mathrm{Hom}(b vdash a, c) to mathrm{Hom}(b, a + c) $$

I have the intuition the opposite category would correspond to continuation passing style or pattern matching but the opposite typing rules seem very strange and hard to figure out.

Trivially one could interpret/compile the simply typed lambda calculus in reverse but that would be extraordinarily confusing.

I have found with a little bit of finagling we can get rules that resemble continuation passing style.

mathrm{kont} : mathrm{Hom}(x, b) to mathrm{Hom}(c, mathrm{0}) to mathrm{Hom}(x, b vdash c) \
mathrm{kont} , x , k = [mathrm{absurd} circ k , mathrm{id}] circ mathrm{try} , mathrm{id} circ x

mathrm{jump} : mathrm{Hom}(x, b vdash a) to mathrm{Hom}(b, a) to mathrm{Hom}(x, mathrm{0}) \ mathrm{jump} , k , x = mathrm{mal} , ( mathrm{i}_1 circ x ) circ k $$

$$ mathrm{env} : mathrm{Hom}(x, b vdash a) to mathrm{Hom}(x, b) \ mathrm{env} , k = mathrm{mal} , mathrm{i}_2 circ k$$

These are still pretty hard to figure out an interpretation for though.

Get this bounty!!!

#StackBounty: #type-theory #lambda-calculus #functional-programming #category-theory Creating a large tuple from smaller tuples via a m…

Bounty: 50

Suppose I have a term $a :alpha$ of the Simply-Typed Lambda Calculus (in the following, $alpha, beta, gamma$ stand for arbitrary types) and I want to lift it to a term

$lambda x_{beta}. ;(x, , a)$

I could use a function $lambda z_{alpha}, x. ;(x,, z)$.

Suppose we then form $(b, a) : beta times alpha$, by applying $lambda x_{beta}. ;(x, , a)$ to $,b_{beta}$.

We might want to add $c$ to the beginning of this to form $(c, b, a) : gamma times beta times alpha$. We could do this (here $pi_1$ and $pi_2$ are projections)) by having a function $lambda z’_{beta times alpha}, z. ,(z,, pi_1 z’,, pi_2 z’)$. And again, we could cook up a function to form $(d,, c,, b,, a)$ and $(e,,d,, c,, b,, a)$ (so on and so forth).

I could do things in the way above; however, I wondered whether there was a way of doing this kind of operation via an applicative or a monad. Then I could (ideally) use the operations of the monad or applicative, to lift term $a$ (perhaps into $lambda x.,(x, , a)$, and then form these tuples $(b, a), (c, b, a), (d, c, b, a)$, etc, by the operations of the monad or applicative.

If you know a way of doing this I would be very interested.

Get this bounty!!!

#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!!!