Add Functor and Monad classes

3 files changed, 85 insertions, 2 deletions

diff --git a/B.agda b/B.agda
index 5c73dd4..d6087d8 100644
--- a/B.agda
+++ b/B.agda
@@ -16,10 +16,10 @@ module B where
 open import B.Prelude.Bool public
 open import B.Prelude.BooleanAlgebra public
 open import B.Prelude.Char public
+open import B.Prelude.Eq public
+open import B.Prelude.Functor public
 open import B.Prelude.List public
 open import B.Prelude.Maybe public
 open import B.Prelude.Product public
 open import B.Prelude.String public
 open import B.Prelude.Sum public
-
-open import B.Prelude.Eq public
diff --git a/Prelude/Functor.agda b/Prelude/Functor.agda
new file mode 100644
index 0000000..805aeff
--- /dev/null
+++ b/Prelude/Functor.agda
@@ -0,0 +1,44 @@
+{- Copyright © 1992–2002 The University of Glasgow
+Copyright © 2015 Benjamin Barenblat
+
+Licensed under the Apache License, Version 2.0 (the ‘License’); you may not use
+this file except in compliance with the License.  You may obtain a copy of the
+License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software distributed
+under the License is distributed on an ‘AS IS’ BASIS, WITHOUT WARRANTIES OR
+CONDITIONS OF ANY KIND, either express or implied.  See the License for the
+specific language governing permissions and limitations under the License. -}
+
+module B.Prelude.Functor where
+
+import Category.Monad as Monad
+import Category.Functor
+import Data.List
+import Data.Maybe
+open import Function using (_∘_)
+
+open Category.Functor
+  using (RawFunctor)
+  public
+
+open Category.Functor.RawFunctor ⦃...⦄
+  using (_<$>_)
+  public
+
+instance
+  Functor-List : ∀ {ℓ} → RawFunctor (Data.List.List {ℓ})
+  Functor-List = Monad.RawMonad.rawFunctor Data.List.monad
+
+  Functor-Maybe : ∀ {ℓ} → RawFunctor (Data.Maybe.Maybe {ℓ})
+  Functor-Maybe = Monad.RawMonad.rawFunctor Data.Maybe.monad
+
+  Functor-Function : ∀ {ℓ} {r : Set ℓ} → RawFunctor {ℓ} (λ s → (r → s))
+  Functor-Function {r} =
+    -- I could say _<$>_ = _∘_ here, but that makes type checking much more
+    -- challenging.
+    record { _<$>_ = λ f g → f ∘ g }
+
+  -- TODO: Do proper instance for dependent pairs
diff --git a/Prelude/Monad.agda b/Prelude/Monad.agda
new file mode 100644
index 0000000..657dd55
--- /dev/null
+++ b/Prelude/Monad.agda
@@ -0,0 +1,39 @@
+{- Copyright © 1992–2002 The University of Glasgow
+Copyright © 2015 Benjamin Barenblat
+
+Licensed under the Apache License, Version 2.0 (the ‘License’); you may not use
+this file except in compliance with the License.  You may obtain a copy of the
+License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software distributed
+under the License is distributed on an ‘AS IS’ BASIS, WITHOUT WARRANTIES OR
+CONDITIONS OF ANY KIND, either express or implied.  See the License for the
+specific language governing permissions and limitations under the License. -}
+
+module B.Prelude.Monad where
+
+import Category.Monad
+import Data.List
+import Data.Maybe
+open import Function using (const)
+
+open Category.Monad
+  using (RawMonad)
+  public
+
+open Category.Monad.RawMonad ⦃...⦄
+  using (_>>=_; _>>_; return)
+  public
+
+instance
+  Monad-List : ∀ {ℓ} → RawMonad (Data.List.List {ℓ})
+  Monad-List = Data.List.monad
+
+  Monad-Maybe : ∀ {ℓ} → RawMonad (Data.Maybe.Maybe {ℓ})
+  Monad-Maybe = Data.Maybe.monad
+
+  Monad-Function : ∀ {ℓ} {r : Set ℓ} → RawMonad (λ s → (r → s))
+  Monad-Function {r} = record { return = const {r}
+                              ; _>>=_ = λ f k → λ r → k (f r) r }