在Set₀建模系统F的参数多态性 [英] Modeling System F's parametric polymorphism at Set₀

问题描述

在系统F中，多态类型的种类是*(因为无论如何这是系统F中唯一的种类...)，例如对于以下封闭类型:

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 α : *. α → α) : *

我想用Agda表示系统F，并且因为所有内容都在*中，所以我想将类型(如上)解释为Agda Set s；像这样

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

但是，Agda没有多态类型，因此在Agda中，上述类型必须是(大！)Π类型:

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

idType = (α : Set) → α → α

这意味着它不在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

有没有解决的办法，或者系统F在这种意义上不能嵌入到Agda中?

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

推荐答案

代替

evalTy : Type → Set

你可以写

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

(AndrásKovács，想添加一个引用与您引用谓词系统F的嵌入吗?)

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

这足以嵌入，但是我已经看到很多Setω错误，它们使我很受苦，所以现在我正尝试尽可能避免依赖宇宙.

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.

您可以将多态类型嵌入到Set₁中，将单态类型嵌入到Set中，因此您可以使用丑陋的提升机制将任何类型嵌入到Set₁中.我试了几次，一直很糟糕.

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.

我要尝试的是将evalTy定义为

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

因此，您仅在实际上需要计算某些内容时才引入Universe依赖项.

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

例如

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，它是一个完全可键入的表达式.这不适用于Universe依赖项:

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

请注意，我只是在谈论系统F的谓词片段.完整系统F不可嵌入，因为 Dominique Devriese 在他对该问题的评论中对此进行了解释.

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.

但是，如果我首先对System F术语进行归一化处理，那么我觉得我们可以嵌入的不仅仅是谓词片段.例如. id [∀ α : *. α → α] id不能直接嵌入，但是在归一化后，它变成可以嵌入的id.

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.

但是，即使不进行标准化也可以嵌入id [∀ α : *. α → α] id，方法是将其转换为Λ α. id [α → α] (id [α])，这就是Agda使用隐式参数的方式(对吗?).因此，我不清楚我们到底不能嵌入什么.

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.

这篇关于在Set₀建模系统F的参数多态性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！