0 | module Control.Lens.Optional
  1 |
  2 | import Data.Profunctor
  3 | import Control.Lens.Optic
  4 | import Control.Lens.Indexed
  5 | import Control.Lens.Lens
  6 | import Control.Lens.Prism
  7 |
  8 | %default total
  9 |
 10 |
 11 | ------------------------------------------------------------------------------
 12 | -- Type definitions
 13 | ------------------------------------------------------------------------------
 14 |
 15 |
 16 | public export
 17 | record IsOptional p where
 18 |   constructor MkIsOptional
 19 |   runIsOptional : (Strong p, Choice p)
 20 |
 21 | export %hint
 22 | optionalToLens : IsOptional p => IsLens p
 23 | optionalToLens @{MkIsOptional _} = MkIsLens %search
 24 |
 25 | export %hint
 26 | optionalToPrism : IsOptional p => IsPrism p
 27 | optionalToPrism @{MkIsOptional _} = MkIsPrism %search
 28 |
 29 | export %hint
 30 | indexedOptional : IsOptional p => IsOptional (Indexed i p)
 31 | indexedOptional @{MkIsOptional _} = MkIsOptional %search
 32 |
 33 |
 34 | ||| An `Optional` is a lens that may or may not contain the focus value.
 35 | ||| As such, accesses will return a `Maybe` value.
 36 | public export
 37 | 0 Optional : (s,t,a,b : Type) -> Type
 38 | Optional = Optic IsOptional
 39 |
 40 | ||| `Optional'` is the `Simple` version of `Optional`.
 41 | public export
 42 | 0 Optional' : (s,a : Type) -> Type
 43 | Optional' = Simple Optional
 44 |
 45 | ||| An `IndexedOptional` allows access to the index of a focus.
 46 | public export
 47 | 0 IndexedOptional : (i,s,t,a,b : Type) -> Type
 48 | IndexedOptional = IndexedOptic IsOptional
 49 |
 50 | ||| `IndexedOptional'` is the `Simple` version of `IndexedOptional`.
 51 | public export
 52 | 0 IndexedOptional' : (i,s,a : Type) -> Type
 53 | IndexedOptional' = Simple . IndexedOptional
 54 |
 55 |
 56 | ------------------------------------------------------------------------------
 57 | -- Utilities for Optionals
 58 | ------------------------------------------------------------------------------
 59 |
 60 |
 61 | ||| Construct an optional from a projection and a setter function.
 62 | public export
 63 | optional : (s -> Either t a) -> (s -> b -> t) -> Optional s t a b
 64 | optional prj set @{MkIsOptional _} = dimap @{fromStrong}
 65 |   (\s => (prj s, set s))
 66 |   (\(e, f) => either id f e)
 67 |   . first . right
 68 |   where
 69 |     -- arbitrary choice of where to pull profunctor instance from
 70 |     fromStrong : Strong p => Profunctor p
 71 |     fromStrong = %search
 72 |
 73 | ||| Construct a simple optional from a projection and a setter function.
 74 | public export
 75 | optional' : (s -> Maybe a) -> (s -> b -> s) -> Optional s s a b
 76 | optional' prj = optional (\x => maybe (Left x) Right (prj x))
 77 |
 78 | ||| Construct an indexed optional from a projection and a setter function.
 79 | public export
 80 | ioptional : (s -> Either t (i, a)) -> (s -> b -> t) -> IndexedOptional i s t a b
 81 | ioptional prj set @{_} @{ind} = optional prj set . indexed @{ind}
 82 |
 83 | ||| Construct a simple indexed optional from a projection and a setter function.
 84 | public export
 85 | ioptional' : (s -> Maybe (i, a)) -> (s -> b -> s) -> IndexedOptional i s s a b
 86 | ioptional' prj = ioptional (\x => maybe (Left x) Right (prj x))
 87 |
 88 |
 89 | ||| The trivial optic that has no focuses.
 90 | public export
 91 | ignored : IndexedOptional i s s a b
 92 | ignored = ioptional' (const Nothing) const
 93 |
 94 | ||| Construct an `Optional` that can be used to filter the focuses of another
 95 | ||| optic.
 96 | |||
 97 | ||| To be more specific, this optic passes the value through unchanged if it
 98 | ||| satisfies the predicate and returns no values if it does not.
 99 | |||
100 | ||| WARNING: This `Optional` is technically invalid! Its setting capability
101 | ||| should only be used in cases where the focuses that pass the filter aren't
102 | ||| changed.
103 | public export
104 | filtered : (a -> Bool) -> Optional' a a
105 | filtered p = optional' (\x => if p x then Just x else Nothing) (const id)
106 |
107 |
108 | ||| Extract projection and setter functions from an optional.
109 | public export
110 | getOptional : Optional s t a b -> (s -> Either t a, s -> b -> t)
111 | getOptional l = l @{MkIsOptional (strong,choice)} (Right, const id)
112 |   where
113 |     Profunctor (\x,y => (x -> Either y a, x -> b -> y)) where
114 |       dimap f g (prj, set) = (either (Left . g) Right . prj . f, (g .) . set . f)
115 |
116 |     [strong] GenStrong Pair (\x,y => (x -> Either y a, x -> b -> y)) where
117 |       strongl (prj, set) = (\(a,c) => mapFst (,c) (prj a), \(a,c),b => (set a b, c))
118 |       strongr (prj, set) = (\(c,a) => mapFst (c,) (prj a), \(c,a),b => (c, set a b))
119 |
120 |     [choice] GenStrong Either (\x,y => (x -> Either y a, x -> b -> y)) where
121 |       strongl (prj, set) = (either (either (Left . Left) Right . prj) (Left . Right),
122 |                             \e,b => mapFst (`set` b) e)
123 |       strongr (prj, set) = (either (Left . Left) (either (Left . Right) Right . prj),
124 |                             \e,b => mapSnd (`set` b) e)
125 |
126 | ||| Extract projection and setter functions from an optional.
127 | public export
128 | withOptional : Optional s t a b -> ((s -> Either t a) -> (s -> b -> t) -> r) -> r
129 | withOptional l f = uncurry f (getOptional l)
130 |
131 | ||| Retrieve the focus value of an optional, or allow its type to change if there
132 | ||| is no focus.
133 | public export
134 | matching : Optional s t a b -> s -> Either t a
135 | matching = fst . getOptional
136 |
137 |