Use instances for type classes

src/FP/Abstractions/Applicative.agda

@@ -1,15 +1,14 @@
 {-# OPTIONS --without-K --exact-split --safe --no-unicode #-}
 
---https://github.com/pigworker/CS410-16/blob/master/lectures/CS410-Functor.agda
-
 module FP.Abstractions.Applicative where
 
 open import TypeTheory.Universes using (Type; 𝑢; usuc)
-open import TypeTheory.SimpleTypes using (OneL; <>; unit; id; _compose_)
+open import TypeTheory.SimpleTypes using (id)
 open import HoTT.Identity-Types using (refl; _≡_)
 open import FP.Types using (Id)
+open import FP.Abstractions.Functor using (Functor; FunctorId)
 
-record Applicative (F : Type 𝑢 -> Type 𝑢) : Type (usuc 𝑢) where
+record Applicative (F : Type 𝑢 -> Type 𝑢) {{ _ : Functor F }} : Type (usuc 𝑢) where
   field
     -- operations
     pure : forall {A : Type 𝑢} -> A -> F A

src/FP/Abstractions/Functor.agda

@@ -3,13 +3,8 @@
 module FP.Abstractions.Functor where
 
 open import TypeTheory.Universes using (Type; 𝑢; usuc; Universe)
-open import TypeTheory.SimpleTypes using (OneL; <>; unit; id; _compose_; Nat)
-open import TypeTheory.FunctionsProperties using (compose-id; compose-compose)
+open import TypeTheory.SimpleTypes using (OneL; unit; id; _compose_)
 open import HoTT.Identity-Types using (refl; _≡_)
-open import FP.Maybe using (Maybe; map-Maybe; maybe-map-id; maybe-map-compose)
-open import FP.List using (List; []; _cons_; map-List; map-id; map-compose)
-open import FP.Vec using (Vec; vMap; vMap-id; vMap-compose)
-open import FP.Types using (Id; Function)
 
 record Functor (F : Type 𝑢 -> Type 𝑢) : Type (usuc 𝑢) where
   field
@@ -31,38 +26,3 @@ record Functor (F : Type 𝑢 -> Type 𝑢) : Type (usuc 𝑢) where
       -> F A
       -> F OneL
   void = fmap unit
-
-FunctorId : Functor {𝑢} Id
-FunctorId = record
-  { fmap = id
-  ; fmap-id = refl
-  ; fmap-compose = \ f g fa -> refl (g (f fa))
-  }
-
-FunctorMaybe : Functor {𝑢} Maybe
-FunctorMaybe = record
-  { fmap         = map-Maybe
-  ; fmap-id      = maybe-map-id
-  ; fmap-compose = maybe-map-compose
-  }
-
-FunctorList : Functor {𝑢} List
-FunctorList = record
-  { fmap         = map-List
-  ; fmap-id      = map-id
-  ; fmap-compose = map-compose
-  }
-
-FunctorVec : (n : Nat) -> Functor {𝑢} (\ X -> Vec X n )
-FunctorVec n = record
-  { fmap         = vMap
-  ; fmap-id      = vMap-id n
-  ; fmap-compose = vMap-compose n
-  }
-
-FunctorFunction : {X : Type 𝑢} -> Functor {𝑢} (Function X)
-FunctorFunction {X} = record
-  { fmap         = _compose_
-  ; fmap-id      = compose-id
-  ; fmap-compose = compose-compose
-  }

src/FP/Abstractions/Monad.agda

@@ -1,18 +1,13 @@
 {-# OPTIONS --without-K --exact-split --safe --no-unicode #-}
 
---https://github.com/pigworker/CS410-16/blob/master/lectures/CS410-Functor.agda
-
 module FP.Abstractions.Monad where
 
 open import TypeTheory.Universes using (Type; 𝑢; usuc; Universe)
-open import TypeTheory.SimpleTypes using (OneL; <>; unit; id; _compose_)
 open import HoTT.Identity-Types using (refl; _≡_)
-open import FP.Maybe using (Maybe; Just; flatMap-Maybe;
-  maybe-flatMap-just-f; maybe-flatMap-f-just; maybe-flatMap-compose)
-open import FP.List using (List; []; _cons_; map-List ; map-id; map-compose; list; flatMap-List)
-open import TypeTheory.Sum using (_+_)
+open import FP.Abstractions.Applicative using (Applicative)
+open import FP.Abstractions.Functor using (Functor)
 
-record Monad (F : Type 𝑢 -> Type 𝑢) : Type (usuc 𝑢) where
+record Monad (F : Type 𝑢 -> Type 𝑢) {{ _ : Functor F }} {{ _ : Applicative F }} : Type (usuc 𝑢) where
   field
     -- operations
     return : forall {A : Type 𝑢} -> A -> F A
@@ -33,30 +28,3 @@ record Monad (F : Type 𝑢 -> Type 𝑢) : Type (usuc 𝑢) where
   -- derived operations
   _>=>_ : {A B C : Type 𝑢} -> (B -> F C) -> (A -> F B) -> (A -> F C)
   (f >=> g) a = g a >>= f
-
-MonadMaybe : Monad {𝑢} Maybe
-MonadMaybe = record
-  { return = Just
-  ; _>>=_ = flatMap-Maybe
-  ; return-flatmap = maybe-flatMap-just-f
-  ; flatmap-return = maybe-flatMap-f-just
-  ; flatmap-compose = maybe-flatMap-compose
-  }
-
-MonadList : Monad {𝑢} List
-MonadList = record
-  { return = list
-  ; _>>=_ = \ xs f -> flatMap-List f xs
-  ; return-flatmap = {!   !}
-  ; flatmap-return = {!   !}
-  ; flatmap-compose = {!   !}
-  }
-
-MonadEither : (E : Type 𝑢) -> Monad {𝑢} (\ A -> E + A)
-MonadEither E = record
-  { return = {!   !}
-  ; _>>=_ = {!   !}
-  ; return-flatmap = {!   !}
-  ; flatmap-return = {!   !}
-  ; flatmap-compose = {!   !}
-  }

src/FP/Abstractions/Profunctor.agda

@@ -3,14 +3,8 @@
 module FP.Abstractions.Profunctor where
 
 open import TypeTheory.Universes using (Type; 𝑢; usuc; Universe)
-open import TypeTheory.SimpleTypes using (OneL; <>; unit; id; _compose_; _andThen_)
-open import TypeTheory.FunctionsProperties using (function-dimap-id; function-dimap-compose; compose3)
+open import TypeTheory.SimpleTypes using (unit; id; _compose_; _andThen_)
 open import HoTT.Identity-Types using (refl; _≡_)
-open import FP.Maybe using (Maybe; map-Maybe; maybe-map-id; maybe-map-compose)
-open import FP.Abstractions.Contravariant using (Contravariant)
-open import FP.Abstractions.Functor using (Functor)
-open import FP.Kleisli using (Kleisli)
-open import FP.Types using (Function)
 
 record Profunctor (F : Type 𝑢 -> Type 𝑢 -> Type 𝑢) : Type (usuc 𝑢) where
   field
@@ -48,10 +42,3 @@ record Profunctor (F : Type 𝑢 -> Type 𝑢 -> Type 𝑢) : Type (usuc 𝑢) w
         -> (fa : F A A)
         -> contramap id fa ≡ fa
   contramap-id = dimap-id
-
-ProfunctorFunction : Profunctor {𝑢} Function
-ProfunctorFunction = record
-  { dimap         = \ f g h -> compose3 f h g
-  ; dimap-id      = function-dimap-id
-  ; dimap-compose = function-dimap-compose
-  }

src/FP/Either/Instances.agda

@@ -0,0 +1,39 @@
+{-# OPTIONS --without-K --exact-split --safe --no-unicode #-}
+
+module FP.Either.Instances where
+
+open import TypeTheory.Universes using (Type; 𝑢)
+open import TypeTheory.Sum using (_+_)
+open import TypeTheory.SimpleTypes using (Nat; succ; zero; id; _compose_)
+open import FP.List using (List; map-List; map-id; map-compose; list; _<*>_)
+open import FP.Abstractions.Functor using (Functor)
+open import FP.Abstractions.Applicative using (Applicative)
+open import FP.Abstractions.Monad using (Monad)
+
+module _ (E : Type 𝑢) where
+  instance
+    FunctorEither : Functor {𝑢} (\ A -> E + A)
+    FunctorEither = record
+      { fmap         = {!   !}
+      ; fmap-id      = {!   !}
+      ; fmap-compose = {!   !}
+      }
+
+    ApplicativeEither : Applicative {𝑢} (\ A -> E + A)
+    ApplicativeEither = record
+      { pure         = {!   !}
+      ; _<*>_        = {!   !}
+      ; identity     = {!   !}
+      ; composition  = {!   !}
+      ; homomorphism = {!   !}
+      ; interchange  = {!   !}
+      }
+
+    MonadEither : Monad {𝑢} (\ A -> E + A)
+    MonadEither = record
+      { return = {!   !}
+      ; _>>=_ = {!   !}
+      ; return-flatmap = {!   !}
+      ; flatmap-return = {!   !}
+      ; flatmap-compose = {!   !}
+      }

src/FP/Function/Instances.agda

@@ -0,0 +1,26 @@
+{-# OPTIONS --without-K --exact-split --safe --no-unicode #-}
+
+module FP.Function.Instances where
+
+open import TypeTheory.Universes using (Type; 𝑢)
+open import TypeTheory.SimpleTypes using (OneL; <>; unit; id; _compose_; Nat)
+open import TypeTheory.FunctionsProperties using (compose-id; compose-compose)
+open import TypeTheory.FunctionsProperties using (function-dimap-id; function-dimap-compose; compose3)
+open import FP.Types using (Function)
+open import FP.Abstractions.Functor using (Functor)
+open import FP.Abstractions.Profunctor using (Profunctor)
+
+instance
+  FunctorFunction : {X : Type 𝑢} -> Functor {𝑢} (Function X)
+  FunctorFunction {X} = record
+    { fmap         = _compose_
+    ; fmap-id      = compose-id
+    ; fmap-compose = compose-compose
+    }
+
+  ProfunctorFunction : Profunctor {𝑢} Function
+  ProfunctorFunction = record
+    { dimap         = \ f g h -> compose3 f h g
+    ; dimap-id      = function-dimap-id
+    ; dimap-compose = function-dimap-compose
+    }

src/FP/Id/Instances.agda

@@ -0,0 +1,17 @@
+{-# OPTIONS --without-K --exact-split --safe --no-unicode #-}
+
+module FP.Id.Instances where
+
+open import TypeTheory.Universes using (Type; 𝑢)
+open import TypeTheory.SimpleTypes using (id)
+open import HoTT.Identity-Types using (refl)
+open import FP.Abstractions.Functor using (Functor)
+open import FP.Types using (Id)
+
+instance
+  FunctorId : Functor {𝑢} Id
+  FunctorId = record
+    { fmap = id
+    ; fmap-id = refl
+    ; fmap-compose = \ f g fa -> refl (g (f fa))
+    }

src/FP/List/Instances.agda

@@ -0,0 +1,41 @@
+{-# OPTIONS --without-K --exact-split --safe --no-unicode #-}
+
+module FP.List.Instances where
+
+open import TypeTheory.Universes using (Type; 𝑢)
+open import TypeTheory.SimpleTypes using (Nat; succ; zero; id; _compose_)
+open import FP.List using (
+  List;
+  map-List;
+  flatMap-List;
+  map-id; map-compose; list; _<*>_)
+open import FP.Abstractions.Functor using (Functor)
+open import FP.Abstractions.Applicative using (Applicative)
+open import FP.Abstractions.Monad using (Monad)
+
+instance
+  FunctorList : Functor {𝑢} List
+  FunctorList = record
+    { fmap         = map-List
+    ; fmap-id      = map-id
+    ; fmap-compose = map-compose
+    }
+
+  ApplicativeList : Applicative {𝑢} List
+  ApplicativeList = record
+    { pure         = list
+    ; _<*>_        = _<*>_
+    ; identity     = {!   !}
+    ; composition  = {!   !}
+    ; homomorphism = {!   !}
+    ; interchange  = {!   !}
+    }
+
+  MonadList : Monad {𝑢} List
+  MonadList = record
+    { return = list
+    ; _>>=_ = \ xs f -> flatMap-List f xs
+    ; return-flatmap = {!   !}
+    ; flatmap-return = {!   !}
+    ; flatmap-compose = {!   !}
+    }

src/FP/Maybe/Instances.agda

@@ -0,0 +1,43 @@
+{-# OPTIONS --without-K --exact-split --safe --no-unicode #-}
+
+module FP.Maybe.Instances where
+
+open import TypeTheory.Universes using (Type; 𝑢)
+open import TypeTheory.SimpleTypes using (Nat; succ; zero; id; _compose_)
+open import FP.List using (List; map-List; map-id; map-compose; list; _<*>_)
+open import FP.Maybe using (
+  Maybe;
+  map-Maybe; maybe-map-id; maybe-map-compose;
+  Just;
+  flatMap-Maybe;
+  maybe-flatMap-just-f; maybe-flatMap-f-just; maybe-flatMap-compose)
+open import FP.Abstractions.Functor using (Functor)
+open import FP.Abstractions.Applicative using (Applicative)
+open import FP.Abstractions.Monad using (Monad)
+
+instance
+  FunctorMaybe : Functor {𝑢} Maybe
+  FunctorMaybe = record
+    { fmap         = map-Maybe
+    ; fmap-id      = maybe-map-id
+    ; fmap-compose = maybe-map-compose
+    }
+
+  ApplicativeMaybe : Applicative {𝑢} Maybe
+  ApplicativeMaybe = record
+    { pure         = {!   !}
+    ; _<*>_        = {!   !}
+    ; identity     = {!   !}
+    ; composition  = {!   !}
+    ; homomorphism = {!   !}
+    ; interchange  = {!   !}
+    }
+
+  MonadMaybe : Monad {𝑢} Maybe
+  MonadMaybe = record
+    { return = Just
+    ; _>>=_ = flatMap-Maybe
+    ; return-flatmap = maybe-flatMap-just-f
+    ; flatmap-return = maybe-flatMap-f-just
+    ; flatmap-compose = maybe-flatMap-compose
+    }

src/FP/Vec/Instances.agda

@@ -0,0 +1,32 @@
+{-# OPTIONS --without-K --exact-split --safe --no-unicode #-}
+
+module FP.Vec.Instances where
+
+open import TypeTheory.Universes using (Type; 𝑢)
+open import TypeTheory.SimpleTypes using (Nat)
+open import FP.Vec using (Vec; vMap; vMap-id; vMap-compose; vec)
+open import FP.Abstractions.Functor using (Functor)
+open import FP.Abstractions.Applicative using (Applicative)
+
+module _ (n : Nat) where
+  instance
+    FunctorVec : Functor {𝑢} (\ X -> Vec X n )
+    FunctorVec = record
+      { fmap         = vMap
+      ; fmap-id      = vMap-id n
+      ; fmap-compose = vMap-compose n
+      }
+
+instance
+  FunctorVec1 : Functor {𝑢} (\ X -> Vec X 1 )
+  FunctorVec1 = FunctorVec 1
+
+  ApplicativeVec1 : Applicative {𝑢} (\ X -> Vec X 1 )
+  ApplicativeVec1 = record
+    { pure         = vec
+    ; _<*>_        = {!   !}
+    ; identity     = {!   !}
+    ; composition  = {!   !}
+    ; homomorphism = {!   !}
+    ; interchange  = {!   !}
+    }