Dans un previous question, j'avais types pour un langage de jouetApprendre à termes avec ascenseur et Setω et occurrences variables dans les expressions
data Type : Set where
Nat : Type
Prp : Type
Je pensais à les interpréter à l'aide d'une union disjointe Type → Set ⊎ Set₁, mais je pensais niveau lifiting serait mieux et a aidé à obtenir
⟦_⟧ₜ : Type → Set₁
⟦ Nat ⟧ₜ = Lift ℕ
⟦ Prp ⟧ₜ = Set
supposons maintenant que ma langue de jouet a des variables et des expressions
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
Puis la sémantique des expressions,
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₁ ⟧ₑ σ))
Je me genre de qu'en général lift (lower x) ≠ x en raison de « niveau rafraîchissant » en raison de lift, mais pourquoi ne peut pas la dernière ligne simplement ⟦ e ⟧ₑ σ ≡ ⟦ e₁ ⟧ₑ σ?
Je dois admettre que c'est la première fois que j'utilise Lift et je n'ai malheureusement pas trouvé de tutoriel/explication dessus --- à part l'idée qu'il incorpore des petits types en grands types, comme indiqué par sa définition.
Depuis que je suis tout aménagé, laissez-moi faire une requête assez particulière.
Avec les égalités standard/dérivés,
-- no quick `deriving Eq' mechanism, yet.
postulate _≟ₜ_ : Decidable {A = Type} _≡_
postulate _≟ᵥ_ : ∀ {t s} → Variable t → Variable s → Bool
Je définis la substitution textuelle sur les expressions,
_[_/_] : ∀ {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 ]
maintenant est la question des occurrences variables dans les expressions.
_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 ⟧ₑ σ
J'ai rencontré des problèmes lors de l'utilisation de l'une ou l'autre définition. En particulier, je ne pouvais même pas définir l'un par rapport à l'autre. Toute aide à ce sujet serait appréciée!
Après some digging around, j'ai essayé
levelOf : Type → Level
levelOf Nat = zero
levelOf Prp = suc zero
New⟦_⟧ₜ : (t : Type) → Set (levelOf t)
New⟦ Nat ⟧ₜ = ℕ
New⟦ Prp ⟧ₜ = Set
Cependant, maintenant je Setω erreurs pour la définition de State ci-dessus! C'est,
-- works fine if i use the risky {-# OPTIONS --type-in-type #-}
NState = {t : Type} → Variable t → New⟦ {!t!} ⟧ₜ
As far as I know, une telle erreur se produit, à peu près, quand on a une mission de niveaux aux univers.
Quelles sont les manigances que je fais inconsciemment pour avoir ce problème?