From e375d008e518393ff1f85a09d7e940a614e89941 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 19 Feb 2023 17:04:57 +0100 Subject: [PATCH] comments etc --- lib/Quox/Equal.idr | 89 +++++++++++++++++++++++++++++++++------- lib/Quox/Syntax/Qty.idr | 3 +- lib/Quox/Typechecker.idr | 9 +++- 3 files changed, 83 insertions(+), 18 deletions(-) diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index 77627a8..c349dfc 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -37,6 +37,11 @@ clashE : CanEqual q m => Elim q d n -> Elim q d n -> m a clashE e f = throwError $ ClashE !mode e f +||| true if a term is syntactically a type, or is neutral. +||| +||| this function *doesn't* push substitutions, because its main use is as a +||| `So` argument to skip cases that are already known to be nonsense. and +||| the substitutions have already been pushed. public export %inline isTyCon : (t : Term {}) -> Bool isTyCon (TYPE {}) = True @@ -67,6 +72,14 @@ sameTyCon (E {}) _ = False parameters (defs : Definitions' q g) + ||| true if a type is known to be a subsingleton purely by its form. + ||| a subsingleton is a type with only zero or one possible values. + ||| equality/subtyping accepts immediately on values of subsingleton types. + ||| + ||| * a function type is a subsingleton if its codomain is. + ||| * a pair type is a subsingleton if both its elements are. + ||| * all equality types are subsingletons because uip is admissible by + ||| boundary separation. private isSubSing : Term q 0 n -> Bool isSubSing ty = @@ -97,6 +110,10 @@ parameters {auto _ : HasErr q m} parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} mutual namespace Term + ||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to + ||| the current variance `mode`. + ||| + ||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠ export covering %inline compare0 : TContext q 0 n -> (ty, s, t : Term q 0 n) -> m () compare0 ctx ty s t = do @@ -106,6 +123,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} tty <- ensureTyCon ty compare0' ctx ty s t + ||| converts an elim "Γ ⊢ e" to "Γ, x ⊢ e x", for comparing with + ||| a lambda "Γ ⊢ λx ⇒ t" that has been converted to "Γ, x ⊢ t". private %inline toLamBody : Elim q d n -> Term q d (S n) toLamBody e = E $ weakE e :@ BVT 0 @@ -119,29 +138,46 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} compare0' ctx (TYPE _) s t = compareType ctx s t compare0' ctx ty@(Pi {arg, res, _}) s t {n} = local {mode := Equal} $ - let ctx' = ctx :< arg - eta : Elim q 0 n -> ScopeTerm q 0 n -> m () - eta e (TUsed b) = compare0 ctx' res.term (toLamBody e) b - eta e (TUnused _) = clashT ty s t - in case (s, t) of + -- Γ, x : A ⊢ s = t : B + -- ----------------------------------------- + -- Γ ⊢ (λx ⇒ s) = (λx ⇒ t) : (π·x : A) → B (Lam _ b1, Lam _ b2) => compare0 ctx' res.term b1.term b2.term - (E e, Lam _ b) => eta e b - (Lam _ b, E e) => eta e b - (E e, E f) => Elim.compare0 ctx e f + + -- Γ, x : A ⊢ s = e x : B + -- ---------------------------------- + -- Γ ⊢ (λx ⇒ s) = e : (π·x : A) → B + (E e, Lam _ b) => eta e b + (Lam _ b, E e) => eta e b + + (E e, E f) => Elim.compare0 ctx e f _ => throwError $ WrongType ty s t + where + ctx' : TContext q 0 (S n) + ctx' = ctx :< arg + + eta : Elim q 0 n -> ScopeTerm q 0 n -> m () + eta e (TUsed b) = compare0 ctx' res.term (toLamBody e) b + eta e (TUnused _) = clashT ty s t compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $ - -- no η (no fst/snd for π ≱ 0), so… - -- [todo] η for π ≥ 0 maybe case (s, t) of + -- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x} + -- ------------------------------------------- + -- Γ ⊢ (s₁,t₁) = (s₂,t₂) : (x : A) × B + -- + -- [todo] η for π ≥ 0 maybe (Pair sFst sSnd, Pair tFst tSnd) => do compare0 ctx fst sFst tFst compare0 ctx (sub1 snd (sFst :# fst)) sSnd tSnd + _ => throwError $ WrongType ty s t - -- ✨ uip ✨ - compare0' _ (Eq {}) _ _ = pure () + compare0' _ (Eq {}) _ _ = + -- ✨ uip ✨ + -- + -- Γ ⊢ e = f : Eq [i ⇒ A] s t + pure () compare0' ctx ty@(E _) s t = do -- a neutral type can only be inhabited by neutral values @@ -150,6 +186,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} E f <- pure t | _ => throwError $ WrongType ty s t Elim.compare0 ctx e f + ||| compares two types, using the current variance `mode` for universes. + ||| fails if they are not types, even if they would happen to be equal. export covering compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m () compareType ctx s t = do @@ -167,22 +205,37 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} (0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) => (0 st : So (sameTyCon s t)) => m () + -- equality is the same as subtyping, except with the + -- "≤" in the TYPE rule being replaced with "=" compareType' ctx (TYPE k) (TYPE l) = + -- 𝓀 ≤ ℓ + -- ---------------------- + -- Γ ⊢ Type 𝓀 <: Type ℓ expectModeU !mode k l compareType' ctx (Pi {qty = sQty, arg = sArg, res = sRes, _}) (Pi {qty = tQty, arg = tArg, res = tRes, _}) = do + -- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂ + -- ---------------------------------------- + -- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂ expectEqualQ sQty tQty local {mode $= flip} $ compareType ctx sArg tArg -- contra compareType (ctx :< sArg) sRes.term tRes.term compareType' ctx (Sig {fst = sFst, snd = sSnd, _}) (Sig {fst = tFst, snd = tSnd, _}) = do + -- Γ ⊢ A₁ <: A₂ Γ, x : A₁ ⊢ B₁ <: B₂ + -- -------------------------------------- + -- Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂ compareType ctx sFst tFst compareType (ctx :< sFst) sSnd.term tSnd.term compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _}) (Eq {ty = tTy, l = tl, r = tr, _}) = do + -- Γ ⊢ A₁‹ε/i› <: A₂‹ε/i› + -- Γ ⊢ l₁ = l₂ : A₁‹𝟎/i› Γ ⊢ r₁ = r₂ : A₁‹𝟏/i› + -- ------------------------------------------------ + -- Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂ compareType ctx sTy.zero tTy.zero compareType ctx sTy.one tTy.one local {mode := Equal} $ do @@ -194,8 +247,9 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} -- has been inlined by whnfD Elim.compare0 ctx e f - ||| assumes the elim is already typechecked! only does the work necessary - ||| to calculate the overall type + ||| performs the minimum work required to recompute the type of an elim. + ||| + ||| ⚠ **assumes the elim is already typechecked.** ⚠ private covering computeElimType : TContext q 0 n -> (e : Elim q 0 n) -> (0 ne : NotRedex defs e) -> @@ -227,6 +281,11 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} namespace Elim -- [fixme] the following code ends up repeating a lot of work in the -- computeElimType calls. the results should be shared better + + ||| compare two eliminations according to the given variance `mode`. + ||| + ||| ⚠ **assumes that they have both been typechecked, and have + ||| equal types.** ⚠ export covering %inline compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m () compare0 ctx e f = @@ -244,6 +303,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} m () -- replace applied equalities with the appropriate end first -- e.g. e : Eq [i ⇒ A] s t ⊢ e 𝟎 = s : A‹𝟎/i› + -- + -- [todo] maybe have typed whnf and do this (and η???) there instead compare0' ctx (e :% K p) f ne nf = compare0 ctx !(replaceEnd ctx e p $ noOr1 ne) f compare0' ctx e (f :% K q) ne nf = diff --git a/lib/Quox/Syntax/Qty.idr b/lib/Quox/Syntax/Qty.idr index e60c4ab..e5ed436 100644 --- a/lib/Quox/Syntax/Qty.idr +++ b/lib/Quox/Syntax/Qty.idr @@ -45,8 +45,7 @@ interface Eq q => IsQty q where compat : Dec2 Compat ||| true if it is ok for this quantity to appear for the - ||| subject of a typing judgement. this is about the - ||| subject reduction stuff in atkey + ||| subject of a typing judgement [@qtt, §2.3]. IsSubj : Pred q isSubj : Dec1 IsSubj zeroIsSubj : IsSubj zero diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr index 067efd8..c875078 100644 --- a/lib/Quox/Typechecker.idr +++ b/lib/Quox/Typechecker.idr @@ -69,6 +69,8 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} -- substitutions. both of them seem like the same amount of work for the -- computer but pushing is less work for the me + ||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ" + ||| ||| `check ctx sg subj ty` checks that in the context `ctx`, the term ||| `subj` has the type `ty`, with quantity `sg`. if so, returns the ||| quantities of all bound variables that it used. @@ -79,12 +81,16 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} let Element subj nc = pushSubsts subj in check' ctx sg subj nc ty - ||| `check0 ctx subj ty` checks a term in a zero context. + ||| "Ψ | Γ ⊢₀ s ⇐ A" + ||| + ||| `check0 ctx subj ty` checks a term (as `check`) in a zero context. export covering %inline check0 : TyContext q d n -> Term q d n -> Term q d n -> m () check0 ctx tm ty = ignore $ check ctx szero tm ty -- the output will always be 𝟎 because the subject quantity is 0 + ||| "Ψ | Γ ⊢ σ · e ⇒ A ⊳ Σ" + ||| ||| `infer ctx sg subj` infers the type of `subj` in the context `ctx`, ||| and returns its type and the bound variables it used. export covering %inline @@ -205,7 +211,6 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} funres <- infer ctx sg fun (qty, argty, res) <- expectPi !ask funres.type -- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂ - -- (σ ⨴ 0 = 0; σ ⨴ π = σ otherwise) argout <- check ctx (subjMult sg qty) arg argty -- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + Σ₂ pure $ InfRes {