Вопрос о Observational Type Theory.Самопрезентация и вселенные в 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 является непредикативным), коды для сга и П-типов и один дополнительный кода πᵤ для «вселенского полиморфного П -типы». Так же, как в Agda ∀ α -> Set α имеет [скрытый] тип Setω, π nat univ имеет тип 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 ω
_‵πᵤ‵_ = πᵤ
мы можем определить множество функций, используя конструкцию языка целевой, например
_≟ₚ_ : ⟦ nat ⇒ nat ⇒ prop ⟧
zero ≟ₚ zero = top
suc n ≟ₚ suc m = n ≟ₚ m
_ ≟ₚ _ = bot
В воображаемом языке мы можем определить коды и соответствующие типы, тем самым образуя замкнутую рефлексивный вселенную (нам необходимо некоторое представление первого порядка типов данных, но это другая история). Но рассмотрим обычное равенство типов:
Eq : ∀ {α β} -> Univ α -> Univ β -> Prop
Как вставить это на языке целевой? Мы можем написать
EqEmb : ⟦ (nat ‵πᵤ‵ λ α → nat ‵πᵤ‵ λ β → univ α ⇒ univ β ⇒ prop) ⟧
но обратите внимание, что целевой язык не содержит ничего о ω. В Eq мы можем шаблон матч на аргументы, как это:
Eq (πᵤ A₁ B₁) (πᵤ A₂ B₂) = ...
α и β оба становятся ω и все в порядке. Но в EqEmb мы не можем сопоставлять рисунок таким образом, потому что в univ αα является номером и не может быть ω, поэтому ⟦ univ α ⟧ никогда не Univ ω.
Предположим, что мы можем сопоставить образец по простым типам Агды. Тогда мы могли бы написать функцию, которая определяет некоторое значение, является ли функция:
isFunction : ∀ {α} {A : Set α} -> A -> Bool
isFunction {A = Π A B} _ = true
isFunction _ = false
Но что, если B является «Вселенная зависит» и есть, скажем, этот тип: ∀ α -> Set α? Затем Π A B имеет тип Setω и α унифицирован с ω. Но если бы мы могли создать экземпляр переменного уровня с ω, то мы могли бы написать такие вещи, как
Id : Set ω
Id = ∀ α -> (A : Set α) -> A -> A
id : Id
id α A x = x
id ω Id id ~> id
Это непредикативный (Хотя я не знаю, приведет ли эта конкретная форма impredicativity к несогласованности. Имеет ли это?).
Таким образом, мы не можем добавить ω в качестве юридического уровня к целевому языку, и мы не можем сопоставлять соответствие Set α при наличии функций, зависящих от «вселенной».Таким образом, «рефлексивный» равенство
EqEmb : ⟦ (nat ‵πᵤ‵ λ α → nat ‵πᵤ‵ λ β → univ α ⇒ univ β ⇒ prop) ⟧
не определен для всех вселенских полиморфных функций (не «Вселенная зависимых»). Например. тип типа из 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).
. Можно ли встроить OTT в себя хорошо типизированным способом? Если нет, можем ли мы как-то обмануть? Можем ли мы сопоставлять совпадение с Set α в присутствии «зависимых от вселенной» функций, таких как все в порядке?