<p>I have not seen this in a dependently-typed setting, but a similar notion <em>is</em> fairly well-known in weaker systems (e.g. System F) with subtyping, under the term "F-bounded quantification". This pops up prominently in type systems for object-oriented programming languages, which typically are heavy on (equi-) type recursion. This notion was originally introduced by <a href="https://dl.acm.org/citation.cfm?id=99392" rel="noreferrer">this paper</a>.</p>

<p>A standard use case is expressing forms of "binary methods" that need to be covariant in their argument types. For example, in those languages you see interface types like</p>

<pre><code>interface Ordered&lt;T&gt; { less(x : T) : Bool }
</code></pre>

<p>with subtypes like</p>

<pre><code>class Int extends Ordered&lt;Int&gt; { ... }
</code></pre>

<p>and usage patterns</p>

<pre><code>class Queue&lt;T extends Ordered&lt;T&gt;&gt; { ... }
</code></pre>

<p>or</p>

<pre><code>sort&lt;T extends Ordered&lt;T&gt;&gt;(array : Array&lt;T&gt;) : Array&lt;T&gt;
</code></pre>

<p>and so on. In the more type-theoretical rendering of System F-sub with F-bounded quantification and records these could be expressed as</p>

<pre><code>Ordered = λ(T &lt;: Top). {less : T → Bool}
Int &lt;: Ordered(Int)
Queue = λ(T &lt;: Ordered(T)). {...}
sort : ∀(T &lt;: Ordered(T)). Array(T) → Array(T)
</code></pre>

CC BY-SA 4.0
2018-09-28T15:56:51.817Z
I was almost regretting having asked that question, thanks a lot for those resources.
MaiaVictor
CC BY-SA 4.0
2018-09-29T20:35:59.313Z
Thanks for the answer. I'd just like to observe that the examples mentioned by @AndreasRossberg all come from programming langauges with general recursion. I thought one of the important facets of the question was whether we can have this sort of recursion without inhabiting every type.
Andrej Bauer
CC BY-SA 4.0
2018-09-29T22:44:19.453Z
@AndrejBauer, yes, good point. This kind of recursive binding hardly makes sense in the absence of general recursive types. And those immediately enable expressing general recursion on the term level.
Andreas Rossberg
CC BY-SA 4.0
2019-02-13T18:18:03.367Z
@AndreasRossberg Wang and Rompf encode F-bounds in a strongly normalizing subset of DOT, where variables are bound in their own type: https://www.cs.purdue.edu/homes/rompf/papers/wang-ecoop17.pdf. Function types stick to usual scoping but I expect they could be changed.
Blaisorblade
CC BY-SA 4.0
2019-02-13T18:27:34.360Z
Beware that mu-types in that paper are not quite recursive types. Dreyer suggested to me they resemble recursively-defined signatures (“What is a recursive module?”, PLDI’99). And somebody (IIRC Sandro Stucki?) pointed out they resemble Fu and Stump’s \iota-types (in their 2014 version, which differs from modern Cedille: http://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf).
Blaisorblade
CC BY-SA 4.0
2018-09-28T10:47:34.067Z
2018-09-28T11:33:23.453Z
2018-09-28T11:33:23.453Z
Andreas Rossberg
<p>Your question is somewhat related to some work I did (sorry for the self-advertisement), where I encode some weak form of dependent type into a Curry-style language (kind of an extension of System F). The idea is to encode the dependent function type <span class="math-container">$\forall x{\in}A \Rightarrow B$</span> as <span class="math-container">$\forall x (x{\in}A \Rightarrow B)$</span>. This encoding relies on first-order quantification and on a specific membership type <span class="math-container">$t{\in}A$</span>, which intuitively corresponds to the singleton type <span class="math-container">$\{t\}$</span> when <span class="math-container">$t$</span> is in <span class="math-container">$A$</span>, and it is empty otherwise. Otherwise said, this type quantifies on every possible term of the language, but terms with the wrong type are filtered out by membership (this is related to the relativized quantification scheme, which is used a lot in (classical) realizability settings).</p>

<p>So how does this relate to your question? In my setting, you can get in a situation where you (kind of, but not really as explained further) have a judgement of the form <span class="math-container">$Γ, x : x{\in}A \vdash t : B$</span> (or more generally <span class="math-container">$Γ, x : u{\in}A \vdash t : B$</span>), and the following rule is used to destruct membership types in the context.
<span class="math-container">$$
  \frac{\Gamma, x : A, x \equiv u \vdash t : B}
       {\Gamma, x : u{\in}A \vdash t : B}
$$</span></p>

<p>To go back to the encoding of dependent function types, being slightly more precise (things are subtle), you can get typing derivations of the following form.
<span class="math-container">$$
  \dfrac{
  \dfrac{
  \dfrac{\Gamma, x : A, x \equiv y \vdash t : B}{\Gamma, x : y{\in}A \vdash t : B}}
    {\Gamma \vdash \lambda x.t : y{\in}A \Rightarrow B} \hspace{1cm} y \notin \Gamma}
       {\Gamma \vdash \lambda x.t : \forall y (y{\in}A \Rightarrow B)}
$$</span>
One thing to note is that we actually have two different variables: one bound by the <span class="math-container">$\lambda$</span>-abstraction, and another one bound by the first-order quantifier. However, we known that they are equal (<span class="math-container">$x \equiv y$</span> is in the context). Using a substitution rule and some weakening you can actually go a bit further and get an hypothesis of the form <span class="math-container">$\Gamma, x : A \vdash t : B[y := x]$</span>.</p>

<p>Sorry for the rough answer, I don't have time to do better right now. If you want to know more, check out <a href="https://doi.org/10.1007/978-3-662-49498-1_19" rel="nofollow noreferrer">this paper</a> or <a href="https://tel.archives-ouvertes.fr/tel-01682908" rel="nofollow noreferrer">my thesis</a>.</p>

CC BY-SA 4.0
2018-09-30T18:27:39.097Z
2018-09-30T18:27:39.097Z
Rodolphe Lepigre
<p>It is rather unusual for the <em>type</em> of <code>x</code> to be allowed to refer to <code>x</code>.</p>

<p>Your proposed typing rules are problematic when they say <code>Γ,x:A ⊢ A:∗</code> because that relies on a different notion of environment than usual: normally the type of a new element <code>x</code> (i.e. <code>A</code> here) must be closed over the prefix (i.e. <code>Γ</code> here), whereas in your case <code>A</code> can have <code>x</code> as free variable.</p>

<p>[ You say it "is possible, because we know the value of A" but I fail to see what you mean by that.  ]</p>

<p>In any case, the usual way to circumvent this is to do as Rodolphe suggests, i.e. split the introduction of <code>x</code> into two steps: <code>∀x:T. ∀_:P(x). e</code>.  You can think of System F-sub in the same way: <code>∀(T &lt;: Ordered(T)). e</code> becomes <code>∀(T:*). ∀(P : (T &lt;: Ordered(T))). e</code>.</p>

<p>Within the context of type-theory, the "tightest" form of recursion I know is that allowed by induction-recursion and induction-induction, with which you're probably familiar since your sample code is in Agda.</p>

<p>One last thing: I'm not sure exactly what you mean by <code>n : Nat n</code> in your sample code, but it sounds very much like a singleton type, so maybe you can break the recursion using singleton types and rewrite your code as: <code>∀(n : Nat). ∀(sn : SNat n). ...</code>.</p>

CC BY-SA 4.0
2018-10-01T14:04:28.953Z
2018-10-01T14:04:28.953Z
Stefan
<p>Usually, in Pure Type Systems, the type of a <code>λ/∀</code>-bound variable is only accessible on its body. That is, on <code>λ (X : A) -&gt; B</code>, <code>X</code> is free inside <code>A</code> and bound in <code>B</code>. But what if <code>X</code> was also bound in <code>A</code>? The typing rules should be updated accordingly, i.e., instead of:</p>

<p><span class="math-container">$$ \frac{Γ \vdash A : * \quad Γ, x : A \vdash B : *}{Γ \vdash ∀ (x : A) \rightarrow B : *}$$</span>
<span class="math-container">$$ \frac{Γ \vdash f : ∀ (x : A) \rightarrow B \quad Γ \vdash a : A}{Γ \vdash f a : [a/x]B}$$</span></p>

<p>we'd have:</p>

<p><span class="math-container">$$ \frac{Γ, x : A \vdash A : * \quad Γ, x : A \vdash B : *}{Γ \vdash ∀ (x : A) \rightarrow B : *}$$</span>
<span class="math-container">$$ \frac{Γ \vdash f : ∀ (x : A) \rightarrow B \quad Γ \vdash a : [a/x]A}{Γ \vdash f a : [a/x]B}$$</span></p>

<p>In other words, on the <code>∀ (x : A) -&gt; B</code> case, in order to infer the type of <code>A</code>, we extend the context with <code>x : A</code>, which is possible, because we know the <strong>value</strong> of <code>A</code>. On the application case <code>f a</code> with <code>f : ∀ (x : A) -&gt; B</code>, we substitute <code>x</code> by <code>a</code> in <code>A</code> before checking for equality. I have never seen such an approach, though. <strong>My question is: was this explored before? If so, is there a name for it so I can look up? If not, is there an obvious reason for it to be undesirable?</strong></p>

<p><em>(The reason I initially asked this question is I've <a href="https://cstheory.stackexchange.com/questions/39921/is-it-possible-to-derive-induction-by-extending-coc-with-recursion">previously asked</a> if it is possible to implement a halting definition of <code>ind</code> on the calculus of constructions with equi-recursion. I've noticed one can do so in a setting with mutually recursive definitions, as long as we also allow a λ/∀-bound variable to refer to itself on its type. <a href="https://gist.github.com/MaiaVictor/5d3385b7c117e29c006cae398a32a880" rel="nofollow noreferrer">Here is an example</a>.)</em></p>

CC BY-SA 4.0
2018-09-27T10:12:09.383Z
I personally feel very unmotivated to keep answering a series of questions "I thought $X$, does it work?", "Ok, how about $X'$, does it work?", "Maybe $X''$ works?", etc.  The phrase "I've come up with" is indicative of what is going on here.
Andrej Bauer
CC BY-SA 4.0
2018-09-27T10:15:43.983Z
On a technical level you failed to explain exactly how you're treating recursive types. Are you using equirecursive types, or isocrecursive types? It is not clear what you are asking.
Andrej Bauer
CC BY-SA 4.0
2018-09-27T12:30:51.323Z
@AndrejBauer I can see how it'd feel unmotivating to answer that kind of question. Your opinion is very valuable to me, so, learning you feel that way is a big alert to me. I'll raise considerably my threshold of when it is acceptable to ask a question, and try to only ask something when I can be much more precise about the involved definitions. Sorry about this, and thanks for letting me know how you feel instead of just giving up of answering without notice.
MaiaVictor
CC BY-SA 4.0
2018-09-27T12:32:08.173Z
@AndrejBauer I've attempted to edit this question to make it more technical and much more effortless to answer: i.e., the answer is either a "no, this is not known at all" or "yes, this actually is a misguided attempt to do what is called by the name X". If possible, please let me know if it is acceptable in this format; otherwise, I'll just delete it.
MaiaVictor
CC BY-SA 4.0
2018-09-27T13:51:08.487Z
You snuck in recursive types, so you're going to have non-termination. What is the normal form of something like `λ (X : X → X) . (λ x : X . x x) (λ x : X . x x)`? It or something similar will be typable, but I don't quite understand your setup. It would be better to explain your type theory by writing down inference rules, not Haskell code. It's a bad idea to bind type theory to an algorithm.
Andrej Bauer
CC BY-SA 4.0
2018-09-27T14:25:50.180Z
@AndrejBauer the point of this (renewed) question should be to ask whether making `X` bound in `A` inside `∀ (X : A) -> B` makes sense. The proof of `ind` with recursion was an example on where I found that to be useful, but that's not essential and, perhaps, I should just remove it completely? I've now updated the question with inference rules instead, but I'm not sure I got them correctly. Is this better? Anyway, from your comments I see how now poor my question was. Do you think I should just delete it?
MaiaVictor
CC BY-SA 4.0
2018-09-27T15:26:11.603Z
Well, now you deleted your intended use to get `ind`, so that's perhaps a bit too much :-) But don't delete the question. I think the idea still leads to non-terminating terms, I just have to find one that goes around your latest restriction.
Andrej Bauer
CC BY-SA 4.0
2018-09-27T15:40:14.960Z
@AndrejBauer oh, no, wait! I'm not claiming this language is terminating. It probably isn't. I'm literally just asking if the idea of having `X` to be in scope in `A` inside `∀ (X : A) -> B` has a name and/or makes sense. For example, imagine a language that allowed you to do it, and used **other means** to assure strong normalization: would it be useful in such language? The point of this exercise is to keep improving my intuition on "what power CoC is truly missing that makes it unable to prove induction". And please, don't worry about answering if it'll be costly to you!
MaiaVictor
CC BY-SA 4.0
2018-09-27T15:47:26.023Z
(A quick thought: I still do not understand if non-termination necessarily leads to inconsistency; I've seen people claiming both ways. Could there be a non-terminating language that is consistent if it somehow avoids `∀ (P : *) -> P` by other means?)
MaiaVictor
CC BY-SA 4.0
2018-09-27T15:57:34.177Z
There can be a non-terminating language that doesn't give inconsistency, simply introduce a type `Boogie` with a constant `boo` and reduction rule `boo ↦ boo`. Regarding your idea, you're just hiding recursive types inside `∀`, so I'd say you should instead cleanly separate those. The recursive types wil allow you to inhabit everything.
Andrej Bauer
CC BY-SA 4.0
2018-09-27T16:36:25.477Z
@AndrejBauer but from the lack of answers to that last question I assumed that even adding, to CoC, equirecursion (mutual `let` blocks, right?) or isorecursion (something like `mu`, right?) wouldn't be sufficient to derive induction (as a proper, normalizing term, not as bottom-elim!). Am I mistaken? In fact I couldn't even implement `bool-elim : ∀ (P : Bool -> *) -> P True -> P False -> ∀ (b : Bool) -> P b` in CoC + recursion. I've tried many different things. Are you sure that actually possible? Perhaps I should ask this as a separate question?
MaiaVictor
CC BY-SA 4.0
2018-09-27T20:11:50.607Z
Rather than asking "is this known?" I think it is usually more useful to ask about some specific question you want answered.  Suppose you discovered it *is* known; what would you do with that?  What specifically would you want to learn about it?  Is there a particular property that you want to know whether holds?  That makes it a technical question that is answerable in two ways, either by directly answering, or by providing a citation/reference.  I think "does it make sense?" is too vague -- what requirements would it need to meet for you to consider it to make sense?  Ask about those.
D.W.
CC BY-SA 4.0
2018-09-27T20:22:23.520Z
@D.W. I disagree about asking if this is known. If it was known, I'd have a name to search for and a whole internet of discussions to read; much more information than I could expect someone to answer here (and without the cost of giving that person work). I don't necessarily want to learn anything specific, so, inventing a property "I'm curious about" looks counter-productive. Sometimes I honestly just want a name/reference I can lookup. I agree "does it make sense" is extremely vague, though. I'll remove that part of the question.
MaiaVictor
CC BY-SA 4.0
2018-09-28T02:44:43.653Z
Victor, I invested time in a [good formal course in Type Theory](https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_YncjXRzdGq2SjKv5F2J8HUFeqN) and I found it totally worth it. Working through Robert Harper's [Practical Foundations](https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf) is even better idea.
Łukasz Lew
CC BY-SA 4.0
2018-09-28T13:20:04.643Z
@ŁukaszLew since you linked resources, do you have a good one on what it means to give a semantics to a language? I've been told this is the way one could justify changes to CoC (like the one I did), as proving consistency is seemingly not enough, but I have no idea on what that means. The practical foundations books seems to have a chapter on "constructive semantics", is that  what I'm looking for?
MaiaVictor
CC BY-SA 4.0
2018-09-28T15:14:17.677Z
@MaiaVictor Yes! And an excellent one at that! [The Type Soundness Theorem That You Really Want to Prove](https://www.youtube.com/watch?v=8Xyk_dGcAwk)
Łukasz Lew
<type-theory><calculus-of-constructions>
Is it reasonable to allow the type of a λ/∀-bound variable to refer to itself?
MaiaVictor
# Is it reasonable to allow the type of a λ/∀-bound variable to refer to itself?

(Asked by: username_0 on 2018-09-27)

Usually, in Pure Type Systems, the type of a `λ/∀`-bound variable is only accessible on its body. That is, on `λ (X : A) -> B`, `X` is free inside `A` and bound in `B`. But what if `X` was also bound in `A`? The typing rules should be updated accordingly, i.e., instead of:

$$ \frac{Γ \vdash A : \* \quad Γ, x : A \vdash B : \*}{Γ \vdash ∀ (x : A) \rightarrow B : \*}$$
$$ \frac{Γ \vdash f : ∀ (x : A) \rightarrow B \quad Γ \vdash a : A}{Γ \vdash f a : [a/x]B}$$

we'd have:

$$ \frac{Γ, x : A \vdash A : \* \quad Γ, x : A \vdash B : \*}{Γ \vdash ∀ (x : A) \rightarrow B : \*}$$
$$ \frac{Γ \vdash f : ∀ (x : A) \rightarrow B \quad Γ \vdash a : [a/x]A}{Γ \vdash f a : [a/x]B}$$

In other words, on the `∀ (x : A) -> B` case, in order to infer the type of `A`, we extend the context with `x : A`, which is possible, because we know the **value** of `A`. On the application case `f a` with `f : ∀ (x : A) -> B`, we substitute `x` by `a` in `A` before checking for equality. I have never seen such an approach, though. **My question is: was this explored before? If so, is there a name for it so I can look up? If not, is there an obvious reason for it to be undesirable?**

*(The reason I initially asked this question is I've [previously asked](https://cstheory.stackexchange.com/questions/39921/is-it-possible-to-derive-induction-by-extending-coc-with-recursion) if it is possible to implement a halting definition of `ind` on the calculus of constructions with equi-recursion. I've noticed one can do so in a setting with mutually recursive definitions, as long as we also allow a λ/∀-bound variable to refer to itself on its type. [Here is an example](https://gist.github.com/username_0/5d3385b7c117e29c006cae398a32a880).)*

**Tags:** type-theory, calculus-of-constructions

> **Comments:**
> **username_1**: I personally feel very unmotivated to keep answering a series of questions "I thought $X$, does it work?", "Ok, how about $X'$, does it work?", "Maybe $X''$ works?", etc.  The phrase "I've come up with" is indicative of what is going on here.  
> **username_1**: On a technical level you failed to explain exactly how you're treating recursive types. Are you using equirecursive types, or isocrecursive types? It is not clear what you are asking.  
> **username_0**: @AndrejBauer I can see how it'd feel unmotivating to answer that kind of question. Your opinion is very valuable to me, so, learning you feel that way is a big alert to me. I'll raise considerably my threshold of when it is acceptable to ask a question, and try to only ask something when I can be much more precise about the involved definitions. Sorry about this, and thanks for letting me know how you feel instead of just giving up of answering without notice.  
> **username_0**: @AndrejBauer I've attempted to edit this question to make it more technical and much more effortless to answer: i.e., the answer is either a "no, this is not known at all" or "yes, this actually is a misguided attempt to do what is called by the name X". If possible, please let me know if it is acceptable in this format; otherwise, I'll just delete it.  
> **username_1**: You snuck in recursive types, so you're going to have non-termination. What is the normal form of something like `λ (X : X → X) . (λ x : X . x x) (λ x : X . x x)`? It or something similar will be typable, but I don't quite understand your setup. It would be better to explain your type theory by writing down inference rules, not Haskell code. It's a bad idea to bind type theory to an algorithm.  
> **username_0**: @AndrejBauer the point of this (renewed) question should be to ask whether making `X` bound in `A` inside `∀ (X : A) -> B` makes sense. The proof of `ind` with recursion was an example on where I found that to be useful, but that's not essential and, perhaps, I should just remove it completely? I've now updated the question with inference rules instead, but I'm not sure I got them correctly. Is this better? Anyway, from your comments I see how now poor my question was. Do you think I should just delete it?  
> **username_1**: Well, now you deleted your intended use to get `ind`, so that's perhaps a bit too much :-) But don't delete the question. I think the idea still leads to non-terminating terms, I just have to find one that goes around your latest restriction.  
> **username_0**: @AndrejBauer oh, no, wait! I'm not claiming this language is terminating. It probably isn't. I'm literally just asking if the idea of having `X` to be in scope in `A` inside `∀ (X : A) -> B` has a name and/or makes sense. For example, imagine a language that allowed you to do it, and used **other means** to assure strong normalization: would it be useful in such language? The point of this exercise is to keep improving my intuition on "what power CoC is truly missing that makes it unable to prove induction". And please, don't worry about answering if it'll be costly to you!  
> **username_0**: (A quick thought: I still do not understand if non-termination necessarily leads to inconsistency; I've seen people claiming both ways. Could there be a non-terminating language that is consistent if it somehow avoids `∀ (P : *) -> P` by other means?)  
> **username_1**: There can be a non-terminating language that doesn't give inconsistency, simply introduce a type `Boogie` with a constant `boo` and reduction rule `boo ↦ boo`. Regarding your idea, you're just hiding recursive types inside `∀`, so I'd say you should instead cleanly separate those. The recursive types wil allow you to inhabit everything.  
> **username_0**: @AndrejBauer but from the lack of answers to that last question I assumed that even adding, to CoC, equirecursion (mutual `let` blocks, right?) or isorecursion (something like `mu`, right?) wouldn't be sufficient to derive induction (as a proper, normalizing term, not as bottom-elim!). Am I mistaken? In fact I couldn't even implement `bool-elim : ∀ (P : Bool -> *) -> P True -> P False -> ∀ (b : Bool) -> P b` in CoC + recursion. I've tried many different things. Are you sure that actually possible? Perhaps I should ask this as a separate question?  
> **username_2**: Rather than asking "is this known?" I think it is usually more useful to ask about some specific question you want answered.  Suppose you discovered it *is* known; what would you do with that?  What specifically would you want to learn about it?  Is there a particular property that you want to know whether holds?  That makes it a technical question that is answerable in two ways, either by directly answering, or by providing a citation/reference.  I think "does it make sense?" is too vague -- what requirements would it need to meet for you to consider it to make sense?  Ask about those.  
> **username_0**: @username_2 I disagree about asking if this is known. If it was known, I'd have a name to search for and a whole internet of discussions to read; much more information than I could expect someone to answer here (and without the cost of giving that person work). I don't necessarily want to learn anything specific, so, inventing a property "I'm curious about" looks counter-productive. Sometimes I honestly just want a name/reference I can lookup. I agree "does it make sense" is extremely vague, though. I'll remove that part of the question.  
> **username_3**: Victor, I invested time in a [good formal course in Type Theory](https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_YncjXRzdGq2SjKv5F2J8HUFeqN) and I found it totally worth it. Working through Robert Harper's [Practical Foundations](https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf) is even better idea.  
> **username_0**: @ŁukaszLew since you linked resources, do you have a good one on what it means to give a semantics to a language? I've been told this is the way one could justify changes to CoC (like the one I did), as proving consistency is seemingly not enough, but I have no idea on what that means. The practical foundations books seems to have a chapter on "constructive semantics", is that  what I'm looking for?  
> **username_3**: @username_0 Yes! And an excellent one at that! [The Type Soundness Theorem That You Really Want to Prove](https://www.youtube.com/watch?v=8Xyk_dGcAwk)  

---

## 3 answers

### Answer by username_4 on 2018-09-28. Score: 10

I have not seen this in a dependently-typed setting, but a similar notion is fairly well-known in weaker systems (e.g. System F) with subtyping, under the term "F-bounded quantification". This pops up prominently in type systems for object-oriented programming languages, which typically are heavy on (equi-) type recursion. This notion was originally introduced by this paper.
A standard use case is expressing forms of "binary methods" that need to be covariant in their argument types. For example, in those languages you see interface types like
interface Ordered { less(x : T) : Bool }

with subtypes like
class Int extends Ordered { ... }

and usage patterns
class Queue> { ... }

or
sort>(array : Array) : Array

and so on. In the more type-theoretical rendering of System F-sub with F-bounded quantification and records these could be expressed as
Ordered = λ(T <: Top). {less : T → Bool}
Int <: Ordered(Int)
Queue = λ(T <: Ordered(T)). {...}
sort : ∀(T <: Ordered(T)). Array(T) → Array(T)

> **Comments:**
> **username_0**: I was almost regretting having asked that question, thanks a lot for those resources.  
> **username_1**: Thanks for the answer. I'd just like to observe that the examples mentioned by @AndreasRossberg all come from programming langauges with general recursion. I thought one of the important facets of the question was whether we can have this sort of recursion without inhabiting every type.  
> **username_4**: @AndrejBauer, yes, good point. This kind of recursive binding hardly makes sense in the absence of general recursive types. And those immediately enable expressing general recursion on the term level.  
> **username_5**: @AndreasRossberg Wang and Rompf encode F-bounds in a strongly normalizing subset of DOT, where variables are bound in their own type: https://www.cs.purdue.edu/homes/rompf/papers/wang-ecoop17.pdf. Function types stick to usual scoping but I expect they could be changed.  
> **username_5**: Beware that mu-types in that paper are not quite recursive types. Dreyer suggested to me they resemble recursively-defined signatures (“What is a recursive module?”, PLDI’99). And somebody (IIRC Sandro Stucki?) pointed out they resemble Fu and Stump’s \iota-types (in their 2014 version, which differs from modern Cedille: http://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf).  

---

### Answer by username_6 on 2018-09-30. Score: 4

Your question is somewhat related to some work I did (sorry for the self-advertisement), where I encode some weak form of dependent type into a Curry-style language (kind of an extension of System F). The idea is to encode the dependent function type $\forall x{\in}A \Rightarrow B$ as $\forall x (x{\in}A \Rightarrow B)$. This encoding relies on first-order quantification and on a specific membership type $t{\in}A$, which intuitively corresponds to the singleton type $\{t\}$ when $t$ is in $A$, and it is empty otherwise. Otherwise said, this type quantifies on every possible term of the language, but terms with the wrong type are filtered out by membership (this is related to the relativized quantification scheme, which is used a lot in (classical) realizability settings).

So how does this relate to your question? In my setting, you can get in a situation where you (kind of, but not really as explained further) have a judgement of the form $Γ, x : x{\in}A \vdash t : B$ (or more generally $Γ, x : u{\in}A \vdash t : B$), and the following rule is used to destruct membership types in the context.
$$
\frac{\Gamma, x : A, x \equiv u \vdash t : B}
{\Gamma, x : u{\in}A \vdash t : B}
$$

To go back to the encoding of dependent function types, being slightly more precise (things are subtle), you can get typing derivations of the following form.
$$
\dfrac{
\dfrac{
\dfrac{\Gamma, x : A, x \equiv y \vdash t : B}{\Gamma, x : y{\in}A \vdash t : B}}
{\Gamma \vdash \lambda x.t : y{\in}A \Rightarrow B} \hspace{1cm} y \notin \Gamma}
{\Gamma \vdash \lambda x.t : \forall y (y{\in}A \Rightarrow B)}
$$
One thing to note is that we actually have two different variables: one bound by the $\lambda$-abstraction, and another one bound by the first-order quantifier. However, we known that they are equal ($x \equiv y$ is in the context). Using a substitution rule and some weakening you can actually go a bit further and get an hypothesis of the form $\Gamma, x : A \vdash t : B[y := x]$.

Sorry for the rough answer, I don't have time to do better right now. If you want to know more, check out [this paper](https://doi.org/10.1007/978-3-662-49498-1_19) or [my thesis](https://tel.archives-ouvertes.fr/tel-01682908).


---

### Answer by username_7 on 2018-10-01. Score: 3

It is rather unusual for the *type* of `x` to be allowed to refer to `x`.

Your proposed typing rules are problematic when they say `Γ,x:A ⊢ A:∗` because that relies on a different notion of environment than usual: normally the type of a new element `x` (i.e. `A` here) must be closed over the prefix (i.e. `Γ` here), whereas in your case `A` can have `x` as free variable.

[ You say it "is possible, because we know the value of A" but I fail to see what you mean by that. ]

In any case, the usual way to circumvent this is to do as Rodolphe suggests, i.e. split the introduction of `x` into two steps: `∀x:T. ∀_:P(x). e`. You can think of System F-sub in the same way: `∀(T <: Ordered(T)). e` becomes `∀(T:*). ∀(P : (T <: Ordered(T))). e`.

Within the context of type-theory, the "tightest" form of recursion I know is that allowed by induction-recursion and induction-induction, with which you're probably familiar since your sample code is in Agda.

One last thing: I'm not sure exactly what you mean by `n : Nat n` in your sample code, but it sounds very much like a singleton type, so maybe you can break the recursion using singleton types and rewrite your code as: `∀(n : Nat). ∀(sn : SNat n). ...`.


---

