
  0 | module Control.Effect.Misc
  1 | 
  2 | -- TODO
  3 | -- Some definitions from this file may be later
  4 | -- relocated to more suitable places.
  5 | 
  6 | namespace Functor
  7 |   public export
  8 |   [Id] Functor (\x => x) where
  9 |     map f x = f x
 10 | 
 11 |   %hint public export
 12 |   FunctorId : Functor (\x => x)
 13 |   FunctorId = Functor.Id
 14 | 
 15 |   public export
 16 |   [LeftPair] Functor (, s) where
 17 |     map f (x, y) = (f x, y)
 18 | 
 19 |   %hint public export
 20 |   FunctorLeftPair : Functor (, s)
 21 |   FunctorLeftPair = Functor.LeftPair
 22 | 
 23 | namespace Applicative
 24 |   public export
 25 |   [Id] Applicative (\x => x) where
 26 |     pure x = x
 27 |     f <*> x = f x
 28 | 
 29 |   %hint public export
 30 |   ApplicativeId : Applicative (\x => x)
 31 |   ApplicativeId = Applicative.Id
 32 | 
 33 | namespace Monad
 34 |   public export
 35 |   [Id] Monad (\x => x) where
 36 |     x >>= f = f x
 37 | 
 38 |   %hint public export
 39 |   MonadId : Monad (\x => x)
 40 |   MonadId = Monad.Id
 41 |