
  0 | module Control.Applicative.Indexing
  1 | 
  2 | import Data.Contravariant
  3 | 
  4 | %default total
  5 | 
  6 | 
  7 | public export
  8 | record Indexing {0 k : Type} i f (a : k) where
  9 |   constructor MkIndexing
 10 |   runIndexing : i -> (i, f a)
 11 | 
 12 | 
 13 | public export
 14 | Functor f => Functor (Indexing i f) where
 15 |   map f (MkIndexing g) = MkIndexing (mapSnd (map f) . g)
 16 | 
 17 | public export
 18 | Applicative f => Applicative (Indexing i f) where
 19 |   pure x = MkIndexing $ \i => (i, pure x)
 20 |   MkIndexing mf <*> MkIndexing ma = MkIndexing $ \i =>
 21 |     let (j, ff) = mf i
 22 |         (k, fa) = ma j
 23 |     in (k, ff <*> fa)
 24 | 
 25 | public export
 26 | Contravariant f => Contravariant (Indexing i f) where
 27 |   contramap f (MkIndexing g) = MkIndexing (mapSnd (contramap f) . g)
 28 | 
 29 | 
 30 | public export
 31 | indexing : Num i => ((a -> Indexing i f b) -> s -> Indexing i f t) -> (i -> a -> f b) -> s -> f t
 32 | indexing l fn s = snd $ runIndexing {f} (l (\x => MkIndexing $ \i => (1 + i, fn i x)) s) 0
 33 |