Моделирование параметрического полиморфизма системы F при множестве
В Системе F тип полиморфного типа *
(поскольку это единственный тип в System F в любом случае...), например, для следующего закрытого типа:
[] ⊢ (forall α : *. α → α) : *
Я хотел бы представлять System F в Агде, и потому что все в *
, Я думал, что я буду интерпретировать типы (как и выше) как Agda Set
s; так что-то вроде
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 [α])
, что делает Агда с неявными аргументами (верно?). Так что мне не ясно, что именно мы не можем встроить.