Вопрос касается теории наблюдательных типов.
Рассмотрим этот параметр:
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 ω.
Допустим, мы можем сопоставить шаблон с простыми типами Agda. Затем мы могли бы написать функцию, которая определяет, является ли какое-то значение функцией:
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
Это непредсказуемо (хотя я не знаю, приводит ли эта конкретная форма непредсказуемости к несогласованности. Неужели?).
Таким образом, мы не можем добавить ω в качестве юридического уровня к целевому языку, и мы не можем сопоставить шаблон на 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 α при наличии "зависимых от вселенной" функций, как будто все в порядке?
