В previous question, я имел виды на игрушечном языкеКак добраться до точки с лифтом и Setω и переменными вхождениями в выражениях
data Type : Set where
Nat : Type
Prp : Type
Я думал об их интерпретации с помощью несвязной Type → Set ⊎ Set₁, но думал, что уровень lifiting будет лучше и помогли получить
⟦_⟧ₜ : Type → Set₁
⟦ Nat ⟧ₜ = Lift ℕ
⟦ Prp ⟧ₜ = Set
Теперь предположим, что мой язык игрушка имеет переменные и выражения
data Variable : Type → Set where
x y : ∀ {t} → Variable t
data Expr : Type → Set₁ where
Var : ∀ {t} (v : Variable t) → Expr t -- varaible symbols
: ℕ → Expr Nat -- constant symbols
: Set → Expr Prp
_+_ : (m n : Expr Nat) → Expr Nat -- binary function symbol
_≈_ : (e f : Expr Nat) → Expr Prp -- binary relation symbol
Тогда семантика выражений,
State = ∀ {t} → Variable t → ⟦ t ⟧ₜ
⟦_⟧ₑ : ∀ {t} → Expr t → State → ⟦ t ⟧ₜ
⟦_⟧ₑ (Var v) σ = σ v
⟦_⟧ₑ (q) σ = lift q
⟦_⟧ₑ (p) σ = p
⟦_⟧ₑ (e + e₁) σ = lift $ lower (⟦ e ⟧ₑ σ) +ℕ lower (⟦ e₁ ⟧ₑ σ)
⟦_⟧ₑ (e ≈ e₁) σ = lift (lower (⟦ e ⟧ₑ σ)) ≡ lift (lower (⟦ e₁ ⟧ₑ σ))
я получить вид, что в общем-lift (lower x) ≠ x из-за «уровень освежающим» из-за lift, , но до сих пор почему не последняя строка просто ⟦ e ⟧ₑ σ ≡ ⟦ e₁ ⟧ₑ σ?
Должен признаться, что это мой первый раз, используя Lift и, к сожалению, не нашел учебника/объяснения на нем - помимо идеи, что он встраивает мелкие типы в большие типы, о чем свидетельствует его определение.
Поскольку у меня все сложилось, позвольте мне сделать довольно конкретный запрос.
С стандартных/полученных равенств,
-- no quick `deriving Eq' mechanism, yet.
postulate _≟ₜ_ : Decidable {A = Type} _≡_
postulate _≟ᵥ_ : ∀ {t s} → Variable t → Variable s → Bool
можно определить текстовую подстановку над выражениями,
_[_/_] : ∀ {s t} → Expr t → Variable s → Expr s → Expr t
_[_/_] {s} {t} (Var v) u e with s ≟ₜ t
Var v [ u/e ] | yes refl = if v ≟ᵥ u then e else Var v
Var v [ u/e ] | no ¬p = Var v
n [ v/e ] = n
p [ v/e ] = p
(E + F) [ v/e ] = E [ v/e ] + F [ v/e ]
(E ≈ F) [ v/e ] = E [ v/e ] ≈ F [ v/e ]
В настоящее время является проблема переменных вхождений внутри выражений.
_not-occurs-in₀_ : ∀ {t} → Variable t → Expr t → Set₁
v not-occurs-in₀ E = ∀ {e} → E [ v/e ] ≡ E
_not-occurs-in₁_ : ∀ {t} → Variable t → Expr t → Set₁
v not-occurs-in₁ E = ∀ {e} {σ : State} → ⟦ E [ v/e ] ⟧ₑ σ ≡ ⟦ E ⟧ₑ σ
У меня возникли проблемы с использованием любого определения. В частности, я не мог даже определить один в терминах другого. Любая помощь по этому поводу будет оценена!
После some digging around, я попытался
levelOf : Type → Level
levelOf Nat = zero
levelOf Prp = suc zero
New⟦_⟧ₜ : (t : Type) → Set (levelOf t)
New⟦ Nat ⟧ₜ = ℕ
New⟦ Prp ⟧ₜ = Set
Однако, теперь я получаю Setω ошибки для определения State выше! То есть,
-- works fine if i use the risky {-# OPTIONS --type-in-type #-}
NState = {t : Type} → Variable t → New⟦ {!t!} ⟧ₜ
As far as I know, такая ошибка возникает, грубо говоря, когда есть задание уровней для вселенных.
Какие шениганы я бессознательно делаю, чтобы справиться с этой проблемой?