Encoding System Fw in predicative dependent type theory

System Fω appears impredicative, but I'm wondering if there is an easy way to embed it into predicative dependent type theory by inferring bounds on universes. Also, if anyone can provide an example of a System Fω term that would be rejected by Coq's typical ambiguity resolver, that would be helpful to me.

Any references or thought are appreciated.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


I'm not sure what you mean by "a term that would be rejected", but the following program is a rather natural equivalent of System F's polymorphic identity, and fails with an universe consistency problem:

Coq < Definition id (X : Type) (x : X) := x.
id is defined

Coq < Set Printing Universes.

Coq < Check id.
     : forall X : Type (* Top.1 *), X -> X

Coq < Check (id _ id).
Error: Universe inconsistency (cannot enforce Top.1 < Top.1).


Yes, that's what I meant. I guess I should have waited to try it before posting (I don't have Coq on this machine), but I thought that case worked (I thought each use of 'id' received its own universe graph). But still I could have just made id a parameter, so I guess that was a trivial question.

I'm still interested in the more general question of encoding System F in a language with explicit universe polymorphism. Maybe like:

id :: forall U:Univ, X:U. X -> X
id U X x = x

newId :: forall U:Univ, X:U. X -> X
newId U X = id (succ U) (forall X':U. X' -> X') (id U X)

This would encode terms of System F at Setω. Some care would be needed when encoding quantified types, so that you don't end up at Setω+1. I'm interested in whether something along these lines is will work or whether there are obstructions.

I fear you will always be

I fear you will always be caught back by predicativity. How would you

  let id = Λα λ(x:α) x
  let auto (x : ∀α.α→α) = x [∀α.α→α] x
  auto id


My hope is that each term in System F only needs some finite number universes to work (that number depending on the term). So you would lift the universe parameterization to the outermost position for each term. And then you'd use some bounded polymorphic version for nested functions.

Your 'auto' might have this type:

auto :: forall U:Univ.  (forall U':Univ[succ U]. T:U'. T -> T) -> (forall U':Univ[U]. T:U'. T -> T)

Here, Univ[U] means the type of universes of level at most U. By keeping such a bound, we allow that function to exist at a small level. I can go into more detail after lunch if you didn't follow that, but I think that type would allow you to derive the previously mentioned type for 'auto id'.

I agree this type is

I agree this type is reasonable for `auto` if you have universe subsumption (a subtyping relation from lower to higher universe levels).

If I remember correctly, a problem with universe polymorphism is that, while "best" universe levels can be inferred in a closed program, as soon as you export some function to users you have to make a choice. There is some discussion of how Coq aggravates this problem by keeping universe level implicit in Judicaël Courant's work, but even with explicit level notations you have to make a choice on the ordinal bound of universe quantification. You get the same kind of problems you had without polymorphism, only later.

(So my intuition is that you could succeed in translating all impredicatively type-correct closed programs in a predicative system, but that this translation will not be closed under all contexts.)

Modularity of the encoding

(Aside: I think the type I gave relies on explicit universe polymorphism rather than a cumulativity/subsumption rule, but I might be missing your point.)

Otherwise, I agree with the potential problem you've pointed out. Consider the functions defined by:

auto2 :: (forall a. a->a) -> (forall a. a->a) -> (forall a. a->a)
auto2 id1 id2 = id1 id2

auto2' :: (forall a. a->a) -> (forall a. a->a) -> (forall a. a->a)
auto2' id1 id2 = id2 id1

Continuing the pattern used above to type auto, we can type auto2 and auto2' but it would assign them different types (recording which parameter could be applied to the other), even though they have the same type in System F. This is a modularity problem (leaking implementation details).

So, it would be desirable to have a single mapping of each System F type to a corresponding encoded type such that any conforming System F term can be mapped to an encoded term with that encoded type. Since implementations of a fixed type can require arbitrarily many universes, that means the type for auto2 would need to use an at least slightly different encoding to achieve this property. My intuition says it still might be possible, though.

What about Reynolds?

The predicative type theories known to me all have pretty straightforward set theoretic models. Using Reynolds result in "Polymorphism is not Set-Theoretic", an encoding like the one you are trying to construct seems to be impossible.
Or is your encoding so creative that the composition with a set-theoretic semantics does not fit Reynolds assumptions?!

but even with explicit level notations you have to make a choice on the ordinal bound of universe quantification. You get the same kind of problems you had without polymorphism, only later.
I don't understand: Courant's universe variables only get assigned lower-bounds, never upper bounds (because only fresh universe levels get lower bounds). So all theory content can be made arbitrarily large.
As long you don't want to write down paradoxes (see Coquand - A new paradox in type theory), I don't see the problem.

Partial model

My idea was to give a model for each context, where only a finite number of universes would be needed for any fixed context. I'll have to go look at Reynolds again to see if it applies to that setup, but I don't think it does.

I was thinking that in a dependent type theory, you'd have to prove something like this: assuming all functions in sight only use a bounded number of universe levels, the new functions I'm constructing also have this property. I think for terms in System F this check would be trivial, whereas inductive definitions would really need to check something.

Paradoxical term is paradoxical in his context

If I remember Reynold's proof correctly, he is exhibiting a paradoxical term whose semantics leads to a contradiction. And his assumptions about the set-theoretic semantics are very reasonable (which is why he gets away with the title in the first place).

If you don't weaken your proposition to something like "all System F terms of practical interest can be encoded with universes", then I don't see how you could possibly make this work. If you still think you can, this will suprise lots of people, so better check it formally.


I'll put this on my list of things to do with my vast amounts of free time.


Bounds on bounding

A technique for "inferring bounds on universes" sounds a little like a technique for finding ordinal bounds on classes of types, and it looks like this is something that can't be done constructively/predicatively. I said something about this in an answer to Can we prove weak normalization for System F by induction on a transfinite ordinal on cstheory - if we are talking about plain Martin-Lof type theory with predicative universes and well-founded types, then I think the difference in provability strength between the systems is going to sharpen this into provably impossible.

But if you can constrain what you need to do (e.g., in the discussion above, all the properly 2nd-order quantification was monadic), then you can probably get something to work.