<p>My personal favorite core language is intensional Martin-Löf type theory with exactly 8 type formers: You have your basic finite types <span class="math-container">$0$</span>, <span class="math-container">$1$</span>, and <span class="math-container">$2$</span>, your quantifiers <span class="math-container">$\Pi$</span> and <span class="math-container">$\Sigma$</span>, and also the <span class="math-container">$W$</span> type (which you may note has the same form as a quantifier). Then you have the <code>Id</code> type of equalities and last but not least, you have a countably infinite cumulative hierarchy of universes <span class="math-container">$U_n$</span> closed under the other type formers.</p>
<p>The negative types <span class="math-container">$1$</span>, <span class="math-container">$\Pi$</span>, and <span class="math-container">$\Sigma$</span> have <span class="math-container">$\eta$</span>-rules: <span class="math-container">$x = \star : 1$</span> and <span class="math-container">$f = \lambda x.f\, x: \Pi_{x:A}B[x]$</span> and <span class="math-container">$p = (p_1, p_2) : \Sigma_{x:A}B[x]$</span>. The empty type <span class="math-container">$0$</span> has only the non-dependent eliminator <span class="math-container">$!_Dx$</span> (the dependent eliminator is definable as <span class="math-container">$!_{
D[x]}x$</span>). The <code>Id</code> type has an eliminator <code>J</code> that computes on <code>refl</code>. And that is all you need to do nearly everything that Coq can do, which is sufficiently expressive for me.</p>
<p>This is sufficient to construct general inductive types (including the natural numbers) with all the expected behavior by an argument given in <a href="https://doi.org/10.4230/LIPIcs.TYPES.2020.8" rel="nofollow noreferrer">Why not W?</a> (I am the author of this paper).</p>
<p>You technically don't even need <span class="math-container">$0$</span>, since without any extra rules on the behavior of <span class="math-container">$0$</span> you can define <span class="math-container">$0 = W_{x:1}1$</span>, which supports elimination into arbitrary types.
Alternatively, you can define <span class="math-container">$0 = \text{Id}_2\,\text{true}\,\text{false}$</span>, and eliminate into any <span class="math-container">$A:U_n$</span> (and as long as you have an infinite universe hierarchy, every type is in some universe).</p>
<p>I said cumulative hierarchy of universes, but I usually think of it as there being a <code>Lift</code> operator that strictly commutes with type and term formers. When you erase the <code>Lift</code> operator, this looks like cumulativity, and it should be relatively easily to infer where to add <code>Lift</code> back in.</p>
<p>This is a subset of the theory implemented by Agda, and Coq is only missing <span class="math-container">$\eta$</span> for <span class="math-container">$1$</span>. Thus prior work should show that the system is consistent and type-checking is decidable.</p>
<h2>Extensions</h2>
<p>You can of course add in axiom K or equality reflection if you are uninterested in Homotopy Type Theory.</p>
<p>As Coq and Agda have done recently, you can add in a universe of strict propositions.</p>
<p>You can probably add an impredicative universe (Prop in Coq), but I'm not sure of the consequences.</p>
<p>You can cut off the universe hierarchy at a finite point if you don't need all the universes. In that case the collection of all types is not closed under binary sums, because they are defined in this system via large elimination from <span class="math-container">$2$</span> into <span class="math-container">$U_n$</span>, and you can't use <a href="https://personal.cis.strath.ac.uk/conor.mcbride/pub/SmallIR/SmallIR.pdf" rel="nofollow noreferrer">small induction-recursion</a> to define types with a function into the largest universe. (caveat: I haven't proven impossibility, but don't know how to construct such types.) Generalizing <span class="math-container">$W$</span> types to include a <a href="https://coq.inria.fr/doc/V8.15.2/refman/language/core/inductive.html#parameterized-inductive-types" rel="nofollow noreferrer">large, non-uniform parameter</a> eases some of these difficulties, and also increases the expressiveness with an infinite universe hierarchy.</p>
<p>It is fun to think about some extra rules for the empty type <span class="math-container">$0$</span>, but I have not found a case where these are necessary. To start with, we can take <span class="math-container">$x = y : 0$</span>. Now there are a bunch of rules that propagate a proof of false. For the negative types these look like <span class="math-container">$!_{\Pi_{a:A}B[a]}x\,a = !_{B[a]}x$</span> and <span class="math-container">$(!_{\Sigma_{a:A}B[a]}x)_1 = !_Ax$</span> and <span class="math-container">$(!_{\Sigma_{a:A}B[a]}x)_2 = !_{B[!_Ax]}x$</span>, while for the positive types <span class="math-container">$2$</span>, <span class="math-container">$W$</span>, and <code>Id</code> these just say that eliminating <span class="math-container">$!_2x$</span> with a motive of <span class="math-container">$D[y]$</span> produces <span class="math-container">$!_{D[!_2x]}x$</span>. These extra rules may complicate conversion, but they look kind of neat. Can probably take <span class="math-container">$!_{U_n}x = 0$</span>.</p>
<h2>Limitations</h2>
<p>The system does not support expressing large induction-recursion, inductive-inductive types (probably), higher inductive types, nested inductive types (where the definition of an inductive type <span class="math-container">$A$</span> refers to say <span class="math-container">$\text{list}\,A$</span> in the constructors), or mutual inductive types where the different inductive types are in different sorts by going through an impredicative universe (Coq can do this, but I've seen no examples of it being useful).</p>
<p>The system does not include function extensionality or Univalence or quotient types.</p>
<p>The system probably does not include coinductive types that compute as expected up to judgmental equality. Adding as primitive coinductive <code>M</code> types with a large parameter gives pretty good expressivity.</p>
<h2>Coinduction</h2>
<p>To expand on the point about coinductive types above, <a href="https://hott.github.io/M-types/m-types.pdf" rel="nofollow noreferrer">Non-wellfounded trees in homotopy type theory</a> gives a construction of coinductive types assuming at least function extensionality, but the computation rules do not hold judgmentally. This can be refined to only use function extensionality to prove the computation rule. If you are working in a system where the <code>K</code> eliminator for <code>Id</code> types exists and computes on <code>refl</code>, then all your problems go away and coinductive types are broadly constructible.</p>
<p>Like inductive types, there are several ways to generalize coinductive types, but unlike inductive types I don't know how to reduce them down to simpler versions. The simplest is just M types (dual to W types), but I don't know how to construct indexed or parametrized coinductive types from these. Multiple destructors is probably not an issue. Since univalence implies funext, you might expect univalence also implies bisimulation is equality for coinductives, but this doesn't seem to hold without an extra assumption such as eta for coinductive types.</p>

CC BY-SA 4.0
2024-10-01T09:17:09.320Z
What's the problem with coinduction?
Martin Berger
CC BY-SA 4.0
2024-10-02T19:59:55.913Z
@MartinBerger too large for a comment, so I added a section with some of my thoughts on coinductive types
Jasper Hugunin
CC BY-SA 4.0
2024-09-30T00:02:26.023Z
2024-10-02T19:59:22.760Z
2024-10-02T19:59:22.760Z
Jasper Hugunin
<p>The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, though, has a few problems: induction isn't derivable, it isn't possible to prove <code>0 != 1</code>, and pattern matching on algebraic data structures take linear time. In order to solve those issues, practical languages such as Coq are based on the Calculus of Inductive Constructions instead, which add a layer of primitive datatypes on top of CoC. That, unfortunately, makes the core language very complex.</p>

<p>An alternative solution to those problems is a new primitive, <a href="https://fermat.github.io/document/papers/rta-tlca.pdf" rel="noreferrer">self</a>, which is a construction that allows a type to reference its typed term. This construct, together with the Parigot encoding, and a slightly weakened but still useful notion of contradiction, is sufficient to solve the problems above. The proposed language, though, is still somewhat complex. In particular, it has different Pi types, complex kind machinery and requires a restricted form of recursion (for the Parigot encoding).</p>

<p>Is it possible to be simpler? I.e., can the calculus of constructions with only self types and nothing else from this paper still be able to derive induction and employ the parigot encoding?                                                                                                                                      </p>

CC BY-SA 3.0
2017-05-01T14:18:26.310Z
I feel like I answered a similar question here: https://cs.stackexchange.com/questions/49638/do-self-types-make-the-calculus-of-inductive-constructions-obsolete/49959#49959. How is your current question different? Also, you seem to be asking 2 different questions in the title and the body.
cody
CC BY-SA 3.0
2017-05-01T16:27:35.847Z
@cody I am so sorry. I spent some time googling and looking up to make sure I wasn't asking a repeated question (as I was fairly sure I had discussed something similar here), but I missed your answer to that post specifically covered this. It has none of the keywords I googled for...
MaiaVictor
CC BY-SA 3.0
2017-05-01T21:32:29.313Z
No problem, and I actually vote for the question to stay open, since it may attract some interesting answers.
cody
CC BY-SA 3.0
2017-07-27T15:05:59.493Z
You may want to look at guarded recursion. For example http://www.itu.dk/people/mogel/papers/lics2017.pdf
xavierm02
CC BY-SA 4.0
2018-07-11T14:41:43.930Z
I'm interested int this subject too. Have you got answers to your questions? Your quote "adding a new primitive, self" is incomplete. The paper states that you need to add mutually recursive definitions too, which break the analogy of types-as-proofs... [Here is a newer work of same authors](https://fermat.github.io/document/papers/scott-dep.pdf). The quote I'm talking about is in the penultimate paragraph of the first page.
user3368561
<type-theory><lambda-calculus><functional-programming>
Are there simple core languages which are consistent and expressive?
MaiaVictor
# Are there simple core languages which are consistent and expressive?

(Asked by: username_0 on 2017-04-28)

The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, though, has a few problems: induction isn't derivable, it isn't possible to prove `0 != 1`, and pattern matching on algebraic data structures take linear time. In order to solve those issues, practical languages such as Coq are based on the Calculus of Inductive Constructions instead, which add a layer of primitive datatypes on top of CoC. That, unfortunately, makes the core language very complex.

An alternative solution to those problems is a new primitive, [self](https://fermat.github.io/document/papers/rta-tlca.pdf), which is a construction that allows a type to reference its typed term. This construct, together with the Parigot encoding, and a slightly weakened but still useful notion of contradiction, is sufficient to solve the problems above. The proposed language, though, is still somewhat complex. In particular, it has different Pi types, complex kind machinery and requires a restricted form of recursion (for the Parigot encoding).

Is it possible to be simpler? I.e., can the calculus of constructions with only self types and nothing else from this paper still be able to derive induction and employ the parigot encoding?

**Tags:** type-theory, lambda-calculus, functional-programming

> **Comments:**
> **username_1**: I feel like I answered a similar question here: https://cs.stackexchange.com/questions/49638/do-self-types-make-the-calculus-of-inductive-constructions-obsolete/49959#49959. How is your current question different? Also, you seem to be asking 2 different questions in the title and the body.  
> **username_0**: @username_1 I am so sorry. I spent some time googling and looking up to make sure I wasn't asking a repeated question (as I was fairly sure I had discussed something similar here), but I missed your answer to that post specifically covered this. It has none of the keywords I googled for...  
> **username_1**: No problem, and I actually vote for the question to stay open, since it may attract some interesting answers.  
> **username_2**: You may want to look at guarded recursion. For example http://www.itu.dk/people/mogel/papers/lics2017.pdf  
> **username_3**: I'm interested int this subject too. Have you got answers to your questions? Your quote "adding a new primitive, self" is incomplete. The paper states that you need to add mutually recursive definitions too, which break the analogy of types-as-proofs... [Here is a newer work of same authors](https://fermat.github.io/document/papers/scott-dep.pdf). The quote I'm talking about is in the penultimate paragraph of the first page.  

---

## 1 answers

### Answer by username_4 on 2024-09-30. Score: 6

My personal favorite core language is intensional Martin-Löf type theory with exactly 8 type formers: You have your basic finite types $0$, $1$, and $2$, your quantifiers $\Pi$ and $\Sigma$, and also the $W$ type (which you may note has the same form as a quantifier). Then you have the `Id` type of equalities and last but not least, you have a countably infinite cumulative hierarchy of universes $U\_n$ closed under the other type formers.

The negative types $1$, $\Pi$, and $\Sigma$ have $\eta$-rules: $x = \star : 1$ and $f = \lambda x.f\, x: \Pi\_{x:A}B[x]$ and $p = (p\_1, p\_2) : \Sigma\_{x:A}B[x]$. The empty type $0$ has only the non-dependent eliminator $!\_Dx$ (the dependent eliminator is definable as $!\_{
D[x]}x$). The `Id` type has an eliminator `J` that computes on `refl`. And that is all you need to do nearly everything that Coq can do, which is sufficiently expressive for me.

This is sufficient to construct general inductive types (including the natural numbers) with all the expected behavior by an argument given in [Why not W?](https://doi.org/10.4230/LIPIcs.TYPES.2020.8) (I am the author of this paper).

You technically don't even need $0$, since without any extra rules on the behavior of $0$ you can define $0 = W\_{x:1}1$, which supports elimination into arbitrary types.
Alternatively, you can define $0 = \text{Id}\_2\,\text{true}\,\text{false}$, and eliminate into any $A:U\_n$ (and as long as you have an infinite universe hierarchy, every type is in some universe).

I said cumulative hierarchy of universes, but I usually think of it as there being a `Lift` operator that strictly commutes with type and term formers. When you erase the `Lift` operator, this looks like cumulativity, and it should be relatively easily to infer where to add `Lift` back in.

This is a subset of the theory implemented by Agda, and Coq is only missing $\eta$ for $1$. Thus prior work should show that the system is consistent and type-checking is decidable.

## Extensions

You can of course add in axiom K or equality reflection if you are uninterested in Homotopy Type Theory.

As Coq and Agda have done recently, you can add in a universe of strict propositions.

You can probably add an impredicative universe (Prop in Coq), but I'm not sure of the consequences.

You can cut off the universe hierarchy at a finite point if you don't need all the universes. In that case the collection of all types is not closed under binary sums, because they are defined in this system via large elimination from $2$ into $U\_n$, and you can't use [small induction-recursion](https://personal.cis.strath.ac.uk/conor.mcbride/pub/SmallIR/SmallIR.pdf) to define types with a function into the largest universe. (caveat: I haven't proven impossibility, but don't know how to construct such types.) Generalizing $W$ types to include a [large, non-uniform parameter](https://coq.inria.fr/doc/V8.15.2/refman/language/core/inductive.html#parameterized-inductive-types) eases some of these difficulties, and also increases the expressiveness with an infinite universe hierarchy.

It is fun to think about some extra rules for the empty type $0$, but I have not found a case where these are necessary. To start with, we can take $x = y : 0$. Now there are a bunch of rules that propagate a proof of false. For the negative types these look like $!\_{\Pi\_{a:A}B[a]}x\,a = !\_{B[a]}x$ and $(!\_{\Sigma\_{a:A}B[a]}x)\_1 = !\_Ax$ and $(!\_{\Sigma\_{a:A}B[a]}x)\_2 = !\_{B[!\_Ax]}x$, while for the positive types $2$, $W$, and `Id` these just say that eliminating $!\_2x$ with a motive of $D[y]$ produces $!\_{D[!\_2x]}x$. These extra rules may complicate conversion, but they look kind of neat. Can probably take $!\_{U\_n}x = 0$.

## Limitations

The system does not support expressing large induction-recursion, inductive-inductive types (probably), higher inductive types, nested inductive types (where the definition of an inductive type $A$ refers to say $\text{list}\,A$ in the constructors), or mutual inductive types where the different inductive types are in different sorts by going through an impredicative universe (Coq can do this, but I've seen no examples of it being useful).

The system does not include function extensionality or Univalence or quotient types.

The system probably does not include coinductive types that compute as expected up to judgmental equality. Adding as primitive coinductive `M` types with a large parameter gives pretty good expressivity.

## Coinduction

To expand on the point about coinductive types above, [Non-wellfounded trees in homotopy type theory](https://hott.github.io/M-types/m-types.pdf) gives a construction of coinductive types assuming at least function extensionality, but the computation rules do not hold judgmentally. This can be refined to only use function extensionality to prove the computation rule. If you are working in a system where the `K` eliminator for `Id` types exists and computes on `refl`, then all your problems go away and coinductive types are broadly constructible.

Like inductive types, there are several ways to generalize coinductive types, but unlike inductive types I don't know how to reduce them down to simpler versions. The simplest is just M types (dual to W types), but I don't know how to construct indexed or parametrized coinductive types from these. Multiple destructors is probably not an issue. Since univalence implies funext, you might expect univalence also implies bisimulation is equality for coinductives, but this doesn't seem to hold without an extra assumption such as eta for coinductive types.

> **Comments:**
> **username_5**: What's the problem with coinduction?  
> **username_4**: @MartinBerger too large for a comment, so I added a section with some of my thoughts on coinductive types  

---

