3
$\begingroup$

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

$\endgroup$
  • 7
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Sep 27 '18 at 10:12
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Sep 27 '18 at 10:15
  • 1
    $\begingroup$ @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. $\endgroup$ – MaiaVictor Sep 27 '18 at 12:30
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Sep 27 '18 at 15:26
  • 2
    $\begingroup$ 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. $\endgroup$ – D.W. Sep 27 '18 at 20:11
10
$\begingroup$

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)
$\endgroup$
  • $\begingroup$ I was almost regretting having asked that question, thanks a lot for those resources. $\endgroup$ – MaiaVictor Sep 28 '18 at 15:56
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Sep 29 '18 at 20:35
  • $\begingroup$ @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. $\endgroup$ – Andreas Rossberg Sep 29 '18 at 22:44
  • $\begingroup$ @AndreasRossberg Wang and Rompf encode F-bounds in a strongly normalizing subset of DOT, where variables are bound in their own type: cs.purdue.edu/homes/rompf/papers/wang-ecoop17.pdf. Function types stick to usual scoping but I expect they could be changed. $\endgroup$ – Blaisorblade Feb 13 at 18:18
  • $\begingroup$ 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: homepage.divms.uiowa.edu/~astump/papers/…). $\endgroup$ – Blaisorblade Feb 13 at 18:27
4
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.