0 | module Control.Lens.Getter
  1 |
  2 | import Data.Bicontravariant
  3 | import Data.Profunctor
  4 | import Data.Profunctor.Costrong
  5 | import Control.Lens.Optic
  6 | import Control.Lens.Indexed
  7 | import Control.Lens.Lens
  8 |
  9 | %default total
 10 |
 11 |
 12 | ------------------------------------------------------------------------------
 13 | -- Type definitions
 14 | ------------------------------------------------------------------------------
 15 |
 16 |
 17 | public export
 18 | record IsGetter p where
 19 |   constructor MkIsGetter
 20 |   runIsGetter : (Strong p, Bicontravariant p)
 21 |
 22 | export %hint
 23 | getterToLens : IsGetter p => IsLens p
 24 | getterToLens @{MkIsGetter _} = MkIsLens %search
 25 |
 26 | export %hint
 27 | indexedGetter : IsGetter p => IsGetter (Indexed i p)
 28 | indexedGetter @{MkIsGetter _} = MkIsGetter %search
 29 |
 30 |
 31 | ||| A getter is an optic that only supports getting, not setting.
 32 | |||
 33 | ||| `Getter s a` is equivalent to a simple function `s -> a`.
 34 | public export
 35 | 0 Getter : (s,a : Type) -> Type
 36 | Getter = Simple (Optic IsGetter)
 37 |
 38 | ||| An indexed getter returns an index while getting.
 39 | public export
 40 | 0 IndexedGetter : (i,s,a : Type) -> Type
 41 | IndexedGetter = Simple . IndexedOptic IsGetter
 42 |
 43 |
 44 | ------------------------------------------------------------------------------
 45 | -- Utilities for getters
 46 | ------------------------------------------------------------------------------
 47 |
 48 |
 49 | ||| Construct a getter from a function.
 50 | public export
 51 | to : (s -> a) -> Getter s a
 52 | to f @{MkIsGetter _} = lmap f . rphantom
 53 |
 54 | ||| Construct an indexed getter from a function.
 55 | public export
 56 | ito : (s -> (i, a)) -> IndexedGetter i s a
 57 | ito f @{MkIsGetter _} @{ind} = lmap f . rphantom . indexed @{ind}
 58 |
 59 | ||| Construct a getter that always returns a constant value.
 60 | public export
 61 | like : a -> Getter s a
 62 | like = to . const
 63 |
 64 |
 65 | ||| Access the value of an optic and apply a function to it, returning the result.
 66 | public export
 67 | views : Getter s a -> (a -> r) -> s -> r
 68 | views l = runForget . l . MkForget
 69 |
 70 | ||| Access the focus value of an optic, particularly a `Getter`.
 71 | public export
 72 | view : Getter s a -> s -> a
 73 | view l = views l id
 74 |
 75 | ||| Access the value and index of an optic and apply a function to them,
 76 | ||| returning the result.
 77 | public export
 78 | iviews : IndexedGetter i s a -> (i -> a -> r) -> s -> r
 79 | iviews l = runForget . l @{%search} @{Idxed} . MkForget . uncurry
 80 |
 81 | ||| Access the focus value and index of an optic, particularly a `Getter`.
 82 | public export
 83 | iview : IndexedGetter i s a -> s -> (i, a)
 84 | iview l = runForget $ l @{%search} @{Idxed} $ MkForget id
 85 |
 86 |
 87 | export infixl 8 ^., ^@.
 88 |
 89 | ||| Access the focus value of an optic, particularly a `Getter`.
 90 | |||
 91 | ||| This is the operator form of `view`.
 92 | public export
 93 | (^.) : s -> Getter s a -> a
 94 | (^.) x l = view l x
 95 |
 96 | ||| Access the focus value and index of an optic, particularly a `Getter`.
 97 | |||
 98 | ||| This is the operator form of `iview`.
 99 | public export
100 | (^@.) : s -> IndexedGetter i s a -> (i, a)
101 | (^@.) x l = iview l x
102 |