Is it reasonable to allow the type of a λ/∀-bound variable to refer to itself?

Question

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 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.)

Answer 1

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<T> { less(x : T) : Bool }

with subtypes like

class Int extends Ordered<Int> { ... }

and usage patterns

class Queue<T extends Ordered<T>> { ... }

or

sort<T extends Ordered<T>>(array : Array<T>) : Array<T>

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)

Answer 2

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 or my thesis.

Answer 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). ....