OTT中的自我表示和宇宙 [英] Self-representation and universes in OTT

问题描述

问题是关于观测类型理论.

请考虑以下设置:

data level : Set where
  # : ℕ -> level
  ω : level

_⊔_ : level -> level -> level
# α ⊔ # β = # (α ⊔ℕ β)
_   ⊔ _   = ω

_⊔ᵢ_ : level -> level -> level
α ⊔ᵢ # 0 = # 0
α ⊔ᵢ β   = α ⊔ β

mutual
  Prop = Univ (# 0)
  Type = Univ ∘ # ∘ suc

  data Univ : level -> Set where
    bot  : Prop
    top  : Prop
    nat  : Type 0
    univ : ∀ α -> Type α
    σ≡    : ∀ {α β γ} -> α ⊔  β ≡ γ -> (A : Univ α) -> (⟦ A ⟧ -> Univ β) -> Univ γ
    π≡    : ∀ {α β γ} -> α ⊔ᵢ β ≡ γ -> (A : Univ α) -> (⟦ A ⟧ -> Univ β) -> Univ γ
    πᵤ   : ∀ {α} -> (A : Univ α) {k : ⟦ A ⟧ -> level} -> (∀ x -> Univ (k x)) -> Univ ω

  ⟦_⟧ : ∀ {α} -> Univ α -> Set
  ⟦ bot      ⟧ = ⊥
  ⟦ top      ⟧ = ⊤
  ⟦ nat      ⟧ = ℕ
  ⟦ univ α   ⟧ = Univ (# α)
  ⟦ σ≡ _ A B ⟧ = Σ ⟦ A ⟧ λ x -> ⟦ B x ⟧
  ⟦ π≡ _ A B ⟧ = (x : ⟦ A ⟧) -> ⟦ B x ⟧
  ⟦ πᵤ   A B ⟧ = (x : ⟦ A ⟧) -> ⟦ B x ⟧

prop = univ 0
type = univ ∘ suc

我们有一个分层的宇宙层次结构:Prop : Type 0 : Type 1 : ...(其中Prop是强制性的)，Σ型和Π型的代码以及一个额外的代码πᵤ用于"Universe polymorphicΠ型".就像在Agda中，∀ α -> Set α具有[隐藏]类型Setω一样，π nat univ具有类型Univ ω.

We have a stratified hierarchy of universes: Prop : Type 0 : Type 1 : ... (where Prop is impredicative), the codes for Σ- and Π-types and one additional code πᵤ for "universe polymorphic Π-types". Just like in Agda ∀ α -> Set α has [the hidden] type Setω, π nat univ has type Univ ω.

带有一些快捷方式

_&_ : ∀ {α β} -> Univ α -> Univ β -> Univ (α ⊔  β)
A & B = σ A λ _ -> B

_⇒_ : ∀ {α β} -> Univ α -> Univ β -> Univ (α ⊔ᵢ β)
A ⇒ B = π A λ _ -> B

_‵π‵_ : ∀ {α β} -> (A : Univ α) -> (⟦ A ⟧ -> Univ β) -> Univ (α ⊔ᵢ β)
_‵π‵_ = π

_‵πᵤ‵_ : ∀ {α} -> (A : Univ α) {k : ⟦ A ⟧ -> level} -> (∀ x -> Univ (k x)) -> Univ ω
_‵πᵤ‵_ = πᵤ

我们可以使用目标语言构造来定义许多功能，例如

we can define many functions using the target language constructs, e.g.

_≟ₚ_ : ⟦ nat ⇒ nat ⇒ prop ⟧
zero  ≟ₚ zero  = top
suc n ≟ₚ suc m = n ≟ₚ m
_     ≟ₚ _     = bot

用一种虚构的语言，我们可以识别代码和相应的类型，从而形成一个封闭的反身宇宙(我们还需要一些数据类型的一阶表示，但这是另一回事了).但是请考虑通常的类型相等性:

In an imaginary language we can identify codes and the corresponding types, thus forming a closed reflexive universe (we also need some first-order representation of data types, but that's another story). But consider the usual equality of types:

Eq : ∀ {α β} -> Univ α -> Univ β -> Prop

如何将其嵌入目标语言?我们可以写

How to embed this in the target language? We can write

EqEmb : ⟦ (nat ‵πᵤ‵ λ α → nat ‵πᵤ‵ λ β → univ α ⇒ univ β ⇒ prop) ⟧

，但是请注意，目标语言不包含有关ω的任何内容.在Eq中，我们可以像这样对参数进行模式匹配:

but notice that the target language doesn't contain anything about ω. In Eq we can pattern match on the arguments like this:

Eq (πᵤ A₁ B₁) (πᵤ A₂ B₂) = ...

α和β都变为ω，一切都很好.但是在EqEmb中，我们无法像这样进行模式匹配，因为在univ α中，α是一个数字，并且不能为ω，所以⟦ univ α ⟧绝不是Univ ω.

α and β both become ω and everything is fine. But in EqEmb we can't pattern-match like this, because in univ α α is a number and cannot be ω, so ⟦ univ α ⟧ is never Univ ω.

假设我们可以对普通的Agda类型进行模式匹配.然后我们可以编写一个确定某个值是否为函数的函数:

Let's say we can pattern match on plain Agda types. Then we could write a function that determines whether some value is a function:

isFunction : ∀ {α} {A : Set α} -> A -> Bool
isFunction {A = Π A B} _ = true
isFunction             _ = false

但是，如果B是与宇宙相关的"，并且具有这种类型:∀ α -> Set α，该怎么办?然后Π A B具有类型Setω，并且α与ω统一.但是，如果我们可以使用ω实例化级别变量，那么我们可以编写类似

But what if B is "universe dependent" and has, say, this type: ∀ α -> Set α? Then Π A B has type Setω and α is unified with ω. But if we could instantiate level variables with ω, then we could write things like

Id : Set ω
Id = ∀ α -> (A : Set α) -> A -> A

id : Id
id α A x = x

id ω Id id ~> id

那是强制性的(尽管我不知道这种特殊形式的强制性是否会导致不一致.是吗?)

That's impredicative (Although I don't know whether this particular form of impredicativity leads to inconsistency. Does it?).

因此，我们不能将ω作为法律级别添加到目标语言，并且在存在依赖于宇宙的函数"的情况下，也不能在Set α上进行模式匹配.因此，反身"平等

So we can't add ω as a legal level to the target language and we can't pattern match on Set α in the presence of "universe dependent" functions. Thus the "reflexive" equality

EqEmb : ⟦ (nat ‵πᵤ‵ λ α → nat ‵πᵤ‵ λ β → univ α ⇒ univ β ⇒ prop) ⟧

并非为所有Universe多态函数(不是"Universe依赖")定义

.例如. map

is not defined for all universe polymorphic functions (not "universe dependent"). E.g. the type of type of map

map : ∀ {α β} {A : Set α} {B : Set β} -> (A -> B) -> List A -> List B

是Setω，我们不能问Eq (typeOf emb-map) (typeOf emb-map)，因为在Eq A B中，A的类型是⟦ univ α ⟧，这是一个有限"的宇宙(对B也是一样的)

is Setω and we can't ask whether Eq (typeOf emb-map) (typeOf emb-map), because in Eq A B the type of A is ⟦ univ α ⟧, which is a "finite" universe (the same holds for B).

那么有可能以一种类型明确的方式将OTT本身嵌入吗?如果没有，我们可以以某种方式作弊吗?我们可以像一切都很好"一样以依赖于宇宙"的功能在Set α上进行模式匹配吗?

So is it possible to embed OTT in itself in a well-typed way? If not, can we cheat somehow? Can we pattern match on Set α in the presense of "universe dependent" functions like everything is fine?

推荐答案

我最终获得了以下层次结构:

I ended up with the following hierarchy:

Prop : Type 0 : Type 1 : ...
(∀ α -> Type α) : Type ω₀ : Type ω₁

没有Type ω₁的代码，因为以前没有Type ω₀的代码，但是我们需要Type ω₀的代码才能定义Universe多态函数的相等性，而Type ω₁的代码则更少有用.

There is no code for Type ω₁ as there was no code for Type ω₀ before, but we need a code for Type ω₀ to be able to define equality of universe polymorphic functions and a code for Type ω₁ is less useful.

现在我们有四个与宇宙有关的量词

Now we have four universe dependent quantifiers

σ₀ π₀   : {α : Lev false}
        -> (A : Univ α) {k : ⟦ A ⟧ -> Lev false} -> (∀ x -> Univ (k x)) -> Univ {false} ω₀
σ₁ π₁   : ∀ {a} {α : Lev a}
        -> (A : Univ α) {b : ⟦ A ⟧ -> Bool} {k : ∀ x -> Lev (b x)}
        -> (∀ x -> Univ (k x))
        -> Univ ω₁

重点是，现在可以在π₀上进行模式匹配，从而可以定义Universe多态函数的相等性，但是不可能在π₁上进行模式匹配(与π₀一样，称为πᵤ )，我们可以接受.

The point is that it's now possible to pattern match on π₀ thus allowing to define equality of universe polymorphic functions, but it's impossible to pattern match on π₁ (as was with π₀ which was called πᵤ) and we can live with that.

等式具有以下自反"类型:

Equalities have these "reflexive" types:

mutual
  Eq : ⟦ (π₁ lev λ α -> π₁ lev λ β -> univ⁺ α ⇒ univ⁺ β ⇒ prop) ⟧
  eq : ⟦ (π₁ lev λ α -> π₁ lev λ β -> π (univ⁺ α) λ A -> π (univ⁺ β) λ B -> A ⇒ B ⇒ prop) ⟧

代码位于此处.但是，看来我需要再次扩展层次结构才能证明一致性.我会问一个问题.

The code is here. However it looks like I need to extend the hierarchy once again to be able to prove coherence. I'll ask a question about that.

这篇关于OTT中的自我表示和宇宙的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！