Made Data.Container(.Any/.FreeMonad) safe by splitting out fixed points

CHANGELOG.md

@@ -8,11 +8,11 @@ Highlights
 
 * New module for making system calls during type checking, `Reflection.External`,
   which re-exports `Agda.Builtin.Reflection.External`.
-  
+
 * New predicate for lists that are enumerations their type in
   `Data.List.Relation.Unary.Enumerates`.
-  
-* New weak induction schemes in `Data.Fin.Induction` that allows one to avoid 
+
+* New weak induction schemes in `Data.Fin.Induction` that allows one to avoid
   the complicated use of `Acc`/`inject`/`raise` when proving inductive properties
   over finite sets.
 
@@ -23,7 +23,7 @@ Bug-fixes
   `Function.Metric.(Core/Definitions/Structures/Bundles)`. This module was referred
   to in the documentation of its children but until now was not present.
 
-* Added missing fixity declaration to `_<_` in 
+* Added missing fixity declaration to `_<_` in
   `Relation.Binary.Construct.NonStrictToStrict`.
 
 Non-backwards compatible changes
@@ -35,7 +35,7 @@ Non-backwards compatible changes
   in `Agda.Builtin.Float`, see <https://github.com/agda/agda/pull/4885>.
 
 * The bitwise binary relations on floating-point numbers (`_<_`, `_≈ᵇ_`, `_==_`)
-  have been removed without replacement, as they were deeply unintuitive, 
+  have been removed without replacement, as they were deeply unintuitive,
   e.g., `∀ x → x < -x`.
 
 #### Reflection
@@ -82,13 +82,12 @@ Non-backwards compatible changes
   `--safe` flag.  For a full list of affected modules, refer to the
   relevant [commit](https://github.com/agda/agda-stdlib/pull/1465/files#diff-e1c0e3196e4cea6ff808f5d2906031a7657130e10181516206647b83c7014584R91-R131.)
 
-* In order to keep `Data.Nat.Pseudorandom.LCG` safe, the function
+* In order to maintain the safety of `Data.Nat.Pseudorandom.LCG`, the function
   `stream` that relies on the newly unsafe `Codata` modules has
   been moved to the new module `Data.Nat.Pseudorandom.LCG.Unsafe`.
 
-* In order to avoid the unsafe usage of the `--sized-types` in the
-  `Codata.Musical` directory, the functions `fromMusical` and
-  `toMusical` defined in:
+* In order to maintain the safety of the modules in the `Codata.Musical` directory,
+  the functions `fromMusical` and `toMusical` defined in:
   ```
   Codata.Musical.Colist
   Codata.Musical.Conat
@@ -106,6 +105,10 @@ Non-backwards compatible changes
   ```
   respectively.
 
+* In order to maintain the safety of `Data.Container(.Indexed)`, the greatest fixpoint
+  of containers, `ν`, has been moved from `Data.Container(.Indexed)` to a new module
+  `Data.Container(.Indexed).Fixpoints.Guarded` which also re-exports the least fixpoint.
+
 #### Other
 
 * Replaced existing O(n) implementation of `Data.Nat.Binary.fromℕ` with a new O(log n)
@@ -158,6 +161,16 @@ New modules
   Data.List.Relation.Unary.Enumerates.Setoid.Properties
   ```
 
+* (Unsafe) sized W type:
+  ```
+  Data.W.Sized
+  ```
+
+* (Unsafe) container fixpoints:
+  ```
+  Data.Container.Fixpoints.Sized
+  ```
+
 Other minor additions
 ---------------------
 
@@ -170,7 +183,7 @@ Other minor additions
 * Added new proofs to `Data.Fin.Induction`:
   ```agda
   >-wellFounded   : WellFounded {A = Fin n} _>_
-  
+
   <-weakInduction : P zero      → (∀ i → P (inject₁ i) → P (suc i)) → ∀ i → P i
   >-weakInduction : P (fromℕ n) → (∀ i → P (suc i) → P (inject₁ i)) → ∀ i → P i
   ```

GenerateEverything.hs

@@ -130,9 +130,8 @@ sizedTypesModules = map modToFile
   , "Codata.Stream.Instances"
   , "Codata.Stream.Properties"
   , "Codata.Thunk"
-  , "Data.Container"
-  , "Data.Container.Any"
-  , "Data.Container.FreeMonad"
+  , "Data.Container.Fixpoints.Sized"
+  , "Data.W.Sized"
   , "Data.Nat.PseudoRandom.LCG.Unsafe"
   , "Data.Tree.Binary.Show"
   , "Data.Tree.Rose"

src/Data/Container.agda

@@ -4,14 +4,12 @@
 -- Containers, based on the work of Abbott and others
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --sized-types #-}
+{-# OPTIONS --without-K --safe #-}
 
-module Data.Container where
+open import Level using (Level; _⊔_)
+open import Data.W using (W)
 
-open import Level using (_⊔_)
-open import Codata.M hiding (map)
-open import Data.W
-open import Size
+module Data.Container where
 
 ------------------------------------------------------------------------
 -- Re-exporting content to maintain backwards compatibility
@@ -41,10 +39,18 @@ module Morphism where
   open import Data.Container.Morphism
     using (id; _∘_) public
 
--- The least and greatest fixpoints of a container.
+private
+  variable
+    s p : Level
 
-μ : ∀ {s p} → Container s p → Set (s ⊔ p)
+-- The least fixpoint of a container.
+
+μ : Container s p → Set (s ⊔ p)
 μ = W
 
-ν : ∀ {s p} → Container s p → Set (s ⊔ p)
-ν C = M C ∞
+-- The greatest fixpoint of a container can be found
+-- in `Data.Container.Fixpoints.Guarded` as it relies
+-- on the `guardedness` flag.
+
+-- You can find sized alternatives in `Data.Container.Fixpoints.Sized`
+-- as they rely on the unsafe flag `--sized-types`.

src/Data/Container/Any.agda

@@ -5,7 +5,7 @@
 -- Data.Container.Relation.Unary.Any directly.
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --sized-types #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Data.Container.Any where
 

src/Data/Container/Fixpoints/Guarded.agda

@@ -0,0 +1,27 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Fixpoints for containers - using guardedness
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K --guardedness #-}
+
+module Data.Container.Fixpoints.Guarded where
+
+open import Level using (Level; _⊔_)
+open import Codata.Musical.M using (M)
+open import Data.Container using (Container)
+
+private
+  variable
+    s p : Level
+
+-- The least fixpoint can be found in `Data.Container`
+
+open Data.Container public
+  using (μ)
+
+-- This lives in its own module due to its use of guardedness.
+
+ν : Container s p → Set (s ⊔ p)
+ν C = M C

src/Data/Container/Fixpoints/Sized.agda

@@ -0,0 +1,27 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Sized fixpoints of containers, based on the work of Abbott and others
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --sized-types #-}
+
+module Data.Container.Fixpoints.Sized where
+
+open import Level
+open import Size
+open import Codata.M
+open import Data.W.Sized
+open import Data.Container hiding (μ) public
+
+private
+  variable
+    s p : Level
+
+-- The sized least and greatest fixpoints of a container.
+
+μ : Container s p → Size → Set (s ⊔ p)
+μ = W
+
+ν : Container s p → Size → Set (s ⊔ p)
+ν = M

src/Data/Container/FreeMonad.agda

@@ -4,7 +4,7 @@
 -- The free monad construction on containers
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --sized-types #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Data.Container.FreeMonad where
 
@@ -13,7 +13,7 @@ open import Data.Sum.Base using (inj₁; inj₂ ; [_,_]′)
 open import Data.Product
 open import Data.Container
 open import Data.Container.Combinator using (const; _⊎_)
-open import Data.W
+open import Data.W using (sup)
 open import Category.Monad
 
 infixl 1 _⋆C_

src/Data/Container/Indexed.agda

@@ -7,12 +7,11 @@
 -- (2006/9).
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --guardedness #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Data.Container.Indexed where
 
 open import Level
-open import Codata.Musical.M.Indexed
 open import Data.Product as Prod hiding (map)
 open import Data.W.Indexed
 open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
@@ -37,9 +36,8 @@ I ▷ O = Container I O zero zero
 
 -- The least and greatest fixpoint.
 
-μ ν : ∀ {o c r} {O : Set o} → Container O O c r → Pred O _
+μ : ∀ {o c r} {O : Set o} → Container O O c r → Pred O _
 μ = W
-ν = M
 
 -- An equivalence relation is defined in Data.Container.Indexed.WithK.
 

src/Data/Container/Indexed/Combinator.agda

@@ -4,7 +4,7 @@
 -- Indexed container combinators
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --guardedness #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Data.Container.Indexed.Combinator where
 

src/Data/Container/Indexed/Fixpoints/Guarded.agda

@@ -0,0 +1,30 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Greatest fixpoint for indexed containers - using guardedness
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K --guardedness #-}
+
+module Data.Container.Indexed.Fixpoints.Guarded where
+
+open import Level using (Level; _⊔_)
+open import Codata.Musical.M.Indexed using (M)
+open import Data.Container.Indexed using (Container)
+open import Relation.Unary using (Pred)
+
+private
+  variable
+    o c r : Level
+    O : Set o
+
+
+-- The least fixpoint can be found in `Data.Container`
+
+open Data.Container.Indexed public
+  using (μ)
+
+-- This lives in its own module due to its use of guardedness.
+
+ν : Container O O c r → Pred O _
+ν = M

src/Data/Container/Indexed/FreeMonad.agda

@@ -4,7 +4,7 @@
 -- The free monad construction on indexed containers
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --guardedness #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Data.Container.Indexed.FreeMonad where
 

src/Data/Container/Indexed/WithK.agda

@@ -9,7 +9,7 @@
 -- by Hancock and Hyvernat in "Programming interfaces and basic
 -- topology" (2006).
 
-{-# OPTIONS --with-K --safe --guardedness #-}
+{-# OPTIONS --with-K --safe #-}
 
 module Data.Container.Indexed.WithK where
 

src/Data/W.agda

@@ -9,60 +9,58 @@
 module Data.W where
 
 open import Level
-open import Function
-open import Data.Product hiding (map)
-open import Data.Container.Core hiding (map)
+open import Function.Base using (_$_; _∘_; const)
+open import Data.Product using (_,_; -,_; proj₂)
+open import Data.Container.Core using (Container; ⟦_⟧; Shape; Position; _⇒_; ⟪_⟫)
 open import Data.Container.Relation.Unary.All using (□; all)
-open import Relation.Nullary
-open import Agda.Builtin.Equality
+open import Relation.Nullary using (¬_)
+open import Agda.Builtin.Equality using (_≡_; refl)
+
+private
+  variable
+    s p s₁ s₂ p₁ p₂ ℓ : Level
+    C : Container s p
+    C₁ : Container s₁ p₁
+    C₂ : Container s₂ p₂
 
 -- The family of W-types.
 
-data W {s p} (C : Container s p) : Set (s ⊔ p) where
+data W (C : Container s p) : Set (s ⊔ p) where
   sup : ⟦ C ⟧ (W C) → W C
 
-module _ {s p} {C : Container s p} {s : Shape C} {f : Position C s → W C} where
-
- sup-injective₁ : ∀ {t g} → sup (s , f) ≡ sup (t , g) → s ≡ t
- sup-injective₁ refl = refl
+sup-injective₁ : ∀ {s t : Shape C} {f : Position C s → W C} {g} →
+                 sup (s , f) ≡ sup (t , g) → s ≡ t
+sup-injective₁ refl = refl
 
- -- See also Data.W.WithK.sup-injective₂.
+-- See also Data.W.WithK.sup-injective₂.
 
 -- Projections.
 
-module _ {s p} {C : Container s p} where
-
-  head : W C → Shape C
-  head (sup (x , f)) = x
+head : W C → Shape C
+head (sup (x , f)) = x
 
-  tail : (x : W C) → Position C (head x) → W C
-  tail (sup (x , f)) = f
+tail : (x : W C) → Position C (head x) → W C
+tail (sup (x , f)) = f
 
 -- map
 
-module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
-         (m : C₁ ⇒ C₂) where
-
-  map : W C₁ → W C₂
-  map (sup (x , f)) = sup (⟪ m ⟫ (x , λ p → map (f p)))
+map : (m : C₁ ⇒ C₂) → W C₁ → W C₂
+map m (sup (x , f)) = sup (⟪ m ⟫ (x , λ p → map m (f p)))
 
 -- induction
 
-module _ {s p ℓ} {C : Container s p} (P : W C → Set ℓ)
+module _ (P : W C → Set ℓ)
          (alg : ∀ {t} → □ C P t → P (sup t)) where
 
  induction : (w : W C) → P w
  induction (sup (s , f)) = alg $ all (induction ∘ f)
 
-module _ {s p ℓ} {C : Container s p} (open Container C)
-         {P : Set ℓ} (alg : ⟦ C ⟧ P → P) where
+module _ {P : Set ℓ} (alg : ⟦ C ⟧ P → P) where
 
  foldr : W C → P
  foldr = induction (const P) (alg ∘ -,_ ∘ □.proof)
 
 -- If Position is always inhabited, then W_C is empty.
 
-module _ {s p} {C : Container s p} where
-
-  inhabited⇒empty : (∀ s → Position C s) → ¬ W C
-  inhabited⇒empty b = foldr ((_$ b _) ∘ proj₂)
+inhabited⇒empty : (∀ s → Position C s) → ¬ W C
+inhabited⇒empty b = foldr ((_$ b _) ∘ proj₂)