Modeling System F's parametric polymorphism at Set₀

Question

In System F, the kind of a polymorphic type is * (as that's the only kind in System F anyway...), so e.g. for the following closed type:

[] ⊢ (forall α : *. α → α) : *

I would like to represent System F in Agda, and because everything is in *, I thought I'd interpret types (like the above) as Agda Sets; so something like

evalTy : RepresentationOfAWellKindedClosedType → Set

However, Agda doesn't have polymorphic types, so the above type, in Agda, would need to be a (large!) Π type:

idType = (α : Set) → α → α

which means it is not in Set₀:

idType : Set
idType = (α : Set) → α → α

poly-level.agda:4,12-29
Set₁ != Set
when checking that the expression (α : Set) → α → α has type Set

Is there a way out of this, or is System F not embeddable in this sense into Agda?

Answer 1

Instead of

evalTy : Type → Set

you can write

evalTy : (σ : Type) -> Set (levelOf σ)

(András Kovács, care to add an answer with references to your embedding of predicative System F?)

This is enough for embedding, but I've seen a lot of Setω errors and they have traumatised me, so now I'm trying to avoid dependent universes as much as possible.

You can embed polymorphic types into Set₁ and monomorphic types into Set, so you can embed any type into Set₁ using the ugly lifting mechanism. I tried this several times and it always was awful.

The thing I would try is to define evalTy as

evalTy : Type -> Set ⊎ Set₁

and then eliminate it at the type level like this:

data [_,_]ᵀ {α β γ δ} {A : Set α} {B : Set β} (C : A -> Set γ) (D : B -> Set δ)
            : A ⊎ B -> Set (γ ⊔ δ) where
  inj¹ : ∀ {x} -> C x -> [ C , D ]ᵀ (inj₁ x)
  inj² : ∀ {y} -> D y -> [ C , D ]ᵀ (inj₂ y)

You can run this elimination:

Runᴸ : ∀ {α β γ δ} {A : Set α} {B : Set β} {C : A -> Set γ} {D : B -> Set δ} {s}
     -> [ C , D ]ᵀ s -> Level
Runᴸ {γ = γ} (inj¹ _) = γ
Runᴸ {δ = δ} (inj² _) = δ

Runᵀ : ∀ {α β γ δ} {A : Set α} {B : Set β} {C : A -> Set γ} {D : B -> Set δ} {s}
     -> (sᵀ : [ C , D ]ᵀ s) -> Set (Runᴸ sᵀ) 
Runᵀ {C = C} (inj¹ {x} _) = C x
Runᵀ {D = D} (inj² {y} _) = D y

runᵀ : ∀ {α β γ δ} {A : Set α} {B : Set β} {C : A -> Set γ} {D : B -> Set δ} {s}
     -> (sᵀ : [ C , D ]ᵀ s) -> Runᵀ sᵀ
runᵀ (inj¹ z) = z
runᵀ (inj² w) = w

Thus you introduce a universe dependency only at the end, when you actually need to compute something.

E.g.

SomeSet : ℕ -> Set ⊎ Set₁
SomeSet 0 = inj₁ ℕ
SomeSet n = inj₂ Set

ofSomeSet : ∀ n -> [ (λ A -> A × A) , id ]ᵀ (SomeSet n)
ofSomeSet  zero   = inj¹ (0 , 5)
ofSomeSet (suc n) = inj² ℕ

-- 0 , 5
test₁ : ℕ × ℕ
test₁ = runᵀ (ofSomeSet 0)

-- ℕ
test₂ : Set
test₂ = runᵀ (ofSomeSet 1)

ofSomeSet is a dependent function, but not a "universally dependent", you can write e.g. f = ofSomeSet ∘ suc and it's a perfectly typeable expression. This doesn't work with universes dependencies:

fun : ∀ α -> Set (Level.suc α)
fun α = Set α

oops = fun ∘ Level.suc

-- ((α : Level) → Set (Level.suc α)) !=< ((y : _B_160 .x) → _C_161 y)
-- because this would result in an invalid use of Setω

You can also enhance [_,_]ᵀ to make it mappable like I did here, but this all is probably overkill and you should just use

evalTy : (σ : Type) -> Set (levelOf σ)

Note that I'm talking only about the predicative fragment of System F. Full System F is not embeddable as Dominique Devriese explains in his comments to the question.

However I feel like we can embed more than the predicative fragment, if we first normalize a System F term. E.g. id [∀ α : *. α → α] id is not directly embeddable, but after normalization it becomes just id, which is embeddable.

However it should be possible to embed id [∀ α : *. α → α] id even without normalization by transforming it into Λ α. id [α → α] (id [α]), which is what Agda does with implicit arguments (right?). So it's not clear to me what exactly we can't embed.