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

Co-authored-by: Guillaume ALLAIS <[email protected]>

Author: MatthewDaggitt

CHANGELOG.md

@@ -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
@@ -99,6 +98,10 @@ Non-backwards compatible changes
   have been moved to a new module `Codata.Musical.Conversion` and renamed to
   `X.fromMusical` and `X.toMusical` for each of `Codata.Musical.X`.
 
+* 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)
@@ -151,6 +154,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
 ---------------------
 

GenerateEverything.hs

@@ -133,9 +133,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