
  0 | ||| Functors able to read some separate data, the "index".
  1 | |||
  2 | ||| They are expected to obey the laws
  3 | |||   imap g . imap f = imap (\i => g i . f i)
  4 | ||| and
  5 | |||   imap (const id) = id
  6 | |||
  7 | ||| The abbreviation "Ind" could be taken to stand for "Indexed", but
  8 | ||| also for "Independent", to contrast it with the "Dependent"
  9 | ||| versions elsewhere in the library.
 10 | module Data.Functor.Indexed
 11 | 
 12 | 
 13 | import Data.Vect
 14 | 
 15 | export infixr 4 <|$>
 16 | 
 17 | 
 18 | public export
 19 | interface (Functor f) => IndFunctor i f | f where
 20 |   imap : (i -> x -> y) -> f x -> f y
 21 | 
 22 | export
 23 | (<|$>) : (IndFunctor i f) => (i -> x -> y) -> f x -> f y
 24 | (<|$>) = imap
 25 | 
 26 | export
 27 | IndFunctor k (Pair k) where
 28 |   imap f (i, x) = (i, f i x)
 29 | 
 30 | export
 31 | IndFunctor () Maybe where
 32 |   imap f = map (f ())
 33 | 
 34 | export
 35 | IndFunctor Nat List where
 36 |   imap f = inner 0 where
 37 |     inner : Nat -> List x -> List y
 38 |     inner _ [] = []
 39 |     inner i (a::as) = f i a::inner (i+1) as
 40 | 
 41 | export
 42 | IndFunctor (Fin k) (Vect k) where
 43 |   imap _ [] = []
 44 |   imap f (x :: xs) = f FZ x :: imap (f . FS) xs
 45 |