Update variable policy in style guide (agda#1379)

Author: MatthewDaggitt

fix-whitespace.yaml

@@ -9,4 +9,4 @@ included-files:
 
 excluded-files:
   - "README/Text/Tabular.agda"
-
+  - CHANGELOG.md

notes/style-guide.md

@@ -311,10 +311,26 @@ line of code, indented by two spaces.
 * If there are lots of implicit arguments that are common to a collection
   of proofs they should be extracted by using an anonymous module.
 
-* Implicit of type `Level` and `Set` can be generalized using the keyword
-  `variable`. At the moment the policy is *not* to generalize over any other
-  types to minimize the amount of information that users have to keep in
-  their head concurrently.
+#### Variables
+
+* `Level` and `Set`s can always be generalized using the keyword `variable`.
+
+* A file may only declare variables of other types if those types are used
+  in the definition of the main type that the file concerns itself with.
+  At the moment the policy is *not* to generalize over any other types to
+  minimize the amount of information that users have to keep in their head
+  concurrently.
+
+* Example 1: the main type in `Data.List.Properties` is `List A` where `A : Set a`.
+  Therefore it may declare variables over `Level`, `Set a`, `A`, `List A`. It may
+  not declare variables, for example, over predicates (e.g. `P : Pred A p`) as
+  predicates are not used in the definition of `List`, even though they are used
+  in may list functions such as `filter`.
+
+* Example 2: the main type in `Data.List.Relation.Unary.All` is `All P xs` where
+  `A : Set a`, `P : Pred A p`, `xs : List A`. It therefore may declare variables
+  over `Level`, `Set a`, `A`, `List A`, `Pred A p`. It may not declare, for example,
+  variables of type `Rel` or `Vec`.
 
 ## Naming conventions
 

src/Data/List/Relation/Unary/All.agda

@@ -31,6 +31,9 @@ private
     a b p q r ℓ : Level
     A : Set a
     B : Set b
+    P Q R : Pred A p
+    x : A
+    xs : List A
 
 ------------------------------------------------------------------------
 -- Definitions
@@ -67,89 +70,77 @@ Null = All (λ _ → ⊥)
 ------------------------------------------------------------------------
 -- Operations on All
 
-module _ {P : Pred A p} where
+uncons : All P (x ∷ xs) → P x × All P xs
+uncons (px ∷ pxs) = px , pxs
 
-  uncons : ∀ {x xs} → All P (x ∷ xs) → P x × All P xs
-  uncons (px ∷ pxs) = px , pxs
+head : All P (x ∷ xs) → P x
+head = proj₁ ∘ uncons
 
-  head : ∀ {x xs} → All P (x ∷ xs) → P x
-  head = proj₁ ∘ uncons
+tail : All P (x ∷ xs) → All P xs
+tail = proj₂ ∘ uncons
 
-  tail : ∀ {x xs} → All P (x ∷ xs) → All P xs
-  tail = proj₂ ∘ uncons
+reduce : (f : ∀ {x} → P x → B) → All P xs → List B
+reduce f []         = []
+reduce f (px ∷ pxs) = f px ∷ reduce f pxs
 
-  reduce : (f : ∀ {x} → P x → B) → ∀ {xs} → All P xs → List B
-  reduce f []         = []
-  reduce f (px ∷ pxs) = f px ∷ reduce f pxs
+construct : (f : B → ∃ P) (xs : List B) → ∃ (All P)
+construct f []       = [] , []
+construct f (x ∷ xs) = Prod.zip _∷_ _∷_ (f x) (construct f xs)
 
-  construct : (f : B → ∃ P) (xs : List B) → ∃ (All P)
-  construct f []       = [] , []
-  construct f (x ∷ xs) = Prod.zip _∷_ _∷_ (f x) (construct f xs)
+fromList : (xs : List (∃ P)) → All P (List.map proj₁ xs)
+fromList []              = []
+fromList ((x , p) ∷ xps) = p ∷ fromList xps
 
-  fromList : (xs : List (∃ P)) → All P (List.map proj₁ xs)
-  fromList []              = []
-  fromList ((x , p) ∷ xps) = p ∷ fromList xps
+toList : All P xs → List (∃ P)
+toList pxs = reduce (λ {x} px → x , px) pxs
 
-  toList : ∀ {xs} → All P xs → List (∃ P)
-  toList pxs = reduce (λ {x} px → x , px) pxs
+map : P ⊆ Q → All P ⊆ All Q
+map g []         = []
+map g (px ∷ pxs) = g px ∷ map g pxs
 
-module _ {P : Pred A p} {Q : Pred A q} where
+zipWith : P ∩ Q ⊆ R → All P ∩ All Q ⊆ All R
+zipWith f ([] , [])             = []
+zipWith f (px ∷ pxs , qx ∷ qxs) = f (px , qx) ∷ zipWith f (pxs , qxs)
 
-  map : P ⊆ Q → All P ⊆ All Q
-  map g []         = []
-  map g (px ∷ pxs) = g px ∷ map g pxs
+unzipWith : R ⊆ P ∩ Q → All R ⊆ All P ∩ All Q
+unzipWith f []         = [] , []
+unzipWith f (rx ∷ rxs) = Prod.zip _∷_ _∷_ (f rx) (unzipWith f rxs)
 
-module _ {P : Pred A p} {Q : Pred A q} {R : Pred A r} where
+zip : All P ∩ All Q ⊆ All (P ∩ Q)
+zip = zipWith id
 
-  zipWith : P ∩ Q ⊆ R → All P ∩ All Q ⊆ All R
-  zipWith f ([] , [])             = []
-  zipWith f (px ∷ pxs , qx ∷ qxs) = f (px , qx) ∷ zipWith f (pxs , qxs)
-
-  unzipWith : R ⊆ P ∩ Q → All R ⊆ All P ∩ All Q
-  unzipWith f []         = [] , []
-  unzipWith f (rx ∷ rxs) = Prod.zip _∷_ _∷_ (f rx) (unzipWith f rxs)
-
-module _ {P : Pred A p} {Q : Pred A q} where
-
-  zip : All P ∩ All Q ⊆ All (P ∩ Q)
-  zip = zipWith id
-
-  unzip : All (P ∩ Q) ⊆ All P ∩ All Q
-  unzip = unzipWith id
+unzip : All (P ∩ Q) ⊆ All P ∩ All Q
+unzip = unzipWith id
 
 module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
   open Setoid S renaming (Carrier to C; refl to refl₁)
   open SetoidMembership S
 
-  tabulateₛ : ∀ {xs} → (∀ {x} → x ∈ xs → P x) → All P xs
+  tabulateₛ : (∀ {x} → x ∈ xs → P x) → All P xs
   tabulateₛ {[]}     hyp = []
   tabulateₛ {x ∷ xs} hyp = hyp (here refl₁) ∷ tabulateₛ (hyp ∘ there)
 
-module _ {P : Pred A p} where
-
-  tabulate : ∀ {xs} → (∀ {x} → x ∈ₚ xs → P x) → All P xs
-  tabulate = tabulateₛ (P.setoid A)
+tabulate : (∀ {x} → x ∈ₚ xs → P x) → All P xs
+tabulate = tabulateₛ (P.setoid _)
 
 self : ∀ {xs : List A} → All (const A) xs
 self = tabulate (λ {x} _ → x)
 
 ------------------------------------------------------------------------
 -- (weak) updateAt
 
-module _ {P : Pred A p} where
-
-  infixl 6 _[_]%=_ _[_]≔_
+infixl 6 _[_]%=_ _[_]≔_
 
-  updateAt : ∀ {x xs} → x ∈ₚ xs → (P x → P x) → All P xs → All P xs
-  updateAt () f []
-  updateAt (here refl) f (px ∷ pxs) = f px ∷ pxs
-  updateAt (there i)   f (px ∷ pxs) =   px ∷ updateAt i f pxs
+updateAt : x ∈ₚ xs → (P x → P x) → All P xs → All P xs
+updateAt () f []
+updateAt (here refl) f (px ∷ pxs) = f px ∷ pxs
+updateAt (there i)   f (px ∷ pxs) =   px ∷ updateAt i f pxs
 
-  _[_]%=_ : ∀ {x xs} → All P xs → x ∈ₚ xs → (P x → P x) → All P xs
-  pxs [ i ]%= f = updateAt i f pxs
+_[_]%=_ : All P xs → x ∈ₚ xs → (P x → P x) → All P xs
+pxs [ i ]%= f = updateAt i f pxs
 
-  _[_]≔_ : ∀ {x xs} → All P xs → x ∈ₚ xs → P x → All P xs
-  pxs [ i ]≔ px = pxs [ i ]%= const px
+_[_]≔_ : All P xs → x ∈ₚ xs → P x → All P xs
+pxs [ i ]≔ px = pxs [ i ]%= const px
 
 ------------------------------------------------------------------------
 -- Traversable-like functions
@@ -168,7 +159,7 @@ module _ (p : Level) {A : Set a} {P : Pred A (a ⊔ p)}
   mapA : ∀ {Q : Pred A q} → (Q ⊆ F ∘′ P) → All Q ⊆ (F ∘′ All P)
   mapA f = sequenceA ∘′ map f
 
-  forA : ∀ {Q : Pred A q} {xs} → All Q xs → (Q ⊆ F ∘′ P) → F (All P xs)
+  forA : ∀ {Q : Pred A q} → All Q xs → (Q ⊆ F ∘′ P) → F (All P xs)
   forA qxs f = mapA f qxs
 
 module _ (p : Level) {A : Set a} {P : Pred A (a ⊔ p)}
@@ -184,56 +175,56 @@ module _ (p : Level) {A : Set a} {P : Pred A (a ⊔ p)}
   mapM : ∀ {Q : Pred A q} → (Q ⊆ M ∘′ P) → All Q ⊆ (M ∘′ All P)
   mapM = mapA p App
 
-  forM : ∀ {Q : Pred A q} {xs} → All Q xs → (Q ⊆ M ∘′ P) → M (All P xs)
+  forM : ∀ {Q : Pred A q} → All Q xs → (Q ⊆ M ∘′ P) → M (All P xs)
   forM = forA p App
 
 ------------------------------------------------------------------------
 -- Generalised lookup based on a proof of Any
 
-module _ {P : Pred A p} {Q : Pred A q} where
-
-  lookupAny : ∀ {xs} → All P xs → (i : Any Q xs) → (P ∩ Q) (Any.lookup i)
-  lookupAny (px ∷ pxs) (here qx) = px , qx
-  lookupAny (px ∷ pxs) (there i) = lookupAny pxs i
+lookupAny : All P xs → (i : Any Q xs) → (P ∩ Q) (Any.lookup i)
+lookupAny (px ∷ pxs) (here qx) = px , qx
+lookupAny (px ∷ pxs) (there i) = lookupAny pxs i
 
-module _ {P : Pred A p} {Q : Pred A q} {R : Pred A r} where
+lookupWith : ∀[ P ⇒ Q ⇒ R ] → All P xs → (i : Any Q xs) → R (Any.lookup i)
+lookupWith f pxs i = Prod.uncurry f (lookupAny pxs i)
 
-  lookupWith : ∀[ P ⇒ Q ⇒ R ] → ∀ {xs} → All P xs → (i : Any Q xs) →
-               R (Any.lookup i)
-  lookupWith f pxs i = Prod.uncurry f (lookupAny pxs i)
-
-module _ {P : Pred A p} where
-
-  lookup : ∀ {xs} → All P xs → (∀ {x} → x ∈ₚ xs → P x)
-  lookup pxs = lookupWith (λ { px refl → px }) pxs
+lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x)
+lookup pxs = lookupWith (λ { px refl → px }) pxs
 
 module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
   open Setoid S renaming (sym to sym₁)
   open SetoidMembership S
 
-  lookupₛ : ∀ {xs} → P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x)
+  lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x)
   lookupₛ resp pxs = lookupWith (λ py x=y → resp (sym₁ x=y) py) pxs
 
 ------------------------------------------------------------------------
 -- Properties of predicates preserved by All
 
-module _ {P : Pred A p} where
+all? : Decidable P → Decidable (All P)
+all? p []       = yes []
+all? p (x ∷ xs) = Dec.map′ (uncurry _∷_) uncons (p x ×-dec all? p xs)
+
+universal : Universal P → Universal (All P)
+universal u []       = []
+universal u (x ∷ xs) = u x ∷ universal u xs
 
-  all? : Decidable P → Decidable (All P)
-  all? p []       = yes []
-  all? p (x ∷ xs) = Dec.map′ (uncurry _∷_) uncons (p x ×-dec all? p xs)
+irrelevant : Irrelevant P → Irrelevant (All P)
+irrelevant irr []           []           = P.refl
+irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
+  P.cong₂ _∷_ (irr px₁ px₂) (irrelevant irr pxs₁ pxs₂)
 
-  universal : Universal P → Universal (All P)
-  universal u []       = []
-  universal u (x ∷ xs) = u x ∷ universal u xs
+satisfiable : Satisfiable (All P)
+satisfiable = [] , []
 
-  irrelevant : Irrelevant P → Irrelevant (All P)
-  irrelevant irr []           []           = P.refl
-  irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
-    P.cong₂ _∷_ (irr px₁ px₂) (irrelevant irr pxs₁ pxs₂)
 
-  satisfiable : Satisfiable (All P)
-  satisfiable = [] , []
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 1.4
 
 all = all?
 {-# WARNING_ON_USAGE all