aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2015-04-24 19:03:18 -0400
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2015-04-24 19:03:18 -0400
commit374045f4a0c4aab339a49c4c4bd3dad7c813bf69 (patch)
tree958685dd89b3bfbcc7c841805829a5a0796c510b
parent26fe1ec59740112c590428bafc49b255249a01cd (diff)
Add Functor and Monad classes
-rw-r--r--B.agda4
-rw-r--r--Prelude/Functor.agda44
-rw-r--r--Prelude/Monad.agda39
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 }