Моделирование параметрического полиморфизма системы F при множестве

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

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

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

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?

1 ответ

Вместо

evalTy : Type → Set

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

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

(Андраш Ковач, хотите добавить ответ со ссылками на ваше вложение предикативной Системы 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

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

Например

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ω

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

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

Обратите внимание, что я говорю только о предикативном фрагменте Системы F. Полная Система F не является встраиваемой, как объясняет Доминик Деврисе в своих комментариях к вопросу.

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

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

Другие вопросы по тегам