0 | module Control.Lens.OptionalFold
 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.Optional
 8 | import Control.Lens.Getter
 9 |
10 | %default total
11 |
12 |
13 | ------------------------------------------------------------------------------
14 | -- Type definitions
15 | ------------------------------------------------------------------------------
16 |
17 |
18 | public export
19 | record IsOptFold p where
20 |   constructor MkIsOptFold
21 |   runIsOptFold : (Strong p, Choice p, Bicontravariant p)
22 |
23 | export %hint
24 | optFoldToOptional : IsOptFold p => IsOptional p
25 | optFoldToOptional @{MkIsOptFold _} = MkIsOptional %search
26 |
27 | export %hint
28 | optFoldToGetter : IsOptFold p => IsGetter p
29 | optFoldToGetter @{MkIsOptFold _} = MkIsGetter %search
30 |
31 | export %hint
32 | indexedOptFold : IsOptFold p => IsOptFold (Indexed i p)
33 | indexedOptFold @{MkIsOptFold _} = MkIsOptFold %search
34 |
35 |
36 | ||| An `OptionalFold` is a getter that may not return a focus value.
37 | ||| `OptionalFold s a` is equivalent to `s -> Maybe a`.
38 | public export
39 | 0 OptionalFold : (s,a : Type) -> Type
40 | OptionalFold = Simple (Optic IsOptFold)
41 |
42 | ||| An `IndexedOptionalFold` returns an index while getting.
43 | public export
44 | 0 IndexedOptionalFold : (i,s,a : Type) -> Type
45 | IndexedOptionalFold = Simple . IndexedOptic IsOptFold
46 |
47 |
48 | ------------------------------------------------------------------------------
49 | -- Utilities for OptionalFolds
50 | ------------------------------------------------------------------------------
51 |
52 |
53 | ||| Construct an `OptionalFold` from a function.
54 | public export
55 | folding : (s -> Maybe a) -> OptionalFold s a
56 | folding f @{MkIsOptFold _} =
57 |   contrabimap (\x => maybe (Left x) Right (f x)) Left . right
58 |
59 | ||| Construct an `IndexedOptionalFold` from a function.
60 | public export
61 | ifolding : (s -> Maybe (i, a)) -> IndexedOptionalFold i s a
62 | ifolding f @{MkIsOptFold _} @{ind} =
63 |   contrabimap (\x => maybe (Left x) Right (f x)) Left . right . indexed @{ind}
64 |