Merge pull request #1 from sourceCode4/containers

Containers

project.agda-lib

@@ -1,4 +1,4 @@
 name: project
-depend: agda2hs
+depend: agda2hs, standard-library
 include: src
 flags: --erase-record-parameters

src/Data/Free.agda

@@ -1,43 +1,43 @@
 module Data.Free where
 
-open import Haskell.Prelude hiding (pure)
 import Haskell.Prelude using (pure)
 import Haskell.Prim.Functor as Functor
+open import Agda.Builtin.Sigma using (_,_)
+open import Haskell.Prelude hiding (pure; _,_)
+open import Data.Container
+open import Level as L
 
-{- Add cases to extend for more functors -}
-data PosFunctor : Set where
-    pList : PosFunctor
-    pMaybe : PosFunctor
+Container00 : Set₁
+Container00 = Container L.zero L.zero
 
-toFunctor : PosFunctor → (Set → Set)
-toFunctor pList = List
-toFunctor pMaybe = Maybe
-
-data Free (F : PosFunctor) (A : Set) : Set where
+data Free (F : Container00) (A : Set) : Set where
     pure : A → Free F A
-    free : toFunctor F (Free F A) → Free F A
+    free : ⟦ F ⟧ (Free F A) → Free F A
 
-iFunctorPosFunctor : (F : PosFunctor) → Functor (toFunctor F)
-iFunctorPosFunctor pList = iFunctorList
-iFunctorPosFunctor pMaybe = iFunctorMaybe
+-- definition of map for Container00 with erased implicit arguments
+cmap : {@0 C : Container00} {@0 A B : Set} → (A → B) → (x : ⟦ C ⟧ A) → ⟦ C ⟧ B
+cmap f (posits , vals) = (posits , f ∘ vals)
 
 instance
     {-# TERMINATING #-}
-    iFunctorFree : {F : PosFunctor} → ⦃ Functor (toFunctor F) ⦄ → Functor (Free F)
+    iFunctorFree : {@0 F : Container00} → ⦃ Functor ⟦ F ⟧ ⦄ → Functor (Free F)
     iFunctorFree .fmap {a = A} {b = B} f = go
         where
-            go : {F : PosFunctor} → {{ Functor (toFunctor F) }} → Free F A → Free F B
+            go : {@0 F : Container00} → ⦃ Functor ⟦ F ⟧ ⦄ → Free F A → Free F B
             go (pure v)   = pure $ f v
             go (free ffa) = free (go <$> ffa)
 
     {-# TERMINATING #-}
-    iApplicativeFree : {F : PosFunctor} → ⦃ Functor (toFunctor F) ⦄ → Applicative (Free F)
-    iApplicativeFree .Applicative.pure  = pure
+    iApplicativeFree : {@0 F : Container00} → ⦃ Functor ⟦ F ⟧ ⦄ → Applicative (Free F)
+    iApplicativeFree .Applicative.pure          = pure
     iApplicativeFree ._<*>_ (pure f) (pure b)   = pure (f b)
     iApplicativeFree ._<*>_ (pure f) (free ffb) = free $ fmap f <$> ffb
     iApplicativeFree ._<*>_ (free ffa) mb       = free $ (_<*> mb) <$> ffa
 
     {-# TERMINATING #-}
-    iMonadFree : {F : PosFunctor} → ⦃ Functor (toFunctor F) ⦄ → Monad (Free F)
+    iMonadFree : {@0 F : Container00} → ⦃ Functor ⟦ F ⟧ ⦄ → Monad (Free F)
     iMonadFree ._>>=_ (pure a)  f = f a
-    iMonadFree ._>>=_ (free fa) f = free (fmap (_>>= f) fa)
+    iMonadFree ._>>=_ (free fa) f = free (fmap (_>>= f) fa)
+
+    iFunctorContainer : {@0 C : Container00} → Functor ⟦ C ⟧
+    iFunctorContainer = record { fmap = cmap }

src/Data/Free/Properties.agda

@@ -1,40 +1,45 @@
 module Data.Free.Properties where
 
+open import Axiom.Extensionality.Propositional
 open import Data.Free
-open import Haskell.Prelude hiding (pure)
+open import Haskell.Prelude hiding (_,_; pure)
+open import Agda.Builtin.Sigma using (_,_)
 open import Equational
+open import Data.Container.Core hiding (map)
+open import Level as L
 
-instance
-    iFunctor_toFunctor : {F : PosFunctor} → Functor (toFunctor F)
-    iFunctor_toFunctor {F = F} = iFunctorPosFunctor F
+postulate extensionality : Extensionality L.zero L.zero
 
-monad-left-id : {F : PosFunctor} → {A B : Set} 
-              → (a : A) → (f : A → Free F B) → (pure a >>= f) ≡ f a
+{- Right identity monad law proof -}
+
+monad-left-id : {F : Container00} {A B : Set}
+              → (a : A) → (f : A → Free F B) → (return a >>= f) ≡ f a 
 monad-left-id a f = refl
 
+{- Right identity monad law proof and its lemmas -}
 
-monad-right-id : {F : PosFunctor} → {A : Set} → (m : Free F A) → m >>= return ≡ m
-fmap-bind-into-return-is-id : {F : PosFunctor} → {A : Set} 
-                            → (fa : (toFunctor F) (Free F A)) → fmap (_>>= return) fa ≡ fa
+monad-right-id : {F : Container00} {A : Set} → (m : Free F A) → m >>= return ≡ m
 
-fmap-bind-into-return-is-id {F = pList} [] = refl
-fmap-bind-into-return-is-id {F = pList} (x ∷ ffa) = 
+bind-into-pure-is-id : {F : Container00} {A : Set} 
+                       ((s , vs) : ⟦ F ⟧ (Free F A)) → (_>>= return) ∘ vs ≡ vs
+bind-into-pure-is-id c@(_ , vs) = 
     begin
-        (x >>= return) ∷ fmap (_>>= return) ffa
-    =⟨ cong (_∷ fmap (_>>= return) ffa) (monad-right-id x) ⟩
-        x ∷ fmap (_>>= return) ffa
-    =⟨ cong (x ∷_) (fmap-bind-into-return-is-id ffa) ⟩
-        x ∷ ffa
+        (λ p → vs p >>= pure)
+    =⟨ extensionality (λ p → monad-right-id (vs p)) ⟩
+        vs
     end
 
-fmap-bind-into-return-is-id {F = pMaybe} Nothing = refl
-fmap-bind-into-return-is-id {F = pMaybe} (Just x) = 
+fmap-bind-into-return-is-id : {F : Container00} {A : Set} 
+                              (fa : ⟦ F ⟧ (Free F A)) → fmap (_>>= return) fa ≡ fa
+fmap-bind-into-return-is-id fa@(s , vs) = 
     begin
-        fmap (_>>= return) (Just x)
-    =⟨⟩
-        Just (x >>= pure)
-    =⟨ cong (λ a → Just a) (monad-right-id x) ⟩
-        (Just x)
+        -- since return is defined as pure I write it direcly
+        fmap (_>>= pure) fa
+    =⟨⟩ -- applying the definition of fmap for containers
+        (s , (_>>= pure) ∘ vs)
+       -- by the above lemma applied to the second position of the pair
+    =⟨ cong (s ,_) (bind-into-pure-is-id fa) ⟩
+        fa
     end
 
 monad-right-id (pure x)  = refl
@@ -45,4 +50,46 @@ monad-right-id (free fa) =
         free fa
     end
 
+{- Associativty monad law proof and its lemmas -}
+
+monad-assoc : {F : Container00} {A B C : Set}
+              (m : Free F A) (g : A → Free F B) (h : B → Free F C) 
+            → (m >>= g) >>= h ≡ m >>= (λ x → g x >>= h)
+
+ext-lemma : {F : Container00} {A B C : Set} 
+            (g : A → Free F B) (h : B → Free F C) ((_ , vs) : ⟦ F ⟧ (Free F A)) 
+          → ∀ x → (λ p → ((vs p) >>= g) >>= h) x ≡ (λ p → (vs p) >>= (λ x → (g x) >>= h)) x
+ext-lemma g h fa@(_ , vs) p = 
+    begin
+        ((vs p) >>= g) >>= h
+    =⟨ monad-assoc (vs p) g h ⟩
+        (vs p) >>= (λ x → (g x) >>= h)
+    end
+
+fmap-bind-lemma : {F : Container00} {A B C : Set}
+                  (fa : ⟦ F ⟧ (Free F A)) (g : A → Free F B) (h : B → Free F C)
+                → fmap (_>>= h) (fmap (_>>= g) fa) ≡ fmap (_>>= (λ x → (g x) >>= h)) fa
+fmap-bind-lemma fa@(s , vs) g h =
+    begin
+{-
+        fmap (_>>= h) (fmap (_>>= g) fa)
+    =⟨⟩
+-}
+        (s , λ p → (vs p >>= g) >>= h)
+    =⟨ cong (s ,_) (extensionality (ext-lemma g h fa)) ⟩
+        (s , λ p → (vs p) >>= (λ x → g x >>= h))
+    =⟨⟩
+        fmap (_>>= (λ x → g x >>= h)) fa
+    end
 
+monad-assoc (pure x) g h = refl
+monad-assoc m@(free fa) g h =
+    begin
+        (free (fmap (_>>= g) fa)) >>= h
+    =⟨⟩
+        free (fmap (_>>= h) (fmap (_>>= g) fa))
+    =⟨ cong free (fmap-bind-lemma fa g h) ⟩
+        free (fmap (_>>= (λ x → g x >>= h)) fa)
+    =⟨⟩
+        (free fa) >>= (λ x → g x >>= h)
+    end