From 374045f4a0c4aab339a49c4c4bd3dad7c813bf69 Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@mit.edu>
Date: Fri, 24 Apr 2015 19:03:18 -0400
Subject: Add Functor and Monad classes

---
 Prelude/Functor.agda | 44 ++++++++++++++++++++++++++++++++++++++++++++
 Prelude/Monad.agda   | 39 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 83 insertions(+)
 create mode 100644 Prelude/Functor.agda
 create mode 100644 Prelude/Monad.agda

(limited to 'Prelude')

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 }
-- 
cgit v1.2.3