Lambda the Ultimate

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 caught back by predicativity. How would you
encode:

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

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

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.

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.

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.