[ fix #693 ] Change the definition of FreeMonad (#1819)

Author: gallais

CHANGELOG.md

@@ -49,6 +49,12 @@ Bug-fixes
   re-exported in their full generality which would lead to unsolved meta variables at
   their use sites.
 
+* In `Data.Container.FreeMonad`, we give a direct definition of `_⋆_` as an inductive
+  type rather than encoding it as an instance of `μ`. This ensures Agda notices that
+  `C ⋆ X` is strictly positive in `X` which in turn allows us to use the free monad
+  when defining auxiliary (co)inductive types (cf. the `Tap` example in
+  `README.Data.Container.FreeMonad`).
+
 * In `Data.Maybe.Base` the fixity declaration of `_<∣>_` was missing. This has been fixed.
 
 Non-backwards compatible changes

README/Data/Container/FreeMonad.agda

@@ -9,20 +9,23 @@
 
 module README.Data.Container.FreeMonad where
 
+open import Level using (0ℓ)
 open import Effect.Monad
 open import Data.Empty
 open import Data.Unit
 open import Data.Bool.Base using (Bool; true)
 open import Data.Nat
 open import Data.Sum using (inj₁; inj₂)
 open import Data.Product renaming (_×_ to _⟨×⟩_)
-open import Data.Container
+open import Data.Container using (Container; _▷_)
 open import Data.Container.Combinator
-open import Data.Container.FreeMonad
+open import Data.Container.FreeMonad as FreeMonad
 open import Data.W
 open import Relation.Binary.PropositionalEquality as P
 
 ------------------------------------------------------------------------
+-- Defining the signature of an effect and building trees describing
+-- computations leveraging that effect.
 
 -- The signature of state and its (generic) operations.
 
@@ -33,29 +36,25 @@ State S = ⊤ ⟶ S ⊎ S ⟶ ⊤
   I ⟶ O = I ▷ λ _ → O
 
 get : ∀ {S} → State S ⋆ S
-get = inn (inj₁ _ , return)
-  where
-  open RawMonad rawMonad
+get = impure (inj₁ _ , pure)
 
 put : ∀ {S} → S → State S ⋆ ⊤
-put s = inn (inj₂ s , return)
-  where
-  open RawMonad rawMonad
+put s = impure (inj₂ s , pure)
 
 -- Using the above we can, for example, write a stateful program that
 -- delivers a boolean.
 prog : State ℕ ⋆ Bool
 prog =
   get         >>= λ n →
   put (suc n) >>
-  return true
+  pure true
   where
-  open RawMonad rawMonad
+  open RawMonad rawMonad using (_>>_)
 
 runState : {S X : Set} → State S ⋆ X → (S → X ⟨×⟩ S)
-runState (sup (inj₁ x , _))        = λ s → x , s
-runState (sup (inj₂ (inj₁ _) , k)) = λ s → runState (k s) s
-runState (sup (inj₂ (inj₂ s) , k)) = λ _ → runState (k _) s
+runState (pure x)                = λ s → x , s
+runState (impure ((inj₁ _) , k)) = λ s → runState (k s) s
+runState (impure ((inj₂ s) , k)) = λ _ → runState (k _) s
 
 test : runState prog 0 ≡ (true , 1)
 test = P.refl
@@ -64,3 +63,56 @@ test = P.refl
 -- could quotient @State S ⋆ X@ by the seven axioms of state (see
 -- Plotkin and Power's "Notions of Computation Determine Monads", 2002)
 -- then we would get the state monad.
+
+------------------------------------------------------------------------
+-- Defining effectful inductive data structures
+
+-- The definition of `C ⋆ A` is strictly positive in `A`, meaning that we
+-- can use `C ⋆_` when defining (co)inductive datatypes.
+
+
+open import Size
+open import Codata.Sized.Thunk
+open import Data.Vec.Base using (Vec; []; _∷_)
+
+
+-- A `Tap C A` is a infinite source of `A`s provided that we can perform
+-- the effectful computations described by `C`.
+-- The first one can be accessed readily but the rest of them is hidden
+-- under layers of `C` computations.
+
+module _ (C : Container 0ℓ 0ℓ) (A : Set 0ℓ) where
+
+  data Tap (i : Size) : Set 0ℓ where
+    _∷_ : A → Thunk (λ i → C ⋆ Tap i) i → Tap i
+
+-- We can run a given tap for a set number of steps and collect the elements
+-- thus generated along the way. This gives us a `C ⋆_` computation of a vector.
+
+module _ {C : Container 0ℓ 0ℓ} {A : Set 0ℓ} where
+
+  take : Tap C A _ → (n : ℕ) → C ⋆ Vec A n
+  take _ 0 = pure []
+  take (x ∷ _) 1 = pure (x ∷ [])
+  take (x ∷ mxs) (suc n) = do
+    xs ← mxs .force
+    rest ← take xs n
+    pure (x ∷ rest)
+
+-- A stream of all the natural numbers starting from a given value is an
+-- example of a tap.
+
+natsFrom : ∀ {i} → State ℕ ⋆ Tap (State ℕ) ℕ i
+natsFrom = let open RawMonad rawMonad using (_>>_) in do
+  n ← get
+  put (suc n)
+  pure (n ∷ λ where .force → natsFrom)
+
+-- We can use `take` to capture an initial segment of the `natsFrom` tap
+-- and, after running the state operations, observe that it does generate
+-- successive numbers.
+
+_ : ∀ k →
+    runState (natsFrom >>= λ ns → take ns 5) k
+  ≡ (k ∷ 1 + k ∷ 2 + k ∷ 3 + k ∷ 4 + k ∷ [] , 5 + k)
+_ = λ k → refl

src/Data/Container/FreeMonad.agda

@@ -8,13 +8,23 @@
 
 module Data.Container.FreeMonad where
 
-open import Level
+open import Level using (Level; _⊔_)
 open import Data.Sum.Base using (inj₁; inj₂ ; [_,_]′)
-open import Data.Product
-open import Data.Container
+open import Data.Product using (_,_; -,_)
+open import Data.Container using (Container; ⟦_⟧; μ)
+open import Data.Container.Relation.Unary.All using (□; all)
 open import Data.Container.Combinator using (const; _⊎_)
-open import Data.W using (sup)
-open import Effect.Monad
+open import Data.W as W using (sup)
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad)
+open import Function.Base as Function using (_$_; _∘_)
+
+variable
+  x y s p ℓ : Level
+  C : Container s p
+  X : Set x
+  Y : Set y
 
 infixl 1 _⋆C_
 infix  1 _⋆_
@@ -29,28 +39,89 @@ infix  1 _⋆_
 -- A useful intuition is to think of containers describing single
 -- operations and the free monad construction over a container and a set
 -- describing a tree of operations as nodes and elements of the set as
--- leafs. If one starts at the root, then any path will pass finitely
+-- leaves. If one starts at the root, then any path will pass finitely
 -- many nodes (operations described by the container) and eventually end
 -- up in a leaf (element of the set) -- hence the Kleene star notation
 -- (the type can be read as a regular expression).
 
+------------------------------------------------------------------------
+-- Type definition
+
+-- The free moand can be defined as the least fixpoint `μ (C ⋆C X)`
+
 _⋆C_ : ∀ {x s p} → Container s p → Set x → Container (s ⊔ x) p
 C ⋆C X = const X ⊎ C
 
-_⋆_ : ∀ {x s p} → Container s p → Set x → Set (x ⊔ s ⊔ p)
-C ⋆ X = μ (C ⋆C X)
+-- However Agda's positivity checker is currently too weak to observe
+-- that `X` is used in a strictly positive manner in `μ (C ⋆C X)` as
+-- demonstrated in #693.
+-- So we provide instead an inductive definition that we prove to be
+-- equivalent to the μ-based one.
+
+data _⋆_ (C : Container s p) (X : Set x) : Set (x ⊔ s ⊔ p) where
+  pure : X → C ⋆ X
+  impure : ⟦ C ⟧ (C ⋆ X) → C ⋆ X
+
+------------------------------------------------------------------------
+-- Equivalent types
+
+-- We can prove that `C ⋆ X` is equivalent to one layer of `C ⋆C X` with
+-- subterms of tyep `C ⋆ X`.
+
+inj : {X : Set x} → ⟦ C ⋆C X ⟧ (C ⋆ X) → C ⋆ X
+inj (inj₁ x , _) = pure x
+inj (inj₂ c , r) = impure (c , r)
+
+out : {X : Set x} → C ⋆ X → ⟦ C ⋆C X ⟧ (C ⋆ X)
+out (pure x) = inj₁ x , λ ()
+out (impure (c , r)) = inj₂ c , r
+
+-- We can fully convert back and forth between `C ⋆ X` and `μ (C ⋆C X)`.
 
-module _ {s p} {C : Container s p} where
+toμ : C ⋆ X → μ (C ⋆C X)
+toμ (pure x) = sup (inj₁ x , λ ())
+toμ (impure (c , r)) = sup (inj₂ c , toμ ∘ r)
+
+fromμ : μ (C ⋆C X) → C ⋆ X
+fromμ = W.foldr inj
+
+-- We can recover an induction principle similar to the one given in `Data.W`.
+-- We curry these ones by distinguishing the pure vs. impure case
+
+module _ (P : C ⋆ X → Set ℓ)
+         (algP : ∀ x → P (pure x))
+         (algI : ∀ {t} → □ C P t → P (impure t)) where
+
+ induction : (t : C ⋆ X) → P t
+ induction (pure x) = algP x
+ induction (impure (c , r)) = algI $ all (induction ∘ r)
+
+module _ {P : Set ℓ}
+         (algP : X → P)
+         (algI : ⟦ C ⟧ P → P) where
+
+ foldr : C ⋆ X → P
+ foldr = induction (Function.const P) algP (algI ∘ -,_ ∘ □.proof)
+
+_<$>_ : (X → Y) → C ⋆ X → C ⋆ Y
+f <$> t = foldr (pure ∘ f) impure t
+
+_<*>_ : C ⋆ (X → Y) → C ⋆ X → C ⋆ Y
+pure f <*> t = f <$> t
+impure (c , r) <*> t = impure (c , λ v → r v <*> t)
+
+_>>=_ : C ⋆ X → (X → C ⋆ Y) → C ⋆ Y
+pure x >>= f = f x
+impure (c , r) >>= f = impure (c , λ v → r v >>= f)
+
+------------------------------------------------------------------------
+-- Structure
 
-  inn : ∀ {x} {X : Set x} → ⟦ C ⟧ (C ⋆ X) → C ⋆ X
-  inn (s , f) = sup (inj₂ s , f)
+rawFunctor : RawFunctor (_⋆_ {x = x} C)
+rawFunctor = record { _<$>_ = _<$>_ }
 
-  rawMonad : ∀ {x} → RawMonad {s ⊔ p ⊔ x} (C ⋆_)
-  rawMonad = record { return = return; _>>=_ = _>>=_ }
-    where
-    return : ∀ {X} → X → C ⋆ X
-    return x = sup (inj₁ x , λ ())
+rawApplicative : {C : Container s p} → RawApplicative (_⋆_ {x = x ⊔ s ⊔ p} C)
+rawApplicative = record { pure = pure ; _⊛_ = _<*>_ }
 
-    _>>=_ : ∀ {X Y} → C ⋆ X → (X → C ⋆ Y) → C ⋆ Y
-    sup (inj₁ x , _) >>= k = k x
-    sup (inj₂ s , f) >>= k = inn (s , λ p → f p >>= k)
+rawMonad : {C : Container s p} → RawMonad (_⋆_ {x = x ⊔ s ⊔ p} C)
+rawMonad = record { return = pure ; _>>=_ = _>>=_ }