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

#StackBounty: #reference-request #pl.programming-languages #type-theory #lambda-calculus #dependent-type Hereditary Substitution with I…

Bounty: 50

I’m wondering, is there any existing work on hereditary substitution with inductive type families and dependent eliminators?

In particular, normalizing the application of an eliminator to an inductive value “obviously” halts, since the head of the elimination is structurally smaller each time.

But, I’m wondering, how does it fit into the structurally-shrinking argument of hereditary substitution? For example, in Harper and Licata’s presentation, hereditary substitution is always strictly decreasing, structurally in the value being substituted into, or in the shape of the type of the variable being replaced.

But, if we have:

$natElim: (m : Nat to Set) to m 0 to (k : Nat to m k to m (succ k) ) to (k : Nat) to m k$

and we are computing $[1/x](natElim m z (lambda k pldotp t_1) x)$, we must compute:

  • $[0/x](natElim m z s x) = t_2$,
  • $[0/k]t_2 = t_3$
  • $[t_2/p]t_3 =t_4$
    to get a result of $t_4$.

But these are not decreasing in either the type of $x$ or the term being substituted into. The first two are decreasing in the value replacing the variable, but the third is not.

Is their prior work on this? I can think of ad-hoc ways to make the decreasing size argument work for Nat, Vec, etc. But is there a general argument for inductive types?

This is possibly related to my previous question question: I’m not sure if this falls under the “large eliminators” described there. If this only works for “small eliminators”, I’m still interested in a reference for this.

Get this bounty!!!