Параметрический полиморфизм моделирования F в Set₀

Question

В системе F тип полиморфного типа - * (так как это единственный вид в System F в любом случае ...), так, например, для следующего закрытого типа:

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

Я хотел бы представить System F в Agda, и потому, что все в *, я думал, что интерпретировать типы (как выше), как Agda Set с; так что-то вроде

evalTy : RepresentationOfAWellKindedClosedType → Set 

Однако Agda не имеет полиморфные типы, поэтому указанные выше типа, в Agda, должны были бы быть (большой!) тип Π:

idType = (α : Set) → α → α 

, что означает его не в Set₀:

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

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

есть ли выход из этого, или система F не вложим в этом смысле в Agda?

Answer 1

Вместо

evalTy : Type → Set 

вы можете написать

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

(András Kovács, уход, чтобы добавить ответ со ссылками на ваше вложение предиктивного F?)

Этих достаточно для встраивания, но я видел много ошибок Setω, и они травмировали меня, так что теперь я пытаюсь чтобы как можно больше избежать зависимых вселенных.

Вы можете вставлять полиморфные типы в Set₁ и мономорфные типы в Set, поэтому вы можете вставлять любой тип в Set₁ с помощью уродливого механизма подъема. Я пробовал это несколько раз, и это всегда было ужасно.

То, что я хотел бы попробовать, чтобы определить evalTy, как

evalTy : Type -> Set ⊎ Set₁ 

, а затем устранить ее на уровне типа, как это:

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) 

Вы можете запустить это исключение:

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 

Таким образом, вы вводите зависимость юниверса только в конце, когда вам действительно нужно вычислить что-то.

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 является зависимой функцией, а не «универсально зависит», вы можете написать, например, f = ofSomeSet ∘ suc, и это совершенно понятное выражение.Это не работает с вселенными зависимостями:

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ω 

Вы можете также повысить [_,_]ᵀ, чтобы сделать его отображаемым, как я сделал here, но все это, вероятно, слишком, и вы должны просто использовать

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

Обратите внимание, что Я говорю только о предикативном фрагменте System F. Full System F не встраивается как Dominique Devriese объясняет в своих комментариях к вопросу.

Однако я чувствую, что мы можем встроить больше, чем предикативный фрагмент, если мы сначала нормализуем термин System F. Например. id [∀ α : *. α → α] id не является непосредственно встраиваемым, но после нормализации он становится только id, который встраивается.

Однако должно быть возможно встраивать id [∀ α : *. α → α] id даже без нормализации, преобразовывая его в Λ α. id [α → α] (id [α]), что и делает Agda с неявными аргументами (справа?). Поэтому мне непонятно, что именно мы не можем внедрить.