0 | module Control.Monad.Identity
  1 |
  2 | import Data.Bits
  3 |
  4 | %default total
  5 |
  6 | ||| The identity monad. This monad provides no abilities other than pure
  7 | ||| computation.
  8 | public export
  9 | record Identity (a : Type) where
 10 |   constructor Id
 11 |   runIdentity : a
 12 |
 13 | public export
 14 | Functor Identity where
 15 |     map fn (Id a) = Id (fn a)
 16 |
 17 | public export
 18 | Applicative Identity where
 19 |     pure x = Id x
 20 |     (Id f) <*> (Id g) = Id (f g)
 21 |
 22 | public export
 23 | Monad Identity where
 24 |     (Id x) >>= k = k x
 25 |
 26 | public export
 27 | Foldable Identity where
 28 |   foldr f init (Id x) = f x init
 29 |   foldl f init (Id x) = f init x
 30 |   null _ = False
 31 |   foldlM f init (Id x) = f init x
 32 |   toList (Id x) = [x]
 33 |   foldMap f (Id x) = f x
 34 |
 35 | public export
 36 | Traversable Identity where
 37 |   traverse f (Id x) = Id <$> f x
 38 |
 39 | public export
 40 | Show a => Show (Identity a) where
 41 |   showPrec d (Id x) = showCon d "Id" $ showArg x
 42 |
 43 | public export
 44 | Eq a => Eq (Identity a) where
 45 |   (Id x) == (Id y) = x == y
 46 |
 47 | public export
 48 | Ord a => Ord (Identity a) where
 49 |   compare (Id x) (Id y) = compare x y
 50 |
 51 | -- public export
 52 | -- Enum a => Enum (Identity a) where
 53 | --   toNat (Id x) = toNat x
 54 | --   fromNat n = Id $ fromNat n
 55 | --   pred (Id n) = Id $ pred n
 56 |
 57 | public export
 58 | Semigroup a => Semigroup (Identity a) where
 59 |   (<+>) x y = Id (runIdentity x <+> runIdentity y)
 60 |
 61 | public export
 62 | Monoid a => Monoid (Identity a) where
 63 |   neutral = Id (neutral)
 64 |
 65 | public export
 66 | Num a => Num (Identity a) where
 67 |   Id x + Id y = Id (x + y)
 68 |   Id x * Id y = Id (x * y)
 69 |   fromInteger = Id . fromInteger
 70 |
 71 | public export
 72 | Neg a => Neg (Identity a) where
 73 |   negate (Id x)    = Id (negate x)
 74 |   Id x - Id y = Id (x - y)
 75 |
 76 | public export
 77 | Abs a => Abs (Identity a) where
 78 |   abs (Id x)    = Id (abs x)
 79 |
 80 | public export
 81 | Fractional a => Fractional (Identity a) where
 82 |   recip (Id x)     = Id (recip x)
 83 |   Id x / Id y = Id (x / y)
 84 |
 85 | public export
 86 | Integral a => Integral (Identity a) where
 87 |   Id x `div` Id y = Id (x `div` y)
 88 |   Id x `mod` Id y = Id (x `mod` y)
 89 |
 90 | public export
 91 | Bits a => Bits (Identity a) where
 92 |   Index = Index {a}
 93 |   Id x .&. Id y = Id (x .&. y)
 94 |   Id x .|. Id y = Id (x .|. y)
 95 |   Id x `xor` Id y = Id (x `xor` y)
 96 |   shiftL (Id v) ix = Id (shiftL v ix)
 97 |   shiftR (Id v) ix = Id (shiftR v ix)
 98 |   bit = Id . bit
 99 |   zeroBits = Id zeroBits
100 |   complement (Id v) = Id (complement v)
101 |   oneBits = Id oneBits
102 |   complementBit (Id v) ix = Id (complementBit v ix)
103 |   clearBit (Id v) ix = Id (clearBit v ix)
104 |   testBit (Id v) ix = testBit v ix
105 |   setBit (Id v) ix = Id (setBit v ix)
106 |
107 | public export
108 | FromString a => FromString (Identity a) where
109 |   fromString = Id . fromString
110 |