Document everything
This commit is contained in:
parent
fd4eb7dd00
commit
2585e9eb04
|
@ -3,6 +3,8 @@ module Control.Applicative.Backwards
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
|
|
||||||
|
||| Wrap an `Applicative` type constructor so that its actions are executed
|
||||||
|
||| in the opposite order.
|
||||||
public export
|
public export
|
||||||
record Backwards {0 k : Type} (f : k -> Type) a where
|
record Backwards {0 k : Type} (f : k -> Type) a where
|
||||||
constructor MkBackwards
|
constructor MkBackwards
|
||||||
|
|
|
@ -5,46 +5,69 @@ import Control.Lens.Optic
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Type definitions
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
-- This type is trivial and thus really isn't necessary;
|
||||||
|
-- it's only defined and used in order to assist Idris with optic coersion.
|
||||||
public export
|
public export
|
||||||
record IsEquality {0 k,k' : _} (p : k -> k' -> Type) where
|
record IsEquality {0 k,k' : _} (p : k -> k' -> Type) where
|
||||||
constructor MkIsEquality
|
constructor MkIsEquality
|
||||||
|
|
||||||
|
|
||||||
|
||| An `Equality s t a b` is a witness that `(s = a, t = b)` that can be used
|
||||||
|
||| as an optic.
|
||||||
|
|||
|
||||||
|
||| The canonical `Equality` is `id : Equality a b a b`.
|
||||||
|
|||
|
||||||
|
||| An `Equality` can be coerced to any other optic.
|
||||||
public export
|
public export
|
||||||
0 Equality : k -> k' -> k -> k' -> Type
|
0 Equality : k -> k' -> k -> k' -> Type
|
||||||
Equality s t a b = forall p. IsEquality p => p a b -> p s t
|
Equality s t a b = forall p. IsEquality p => p a b -> p s t
|
||||||
|
|
||||||
|
||| An `Equality' s a` is a witness that `s = a` that can be used as an optic.
|
||||||
|
||| This is the `Simple` version of `Equality`.
|
||||||
public export
|
public export
|
||||||
0 Equality' : k -> k -> Type
|
0 Equality' : (s,a : k) -> Type
|
||||||
Equality' = Simple Equality
|
Equality' = Simple Equality
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Utilities for Equality
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
||| Extract the two `Equal` values from an `Equality`.
|
||||||
public export
|
public export
|
||||||
runEq : Equality s t a b -> (s = a, t = b)
|
runEq : Equality s t a b -> (s = a, t = b)
|
||||||
runEq l = (l {p = \x,_ => x = a} Refl,
|
runEq l = (l {p = \x,_ => x = a} Refl,
|
||||||
l {p = \_,y => y = b} Refl)
|
l {p = \_,y => y = b} Refl)
|
||||||
|
|
||||||
|
||| Extract an `Equal` value from an `Equality`.
|
||||||
public export
|
public export
|
||||||
runEq' : Equality s t a b -> s = a
|
runEq' : Equality s t a b -> s = a
|
||||||
runEq' l = l {p = \x,_ => x = a} Refl
|
runEq' l = l {p = \x,_ => x = a} Refl
|
||||||
|
|
||||||
|
|
||||||
public export
|
||| `Equality` is a congruence.
|
||||||
substEq : forall p. Equality s t a b -> p a b a b -> p s t a b
|
|
||||||
substEq {p} l = l {p = \x,y => p x y a b}
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
congEq : forall f,g. Equality s t a b -> Equality (f s) (g t) (f a) (g b)
|
congEq : forall f,g. Equality s t a b -> Equality (f s) (g t) (f a) (g b)
|
||||||
congEq l {p} = l {p = \x,y => p (f x) (g y)}
|
congEq l {p} = l {p = \x,y => p (f x) (g y)}
|
||||||
|
|
||||||
|
||| Symmetry of an `Equality` optic.
|
||||||
public export
|
public export
|
||||||
symEq : Equality s t a b -> Equality b a t s
|
symEq : Equality s t a b -> Equality b a t s
|
||||||
symEq l = case runEq l of (Refl, Refl) => id
|
symEq l = case runEq l of (Refl, Refl) => id
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
refl : Equality a b a b
|
substEq : forall p. Equality s t a b -> p a b a b -> p s t a b
|
||||||
refl = id
|
substEq {p} l = l {p = \x,y => p x y a b}
|
||||||
|
|
||||||
|
|
||||||
|
||| A trivial `Simple Equality`.
|
||||||
|
||| Composing this optic with any other can force it to be a `Simple` optic.
|
||||||
public export
|
public export
|
||||||
simple : Equality' a a
|
simple : Equality' a a
|
||||||
simple = id
|
simple = id
|
||||||
|
|
|
@ -12,6 +12,13 @@ import Control.Lens.Traversal
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Type definitions
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
-- IsFold
|
||||||
|
|
||||||
public export
|
public export
|
||||||
record IsFold p where
|
record IsFold p where
|
||||||
constructor MkIsFold
|
constructor MkIsFold
|
||||||
|
@ -26,15 +33,29 @@ foldToTraversal : IsFold p => IsTraversal p
|
||||||
foldToTraversal @{MkIsFold _} = MkIsTraversal %search
|
foldToTraversal @{MkIsFold _} = MkIsTraversal %search
|
||||||
|
|
||||||
|
|
||||||
|
-- Fold
|
||||||
|
|
||||||
|
||| A fold is a getter that accesses multiple focus elements.
|
||||||
|
||| `Fold s a` is equivalent to `s -> List a`.
|
||||||
public export
|
public export
|
||||||
0 Fold : (s,a : Type) -> Type
|
0 Fold : (s,a : Type) -> Type
|
||||||
Fold s a = Optic IsFold s s a a
|
Fold s a = Optic IsFold s s a a
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Utilities for folds
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
||| Derive a fold from a `Foldable` implementation.
|
||||||
public export
|
public export
|
||||||
folded : Foldable f => Fold (f a) a
|
folded : Foldable f => Fold (f a) a
|
||||||
folded @{_} @{MkIsFold _} = rphantom . wander traverse_
|
folded @{_} @{MkIsFold _} = rphantom . wander traverse_
|
||||||
|
|
||||||
|
||| Construct a fold from an unfolding function.
|
||||||
|
|||
|
||||||
|
||| This function is not total, as it may result in an infinite amount
|
||||||
|
||| of focuses.
|
||||||
public export covering
|
public export covering
|
||||||
unfolded : (s -> Maybe (a, s)) -> Fold s a
|
unfolded : (s -> Maybe (a, s)) -> Fold s a
|
||||||
unfolded coalg @{MkIsFold _} = rphantom . wander loop
|
unfolded coalg @{MkIsFold _} = rphantom . wander loop
|
||||||
|
@ -42,13 +63,15 @@ unfolded coalg @{MkIsFold _} = rphantom . wander loop
|
||||||
loop : Applicative f => (a -> f a) -> s -> f ()
|
loop : Applicative f => (a -> f a) -> s -> f ()
|
||||||
loop f = maybe (pure ()) (uncurry $ \x,y => f x *> loop f y) . coalg
|
loop f = maybe (pure ()) (uncurry $ \x,y => f x *> loop f y) . coalg
|
||||||
|
|
||||||
|
||| Construct a fold from a function into a foldable container.
|
||||||
public export
|
public export
|
||||||
folding : Foldable f => (s -> f a) -> Fold s a
|
folding : Foldable f => (s -> f a) -> Fold s a
|
||||||
folding @{_} f @{MkIsFold _} = rphantom . contramapFst f . wander traverse_
|
folding @{_} f @{MkIsFold _} = rphantom . contramapFst f . wander traverse_
|
||||||
|
|
||||||
|
||| Reverse the order of a fold's focuses.
|
||||||
public export
|
public export
|
||||||
backwards : Fold s a -> Fold s a
|
backwardsFold : Fold s a -> Fold s a
|
||||||
backwards l @{MkIsFold _} = rphantom . wander func
|
backwardsFold l @{MkIsFold _} = rphantom . wander func
|
||||||
where
|
where
|
||||||
traversing : Applicative f => Traversing (Forget (f ()))
|
traversing : Applicative f => Traversing (Forget (f ()))
|
||||||
traversing =
|
traversing =
|
||||||
|
@ -60,83 +83,108 @@ backwards l @{MkIsFold _} = rphantom . wander func
|
||||||
forwards . runForget (l $ MkForget (MkBackwards {f} . ignore . fn))
|
forwards . runForget (l $ MkForget (MkBackwards {f} . ignore . fn))
|
||||||
|
|
||||||
|
|
||||||
|
||| Map each focus of an optic to a monoid value and combine them.
|
||||||
public export
|
public export
|
||||||
foldMapOf : Monoid m => Fold s a -> (a -> m) -> s -> m
|
foldMapOf : Monoid m => Fold s a -> (a -> m) -> s -> m
|
||||||
foldMapOf l = runForget . l . MkForget
|
foldMapOf l = runForget . l . MkForget
|
||||||
|
|
||||||
public export
|
||| Combine the focuses of an optic using the provided function, starting from
|
||||||
foldMapByOf : Fold s a -> (m -> m -> m) -> m -> (a -> m) -> (s -> m)
|
||| the right.
|
||||||
foldMapByOf l fork nil =
|
|
||||||
let _ = MkMonoid @{MkSemigroup fork} nil
|
|
||||||
in foldMapOf l
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
foldrOf : Fold s a -> (a -> acc -> acc) -> acc -> s -> acc
|
foldrOf : Fold s a -> (a -> acc -> acc) -> acc -> s -> acc
|
||||||
foldrOf l = flip . foldMapByOf l (.) id
|
foldrOf l = flip . foldMapOf @{MkMonoid @{MkSemigroup (.)} id} l
|
||||||
|
|
||||||
|
||| Combine the focuses of an optic using the provided function, starting from
|
||||||
|
||| the left.
|
||||||
public export
|
public export
|
||||||
foldlOf : Fold s a -> (acc -> a -> acc) -> acc -> s -> acc
|
foldlOf : Fold s a -> (acc -> a -> acc) -> acc -> s -> acc
|
||||||
foldlOf l = flip . foldMapByOf l (flip (.)) id . flip
|
foldlOf l = flip . foldMapOf @{MkMonoid @{MkSemigroup $ flip (.)} id} l . flip
|
||||||
|
|
||||||
|
||| Combine each focus value of an optic using a monoid structure.
|
||||||
public export
|
public export
|
||||||
concatOf : Monoid m => Fold s m -> s -> m
|
concatOf : Monoid m => Fold s m -> s -> m
|
||||||
concatOf l = foldMapOf l id
|
concatOf l = foldMapOf l id
|
||||||
|
|
||||||
|
||| Evaluate each computation of an optic and discard the results.
|
||||||
public export
|
public export
|
||||||
sequenceOf_ : Applicative f => Fold s (f a) -> s -> f ()
|
sequenceOf_ : Applicative f => Fold s (f a) -> s -> f ()
|
||||||
sequenceOf_ l =
|
sequenceOf_ l =
|
||||||
let _ = MkMonoid @{MkSemigroup (*>)} (pure ())
|
let _ = MkMonoid @{MkSemigroup (*>)} (pure ())
|
||||||
in foldMapOf l ignore
|
in foldMapOf l ignore
|
||||||
|
|
||||||
|
||| Map each focus of an optic to a computation, evaluate those
|
||||||
|
||| computations and discard the results.
|
||||||
public export
|
public export
|
||||||
traverseOf_ : Applicative f => Fold s a -> (a -> f b) -> s -> f ()
|
traverseOf_ : Applicative f => Fold s a -> (a -> f b) -> s -> f ()
|
||||||
traverseOf_ l f =
|
traverseOf_ l f =
|
||||||
let _ = MkMonoid @{MkSemigroup (*>)} (pure ())
|
let _ = MkMonoid @{MkSemigroup (*>)} (pure ())
|
||||||
in foldMapOf l (ignore . f)
|
in foldMapOf l (ignore . f)
|
||||||
|
|
||||||
|
||| A version of `traverseOf_` with the arguments flipped.
|
||||||
public export
|
public export
|
||||||
forOf_ : Applicative f => Fold s a -> s -> (a -> f b) -> f ()
|
forOf_ : Applicative f => Fold s a -> s -> (a -> f b) -> f ()
|
||||||
forOf_ = flip . traverseOf_
|
forOf_ = flip . traverseOf_
|
||||||
|
|
||||||
|
||| The conjunction of an optic containing lazy boolean values.
|
||||||
public export
|
public export
|
||||||
andOf : Fold s (Lazy Bool) -> s -> Bool
|
andOf : Fold s (Lazy Bool) -> s -> Bool
|
||||||
andOf = force .: concatOf @{All}
|
andOf = force .: concatOf @{All}
|
||||||
|
|
||||||
|
||| The disjunction of an optic containing lazy boolean values.
|
||||||
public export
|
public export
|
||||||
orOf : Fold s (Lazy Bool) -> s -> Bool
|
orOf : Fold s (Lazy Bool) -> s -> Bool
|
||||||
orOf = force .: concatOf @{Any}
|
orOf = force .: concatOf @{Any}
|
||||||
|
|
||||||
|
||| Return `True` if all focuses of the optic satisfy the predicate.
|
||||||
public export
|
public export
|
||||||
allOf : Fold s a -> (a -> Bool) -> s -> Bool
|
allOf : Fold s a -> (a -> Bool) -> s -> Bool
|
||||||
allOf = foldMapOf @{All}
|
allOf = foldMapOf @{All}
|
||||||
|
|
||||||
|
||| Return `True` if any focuses of the optic satisfy the predicate.
|
||||||
public export
|
public export
|
||||||
anyOf : Fold s a -> (a -> Bool) -> s -> Bool
|
anyOf : Fold s a -> (a -> Bool) -> s -> Bool
|
||||||
anyOf = foldMapOf @{Any}
|
anyOf = foldMapOf @{Any}
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Accessing folds
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
||| Return `True` if the optic focuses on any values.
|
||||||
public export
|
public export
|
||||||
has : Fold s a -> s -> Bool
|
has : Fold s a -> s -> Bool
|
||||||
has l = anyOf l (const True)
|
has l = anyOf l (const True)
|
||||||
|
|
||||||
|
||| Return `True` if the optic does not focus on any values.
|
||||||
public export
|
public export
|
||||||
hasn't : Fold s a -> s -> Bool
|
hasn't : Fold s a -> s -> Bool
|
||||||
hasn't l = allOf l (const False)
|
hasn't l = allOf l (const False)
|
||||||
|
|
||||||
|
|
||||||
|
||| Access the first focus value of an optic and apply a function to it,
|
||||||
|
||| returning `Nothing` if there are no focuses.
|
||||||
public export
|
public export
|
||||||
previews : Fold s a -> (a -> r) -> s -> Maybe r
|
previews : Fold s a -> (a -> r) -> s -> Maybe r
|
||||||
previews l f = foldMapOf @{MonoidAlternative} l (Just . f)
|
previews l f = foldMapOf @{MonoidAlternative} l (Just . f)
|
||||||
|
|
||||||
|
||| Access the first focus value of an optic, returning `Nothing` if there are
|
||||||
|
||| no focuses.
|
||||||
public export
|
public export
|
||||||
preview : Fold s a -> s -> Maybe a
|
preview : Fold s a -> s -> Maybe a
|
||||||
preview l = foldMapOf @{MonoidAlternative} l Just
|
preview l = foldMapOf @{MonoidAlternative} l Just
|
||||||
|
|
||||||
infixl 8 ^?
|
infixl 8 ^?
|
||||||
|
|
||||||
|
||| Access the first focus value of an optic, returning `Nothing` if there are
|
||||||
|
||| no focuses.
|
||||||
|
|||
|
||||||
|
||| This is the operator form of `preview`.
|
||||||
public export
|
public export
|
||||||
(^?) : s -> Fold s a -> Maybe a
|
(^?) : s -> Fold s a -> Maybe a
|
||||||
(^?) s l = preview l s
|
(^?) s l = preview l s
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
toListOf : Fold s a -> s -> List a
|
toListOf : Fold s a -> s -> List a
|
||||||
toListOf l = foldrOf l (::) []
|
toListOf l = foldrOf l (::) []
|
||||||
|
|
|
@ -9,6 +9,11 @@ import Control.Lens.Lens
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Type definitions
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
record IsGetter p where
|
record IsGetter p where
|
||||||
constructor MkIsGetter
|
constructor MkIsGetter
|
||||||
|
@ -19,26 +24,41 @@ getterToLens : IsGetter p => IsLens p
|
||||||
getterToLens @{MkIsGetter _} = MkIsLens %search
|
getterToLens @{MkIsGetter _} = MkIsLens %search
|
||||||
|
|
||||||
|
|
||||||
|
||| A getter is an optic that only supports getting, not setting.
|
||||||
|
|||
|
||||||
|
||| `Getter s a` is equivalent to a simple function `s -> a`.
|
||||||
public export
|
public export
|
||||||
0 Getter : (s,a : Type) -> Type
|
0 Getter : (s,a : Type) -> Type
|
||||||
Getter = Simple (Optic IsGetter)
|
Getter = Simple (Optic IsGetter)
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Utilities for getters
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
||| Construct a getter from a function.
|
||||||
public export
|
public export
|
||||||
to : (s -> a) -> Getter s a
|
to : (s -> a) -> Getter s a
|
||||||
to f @{MkIsGetter _} = lmap f . rphantom
|
to f @{MkIsGetter _} = lmap f . rphantom
|
||||||
|
|
||||||
|
|
||||||
|
||| Access the value of an optic and apply a function to it, returning the result.
|
||||||
public export
|
public export
|
||||||
views : Getter s a -> (a -> r) -> (s -> r)
|
views : Getter s a -> (a -> r) -> (s -> r)
|
||||||
views l = runForget . l . MkForget
|
views l = runForget . l . MkForget
|
||||||
|
|
||||||
|
||| Access the focus value of an optic, particularly a `Getter`.
|
||||||
public export
|
public export
|
||||||
view : Getter s a -> (s -> a)
|
view : Getter s a -> s -> a
|
||||||
view l = views l id
|
view l = views l id
|
||||||
|
|
||||||
|
|
||||||
infixl 8 ^.
|
infixl 8 ^.
|
||||||
|
|
||||||
|
||| Access the focus value of an optic, particularly a `Getter`.
|
||||||
|
|||
|
||||||
|
||| This is the operator form of `view`.
|
||||||
public export
|
public export
|
||||||
(^.) : s -> Getter s a -> a
|
(^.) : s -> Getter s a -> a
|
||||||
(^.) x l = view l x
|
(^.) x l = view l x
|
||||||
|
|
|
@ -10,22 +10,39 @@ import Control.Lens.Equality
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Type definitions
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
record IsIso p where
|
record IsIso p where
|
||||||
constructor MkIsIso
|
constructor MkIsIso
|
||||||
runIsIso : Profunctor p
|
runIsIso : Profunctor p
|
||||||
|
|
||||||
|
|
||||||
|
||| An `Iso` is an isomorphism family between types. It allows a value to be
|
||||||
|
||| converted or updated across this isomorphism.
|
||||||
public export
|
public export
|
||||||
0 Iso : (s,t,a,b : Type) -> Type
|
0 Iso : (s,t,a,b : Type) -> Type
|
||||||
Iso = Optic IsIso
|
Iso = Optic IsIso
|
||||||
|
|
||||||
|
||| An `Iso'` is an isomorphism family between types. It allows a value to be
|
||||||
|
||| converted or updated across this isomorphism.
|
||||||
|
||| This is the `Simple` version of `Iso`.
|
||||||
public export
|
public export
|
||||||
0 Iso' : (s,a : Type) -> Type
|
0 Iso' : (s,a : Type) -> Type
|
||||||
Iso' = Simple Iso
|
Iso' = Simple Iso
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Utilities for isomorphisms
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
-- Eliminators
|
||||||
|
|
||||||
|
||| Extract the conversion functions from an `Iso`.
|
||||||
public export
|
public export
|
||||||
getIso : Iso s t a b -> (s -> a, b -> t)
|
getIso : Iso s t a b -> (s -> a, b -> t)
|
||||||
getIso l = l @{MkIsIso coexp} (id, id)
|
getIso l = l @{MkIsIso coexp} (id, id)
|
||||||
|
@ -33,109 +50,146 @@ getIso l = l @{MkIsIso coexp} (id, id)
|
||||||
[coexp] Profunctor (\x,y => (x -> a, b -> y)) where
|
[coexp] Profunctor (\x,y => (x -> a, b -> y)) where
|
||||||
dimap f g (f', g') = (f' . f, g . g')
|
dimap f g (f', g') = (f' . f, g . g')
|
||||||
|
|
||||||
|
||| Extract the conversion functions from an `Iso`.
|
||||||
public export
|
public export
|
||||||
withIso : Iso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
|
withIso : Iso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
|
||||||
withIso l f = uncurry f (getIso l)
|
withIso l f = uncurry f (getIso l)
|
||||||
|
|
||||||
public export
|
|
||||||
under : Iso s t a b -> (t -> s) -> (b -> a)
|
|
||||||
under l = let (f,g) = getIso l in (f .) . (. g)
|
|
||||||
|
|
||||||
|
|
||||||
|
-- Constructors
|
||||||
|
|
||||||
|
||| Construct an `Iso` from two inverse functions.
|
||||||
public export
|
public export
|
||||||
iso : (s -> a) -> (b -> t) -> Iso s t a b
|
iso : (s -> a) -> (b -> t) -> Iso s t a b
|
||||||
iso f g @{MkIsIso _} = dimap f g
|
iso f g @{MkIsIso _} = dimap f g
|
||||||
|
|
||||||
|
||| Construct a simple `Iso` from an equivalence.
|
||||||
public export
|
public export
|
||||||
fromEqv : s <=> a -> Iso' s a
|
fromEqv : s <=> a -> Iso' s a
|
||||||
fromEqv (MkEquivalence l r) = iso l r
|
fromEqv (MkEquivalence l r) = iso l r
|
||||||
|
|
||||||
|
||| Invert an isomorphism.
|
||||||
public export
|
public export
|
||||||
from : Iso s t a b -> Iso b a t s
|
from : Iso s t a b -> Iso b a t s
|
||||||
from l @{MkIsIso _} = withIso l (flip dimap)
|
from l @{MkIsIso _} = withIso l (flip dimap)
|
||||||
|
|
||||||
|
|
||||||
|
-- `au`
|
||||||
|
|
||||||
|
||| Based on Epigram's `ala`.
|
||||||
public export
|
public export
|
||||||
au : Functor f => Iso s t a b -> ((b -> t) -> f s) -> f a
|
au : Functor f => Iso s t a b -> ((b -> t) -> f s) -> f a
|
||||||
au l f = withIso l $ \g,h => g <$> f h
|
au l f = withIso l $ \g,h => g <$> f h
|
||||||
|
|
||||||
|
||| Based on Epigram's `ala'`.
|
||||||
public export
|
public export
|
||||||
auf : (Functor f, Functor g) => Iso s t a b -> (f t -> g s) -> f b -> g a
|
auf : (Functor f, Functor g) => Iso s t a b -> (f t -> g s) -> f b -> g a
|
||||||
auf l f x = withIso l $ \g,h => g <$> f (h <$> x)
|
auf l f x = withIso l $ \g,h => g <$> f (h <$> x)
|
||||||
|
|
||||||
|
||| An alias for `au . from`.
|
||||||
public export
|
public export
|
||||||
xplat : Functor f => Iso s t a b -> ((s -> a) -> f b) -> f t
|
xplat : Functor f => Iso s t a b -> ((s -> a) -> f b) -> f t
|
||||||
xplat l f = withIso l $ \g,h => h <$> f g
|
xplat l f = withIso l $ \g,h => h <$> f g
|
||||||
|
|
||||||
|
||| an alias for `auf . from`.
|
||||||
public export
|
public export
|
||||||
xplatf : (Functor f, Functor g) => Iso s t a b -> (f a -> g b) -> f s -> g t
|
xplatf : (Functor f, Functor g) => Iso s t a b -> (f a -> g b) -> f s -> g t
|
||||||
xplatf l f x = withIso l $ \g,h => h <$> f (g <$> x)
|
xplatf l f x = withIso l $ \g,h => h <$> f (g <$> x)
|
||||||
|
|
||||||
|
|
||||||
-- Example Isos
|
||| Update a value under an `Iso`, as opposed to `over` it.
|
||||||
|
||| In other words, this is a convenient alias for `over . from`.
|
||||||
|
public export
|
||||||
|
under : Iso s t a b -> (t -> s) -> (b -> a)
|
||||||
|
under l = let (f,g) = getIso l in (f .) . (. g)
|
||||||
|
|
||||||
|
|
||||||
|
-- Examples of isomorphisms
|
||||||
|
|
||||||
|
||| An "isomorphism" between a function and its result type, assuming that
|
||||||
|
||| the parameter type is inhabited.
|
||||||
public export
|
public export
|
||||||
constant : a -> Iso (a -> b) (a' -> b') b b'
|
constant : a -> Iso (a -> b) (a' -> b') b b'
|
||||||
constant x = iso ($ x) const
|
constant x = iso ($ x) const
|
||||||
|
|
||||||
|
||| Construct an isomorphism given an involution.
|
||||||
public export
|
public export
|
||||||
involuted : (a -> a) -> Iso' a a
|
involuted : (a -> a) -> Iso' a a
|
||||||
involuted f = iso f f
|
involuted f = iso f f
|
||||||
|
|
||||||
|
||| Flipping a function's arguments forms an isomorphism.
|
||||||
public export
|
public export
|
||||||
flipped : Iso (a -> b -> c) (a' -> b' -> c') (b -> a -> c) (b' -> a' -> c')
|
flipped : Iso (a -> b -> c) (a' -> b' -> c') (b -> a -> c) (b' -> a' -> c')
|
||||||
flipped = iso flip flip
|
flipped = iso flip flip
|
||||||
|
|
||||||
|
||| Swapping a symmetric tensor product's parameters is an isomorphism.
|
||||||
public export
|
public export
|
||||||
swapped : Symmetric f => Iso (f a b) (f a' b') (f b a) (f b' a')
|
swapped : Symmetric f => Iso (f a b) (f a' b') (f b a) (f b' a')
|
||||||
swapped = iso swap' swap'
|
swapped = iso swap' swap'
|
||||||
|
|
||||||
|
||| Casting between types forms an isomorphism.
|
||||||
|
||| WARNING: This is only a true isomorphism if casts in both directions are
|
||||||
|
||| lossless and mutually inverse.
|
||||||
public export
|
public export
|
||||||
casted : (Cast s a, Cast b t) => Iso s t a b
|
casted : (Cast s a, Cast b t) => Iso s t a b
|
||||||
casted = iso cast cast
|
casted = iso cast cast
|
||||||
|
|
||||||
|
||| The isomorphism `non x` converts between `Maybe a` and `a` sans the
|
||||||
|
||| element `x`.
|
||||||
|
|||
|
||||||
|
||| This is useful for working with optics whose focus type is `Maybe a`,
|
||||||
|
||| such as `at`.
|
||||||
public export
|
public export
|
||||||
non : Eq a => a -> Iso' (Maybe a) a
|
non : Eq a => a -> Iso' (Maybe a) a
|
||||||
non x = iso (fromMaybe x) (\y => guard (x /= y) $> y)
|
non x = iso (fromMaybe x) (\y => guard (x /= y) $> y)
|
||||||
|
|
||||||
|
|
||||||
-- Mapping
|
-- Mapping
|
||||||
|
|
||||||
|
||| Lift an isomorphism through a `Functor`.
|
||||||
public export
|
public export
|
||||||
mapping : (Functor f, Functor g) => Iso s t a b -> Iso (f s) (g t) (f a) (g b)
|
mapping : (Functor f, Functor g) => Iso s t a b -> Iso (f s) (g t) (f a) (g b)
|
||||||
mapping l = withIso l $ \f,g => iso (map f) (map g)
|
mapping l = withIso l $ \f,g => iso (map f) (map g)
|
||||||
|
|
||||||
|
||| Lift an isomorphism through a `Contravariant` functor.
|
||||||
public export
|
public export
|
||||||
contramapping : (Contravariant f, Contravariant g) => Iso s t a b -> Iso (f a) (g b) (f s) (g t)
|
contramapping : (Contravariant f, Contravariant g) => Iso s t a b -> Iso (f a) (g b) (f s) (g t)
|
||||||
contramapping l = withIso l $ \f,g => iso (contramap f) (contramap g)
|
contramapping l = withIso l $ \f,g => iso (contramap f) (contramap g)
|
||||||
|
|
||||||
|
||| Lift isomorphisms through a `Bifunctor`.
|
||||||
public export
|
public export
|
||||||
bimapping : (Bifunctor f, Bifunctor g) => Iso s t a b -> Iso s' t' a' b' ->
|
bimapping : (Bifunctor f, Bifunctor g) => Iso s t a b -> Iso s' t' a' b' ->
|
||||||
Iso (f s s') (g t t') (f a a') (g b b')
|
Iso (f s s') (g t t') (f a a') (g b b')
|
||||||
bimapping l r = withIso l $ \f,g => withIso r $ \f',g' =>
|
bimapping l r = withIso l $ \f,g => withIso r $ \f',g' =>
|
||||||
iso (bimap f f') (bimap g g')
|
iso (bimap f f') (bimap g g')
|
||||||
|
|
||||||
|
||| Lift an isomorphism through the first parameter of a `Bifunctor`.
|
||||||
public export
|
public export
|
||||||
mappingFst : (Bifunctor f, Bifunctor g) => Iso s t a b ->
|
mappingFst : (Bifunctor f, Bifunctor g) => Iso s t a b ->
|
||||||
Iso (f s x) (g t y) (f a x) (g b y)
|
Iso (f s x) (g t y) (f a x) (g b y)
|
||||||
mappingFst l = withIso l $ \f,g => iso (mapFst f) (mapFst g)
|
mappingFst l = withIso l $ \f,g => iso (mapFst f) (mapFst g)
|
||||||
|
|
||||||
|
||| Lift an isomorphism through the second parameter of a `Bifunctor`.
|
||||||
public export
|
public export
|
||||||
mappingSnd : (Bifunctor f, Bifunctor g) => Iso s t a b ->
|
mappingSnd : (Bifunctor f, Bifunctor g) => Iso s t a b ->
|
||||||
Iso (f x s) (g y t) (f x a) (g y b)
|
Iso (f x s) (g y t) (f x a) (g y b)
|
||||||
mappingSnd l = withIso l $ \f,g => iso (mapSnd f) (mapSnd g)
|
mappingSnd l = withIso l $ \f,g => iso (mapSnd f) (mapSnd g)
|
||||||
|
|
||||||
|
||| Lift isomorphisms through a `Profunctor`.
|
||||||
public export
|
public export
|
||||||
dimapping : (Profunctor f, Profunctor g) => Iso s t a b -> Iso s' t' a' b' ->
|
dimapping : (Profunctor f, Profunctor g) => Iso s t a b -> Iso s' t' a' b' ->
|
||||||
Iso (f a s') (g b t') (f s a') (g t b')
|
Iso (f a s') (g b t') (f s a') (g t b')
|
||||||
dimapping l r = withIso l $ \f,g => withIso r $ \f',g' =>
|
dimapping l r = withIso l $ \f,g => withIso r $ \f',g' =>
|
||||||
iso (dimap f f') (dimap g g')
|
iso (dimap f f') (dimap g g')
|
||||||
|
|
||||||
|
||| Lift an isomorphism through the first parameter of a `Profunctor`.
|
||||||
public export
|
public export
|
||||||
lmapping : (Profunctor f, Profunctor g) => Iso s t a b ->
|
lmapping : (Profunctor f, Profunctor g) => Iso s t a b ->
|
||||||
Iso (f a x) (g b y) (f s x) (g t y)
|
Iso (f a x) (g b y) (f s x) (g t y)
|
||||||
lmapping l = withIso l $ \f,g => iso (lmap f) (lmap g)
|
lmapping l = withIso l $ \f,g => iso (lmap f) (lmap g)
|
||||||
|
|
||||||
|
||| Lift an isomorphism through the second parameter of a `Profunctor`.
|
||||||
public export
|
public export
|
||||||
rmapping : (Profunctor f, Profunctor g) => Iso s t a b ->
|
rmapping : (Profunctor f, Profunctor g) => Iso s t a b ->
|
||||||
Iso (f x s) (g y t) (f x a) (g y b)
|
Iso (f x s) (g y t) (f x a) (g y b)
|
||||||
|
|
|
@ -9,6 +9,11 @@ import Control.Lens.Iso
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Type definitions
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
record IsLens p where
|
record IsLens p where
|
||||||
constructor MkIsLens
|
constructor MkIsLens
|
||||||
|
@ -19,19 +24,45 @@ lensToIso : IsLens p => IsIso p
|
||||||
lensToIso @{MkIsLens _} = MkIsIso %search
|
lensToIso @{MkIsLens _} = MkIsIso %search
|
||||||
|
|
||||||
|
|
||||||
|
||| A *lens* is a functional reference to a value within a larger data structure.
|
||||||
|
||| Lenses allow one to access or modify the value that they reference, called
|
||||||
|
||| the "focus" or "focus element".
|
||||||
|
|||
|
||||||
|
||| For example, the lens `fst_` from `Data.Tuple.Lens` focuses on the first
|
||||||
|
||| element of a pair. It has the type:
|
||||||
|
|||
|
||||||
|
||| ```idris
|
||||||
|
||| fst_ : Lens (a, c) (b, c) a b
|
||||||
|
||| ```
|
||||||
|
|||
|
||||||
|
||| The types `s, t` correspond to the type of the outside data structure, and
|
||||||
|
||| `a, b` correspond to the type of the focus element. Two of each type is
|
||||||
|
||| provided to allow for operations that change the type of the focus.
|
||||||
public export
|
public export
|
||||||
0 Lens : (s,t,a,b : Type) -> Type
|
0 Lens : (s,t,a,b : Type) -> Type
|
||||||
Lens = Optic IsLens
|
Lens = Optic IsLens
|
||||||
|
|
||||||
|
||| `Lens'` is the `Simple` version of `Lens`.
|
||||||
public export
|
public export
|
||||||
0 Lens' : (s,a : Type) -> Type
|
0 Lens' : (s,a : Type) -> Type
|
||||||
Lens' = Simple Lens
|
Lens' = Simple Lens
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Utilities for lenses
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
||| Construct a lens given getter and setter functions.
|
||||||
|
|||
|
||||||
|
||| @ get The getter function
|
||||||
|
||| @ set The setter function, where the first argument is the data structure
|
||||||
|
||| to modify and the second argument is the new focus value
|
||||||
public export
|
public export
|
||||||
lens : (s -> a) -> (s -> b -> t) -> Lens s t a b
|
lens : (get : s -> a) -> (set : s -> b -> t) -> Lens s t a b
|
||||||
lens get set @{MkIsLens _} = dimap (\x => (x, get x)) (uncurry set) . second
|
lens get set @{MkIsLens _} = dimap (\x => (x, get x)) (uncurry set) . second
|
||||||
|
|
||||||
|
||| Extract getter and setter functions from a lens.
|
||||||
public export
|
public export
|
||||||
getLens : Lens s t a b -> (s -> a, s -> b -> t)
|
getLens : Lens s t a b -> (s -> a, s -> b -> t)
|
||||||
getLens l = l @{MkIsLens strong} (id, const id)
|
getLens l = l @{MkIsLens strong} (id, const id)
|
||||||
|
@ -43,21 +74,28 @@ getLens l = l @{MkIsLens strong} (id, const id)
|
||||||
strongl (get, set) = (get . fst, \(a,c),b => (set a b, c))
|
strongl (get, set) = (get . fst, \(a,c),b => (set a b, c))
|
||||||
strongr (get, set) = (get . snd, \(c,a),b => (c, set a b))
|
strongr (get, set) = (get . snd, \(c,a),b => (c, set a b))
|
||||||
|
|
||||||
|
||| Extract getter and setter functions from a lens.
|
||||||
public export
|
public export
|
||||||
withLens : Lens s t a b -> ((s -> a) -> (s -> b -> t) -> r) -> r
|
withLens : Lens s t a b -> ((s -> a) -> (s -> b -> t) -> r) -> r
|
||||||
withLens l f = uncurry f (getLens l)
|
withLens l f = uncurry f (getLens l)
|
||||||
|
|
||||||
|
|
||||||
|
||| `Void` vacuously "contains" a value of any other type.
|
||||||
public export
|
public export
|
||||||
devoid : Lens Void Void a b
|
devoid : Lens Void Void a b
|
||||||
devoid @{MkIsLens _} = dimap absurd snd . first
|
devoid @{MkIsLens _} = dimap absurd snd . first
|
||||||
|
|
||||||
|
||| All values contain a unit.
|
||||||
public export
|
public export
|
||||||
united : Lens' a ()
|
united : Lens' a ()
|
||||||
united @{MkIsLens _} = dimap ((),) snd . first
|
united @{MkIsLens _} = dimap ((),) snd . first
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
||| Optimize a composition of optics by fusing their uses of `dimap` into one.
|
||||||
|
|||
|
||||||
|
||| This function exploits the Yoneda lemma. `fusing (a . b)` is essentially
|
||||||
|
||| equivalent to `a . b`, but the former will only call `dimap` once.
|
||||||
public export
|
public export
|
||||||
fusing : IsIso p => Optic' (Yoneda p) s t a b -> Optic' p s t a b
|
fusing : IsIso p => Optic' (Yoneda p) s t a b -> Optic' p s t a b
|
||||||
fusing @{MkIsIso _} l = proextract . l . propure
|
fusing @{MkIsIso _} l = proextract . l . propure
|
||||||
|
|
|
@ -7,6 +7,12 @@ import Control.Lens.Prism
|
||||||
|
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Type definitions
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
record IsOptional p where
|
record IsOptional p where
|
||||||
constructor MkIsOptional
|
constructor MkIsOptional
|
||||||
|
@ -21,15 +27,24 @@ optionalToPrism : IsOptional p => IsPrism p
|
||||||
optionalToPrism @{MkIsOptional _} = MkIsPrism %search
|
optionalToPrism @{MkIsOptional _} = MkIsPrism %search
|
||||||
|
|
||||||
|
|
||||||
|
||| An `Optional` is a lens that may or may not contain the focus value.
|
||||||
|
||| As such, accesses will return a `Maybe` value.
|
||||||
public export
|
public export
|
||||||
0 Optional : (s,t,a,b : Type) -> Type
|
0 Optional : (s,t,a,b : Type) -> Type
|
||||||
Optional = Optic IsOptional
|
Optional = Optic IsOptional
|
||||||
|
|
||||||
|
||| `Optional'` is the `Simple` version of `Optional`.
|
||||||
public export
|
public export
|
||||||
0 Optional' : (s,a : Type) -> Type
|
0 Optional' : (s,a : Type) -> Type
|
||||||
Optional' = Simple Optional
|
Optional' = Simple Optional
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Utilities for Optionals
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
||| Construct an optional from a projection and a setter function.
|
||||||
public export
|
public export
|
||||||
optional : (s -> Either t a) -> (s -> b -> t) -> Optional s t a b
|
optional : (s -> Either t a) -> (s -> b -> t) -> Optional s t a b
|
||||||
optional prj set @{MkIsOptional _} = dimap @{fromStrong}
|
optional prj set @{MkIsOptional _} = dimap @{fromStrong}
|
||||||
|
@ -41,11 +56,25 @@ optional prj set @{MkIsOptional _} = dimap @{fromStrong}
|
||||||
fromStrong : Strong p => Profunctor p
|
fromStrong : Strong p => Profunctor p
|
||||||
fromStrong = %search
|
fromStrong = %search
|
||||||
|
|
||||||
|
||| Construct a simple optional from a projection and a setter function.
|
||||||
public export
|
public export
|
||||||
optional' : (s -> Maybe a) -> (s -> b -> s) -> Optional s s a b
|
optional' : (s -> Maybe a) -> (s -> b -> s) -> Optional s s a b
|
||||||
optional' prj = optional (\x => maybe (Left x) Right (prj x))
|
optional' prj = optional (\x => maybe (Left x) Right (prj x))
|
||||||
|
|
||||||
|
||| The trivial optic that has no focuses.
|
||||||
|
public export
|
||||||
|
ignored : Optional s s a b
|
||||||
|
ignored @{MkIsOptional _} = dimap @{fromStrong}
|
||||||
|
(\x => (Left x, const x))
|
||||||
|
(\(e, f) => either id (the (b -> s) f) e)
|
||||||
|
. first . right
|
||||||
|
where
|
||||||
|
-- arbitrary choice of where to pull profunctor instance from
|
||||||
|
fromStrong : Strong p => Profunctor p
|
||||||
|
fromStrong = %search
|
||||||
|
|
||||||
|
|
||||||
|
||| Extract projection and setter functions from an optional.
|
||||||
public export
|
public export
|
||||||
getOptional : Optional s t a b -> (s -> Either t a, s -> b -> t)
|
getOptional : Optional s t a b -> (s -> Either t a, s -> b -> t)
|
||||||
getOptional l = l @{MkIsOptional (strong,choice)} (Right, const id)
|
getOptional l = l @{MkIsOptional (strong,choice)} (Right, const id)
|
||||||
|
@ -63,18 +92,7 @@ getOptional l = l @{MkIsOptional (strong,choice)} (Right, const id)
|
||||||
strongr (prj, set) = (either (Left . Left) (either (Left . Right) Right . prj),
|
strongr (prj, set) = (either (Left . Left) (either (Left . Right) Right . prj),
|
||||||
\e,b => mapSnd (`set` b) e)
|
\e,b => mapSnd (`set` b) e)
|
||||||
|
|
||||||
|
||| Extract projection and setter functions from an optional.
|
||||||
public export
|
public export
|
||||||
withOptional : Optional s t a b -> ((s -> Either t a) -> (s -> b -> t) -> r) -> r
|
withOptional : Optional s t a b -> ((s -> Either t a) -> (s -> b -> t) -> r) -> r
|
||||||
withOptional l f = uncurry f (getOptional l)
|
withOptional l f = uncurry f (getOptional l)
|
||||||
|
|
||||||
|
|
||||||
public export
|
|
||||||
ignored : Optional s s a b
|
|
||||||
ignored @{MkIsOptional _} = dimap @{fromStrong}
|
|
||||||
(\x => (Left x, const x))
|
|
||||||
(\(e, f) => either id (the (b -> s) f) e)
|
|
||||||
. first . right
|
|
||||||
where
|
|
||||||
-- arbitrary choice of where to pull profunctor instance from
|
|
||||||
fromStrong : Strong p => Profunctor p
|
|
||||||
fromStrong = %search
|
|
||||||
|
|
|
@ -10,6 +10,11 @@ import Control.Lens.Getter
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Type definitions
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
record IsOptFold p where
|
record IsOptFold p where
|
||||||
constructor MkIsOptFold
|
constructor MkIsOptFold
|
||||||
|
@ -24,16 +29,29 @@ optFoldToGetter : IsOptFold p => IsGetter p
|
||||||
optFoldToGetter @{MkIsOptFold _} = MkIsGetter %search
|
optFoldToGetter @{MkIsOptFold _} = MkIsGetter %search
|
||||||
|
|
||||||
|
|
||||||
|
||| An `OptionalFold` is a getter that may not return a focus value.
|
||||||
|
||| `OptionalFold s a` is equivalent to `s -> Maybe a`.
|
||||||
public export
|
public export
|
||||||
0 OptionalFold : (s,a : Type) -> Type
|
0 OptionalFold : (s,a : Type) -> Type
|
||||||
OptionalFold = Simple (Optic IsOptFold)
|
OptionalFold = Simple (Optic IsOptFold)
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Utilities for OptionalFolds
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
||| Construct an `OptionalFold` from a function.
|
||||||
public export
|
public export
|
||||||
folding : (s -> Maybe a) -> OptionalFold s a
|
folding : (s -> Maybe a) -> OptionalFold s a
|
||||||
folding f @{MkIsOptFold _} =
|
folding f @{MkIsOptFold _} =
|
||||||
contrabimap (\x => maybe (Left x) Right (f x)) Left . right
|
contrabimap (\x => maybe (Left x) Right (f x)) Left . right
|
||||||
|
|
||||||
|
||| Construct an `OptionalFold` that can be used to filter the focuses
|
||||||
|
||| of another optic.
|
||||||
|
|||
|
||||||
|
||| To be more specific, this optic passes the value through unchanged if it
|
||||||
|
||| satisfies the predicate and returns no values if it does not.
|
||||||
public export
|
public export
|
||||||
filtered : (a -> Bool) -> OptionalFold a a
|
filtered : (a -> Bool) -> OptionalFold a a
|
||||||
filtered p = folding (\x => if p x then Just x else Nothing)
|
filtered p = folding (\x => if p x then Just x else Nothing)
|
||||||
|
|
|
@ -7,6 +7,11 @@ import Control.Lens.Iso
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Type definitions
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
record IsPrism p where
|
record IsPrism p where
|
||||||
constructor MkIsPrism
|
constructor MkIsPrism
|
||||||
|
@ -17,24 +22,39 @@ prismToIso : IsPrism p => IsIso p
|
||||||
prismToIso @{MkIsPrism _} = MkIsIso %search
|
prismToIso @{MkIsPrism _} = MkIsIso %search
|
||||||
|
|
||||||
|
|
||||||
|
||| A prism is a first-class reference to one of the cases of a sum type.
|
||||||
|
||| Prisms allow one to determine whether a value matches the focused case
|
||||||
|
||| and extract the corresponding data if it does.
|
||||||
|
|||
|
||||||
|
||| More precisely, a `Prism` is an `Optional` that can be flipped to obtain
|
||||||
|
||| a `Getter` in the opposite direction.
|
||||||
public export
|
public export
|
||||||
0 Prism : (s,t,a,b : Type) -> Type
|
0 Prism : (s,t,a,b : Type) -> Type
|
||||||
Prism = Optic IsPrism
|
Prism = Optic IsPrism
|
||||||
|
|
||||||
|
||| `Prism'` is the `Simple` version of `Prism`.
|
||||||
public export
|
public export
|
||||||
0 Prism' : (s,a : Type) -> Type
|
0 Prism' : (s,a : Type) -> Type
|
||||||
Prism' = Simple Prism
|
Prism' = Simple Prism
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Utilities for prisms
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
||| Construct a prism from injection and projection functions.
|
||||||
public export
|
public export
|
||||||
prism : (b -> t) -> (s -> Either t a) -> Prism s t a b
|
prism : (b -> t) -> (s -> Either t a) -> Prism s t a b
|
||||||
prism inj prj @{MkIsPrism _} = dimap prj (either id inj) . right
|
prism inj prj @{MkIsPrism _} = dimap prj (either id inj) . right
|
||||||
|
|
||||||
|
||| Construct a simple prism from injection and projection functions.
|
||||||
public export
|
public export
|
||||||
prism' : (b -> s) -> (s -> Maybe a) -> Prism s s a b
|
prism' : (b -> s) -> (s -> Maybe a) -> Prism s s a b
|
||||||
prism' inj prj = prism inj (\x => maybe (Left x) Right (prj x))
|
prism' inj prj = prism inj (\x => maybe (Left x) Right (prj x))
|
||||||
|
|
||||||
|
|
||||||
|
||| Extract injection and projection functions from a prism.
|
||||||
public export
|
public export
|
||||||
getPrism : Prism s t a b -> (b -> t, s -> Either t a)
|
getPrism : Prism s t a b -> (b -> t, s -> Either t a)
|
||||||
getPrism l = l @{MkIsPrism choice} (id, Right)
|
getPrism l = l @{MkIsPrism choice} (id, Right)
|
||||||
|
@ -46,15 +66,18 @@ getPrism l = l @{MkIsPrism choice} (id, Right)
|
||||||
strongl (inj, prj) = (Left . inj, either (either (Left . Left) Right . prj) (Left . Right))
|
strongl (inj, prj) = (Left . inj, either (either (Left . Left) Right . prj) (Left . Right))
|
||||||
strongr (inj, prj) = (Right . inj, either (Left . Left) (either (Left . Right) Right . prj))
|
strongr (inj, prj) = (Right . inj, either (Left . Left) (either (Left . Right) Right . prj))
|
||||||
|
|
||||||
|
||| Extract injection and projection functions from a prism.
|
||||||
public export
|
public export
|
||||||
withPrism : Prism s t a b -> ((b -> t) -> (s -> Either t a) -> r) -> r
|
withPrism : Prism s t a b -> ((b -> t) -> (s -> Either t a) -> r) -> r
|
||||||
withPrism l f = uncurry f (getPrism l)
|
withPrism l f = uncurry f (getPrism l)
|
||||||
|
|
||||||
|
|
||||||
|
||| Construct a prism that uses a predicate to determine if a value matches.
|
||||||
public export
|
public export
|
||||||
nearly : a -> (a -> Bool) -> Prism' a ()
|
nearly : a -> (a -> Bool) -> Prism' a ()
|
||||||
nearly x p = prism' (const x) (guard . p)
|
nearly x p = prism' (const x) (guard . p)
|
||||||
|
|
||||||
|
||| Construct a prism that matches only one value.
|
||||||
public export
|
public export
|
||||||
only : Eq a => a -> Prism' a ()
|
only : Eq a => a -> Prism' a ()
|
||||||
only x = nearly x (x ==)
|
only x = nearly x (x ==)
|
||||||
|
|
|
@ -9,6 +9,11 @@ import Control.Lens.Getter
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Type definitions
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
record IsReview p where
|
record IsReview p where
|
||||||
constructor MkIsReview
|
constructor MkIsReview
|
||||||
|
@ -19,37 +24,59 @@ reviewToPrism : IsReview p => IsPrism p
|
||||||
reviewToPrism @{MkIsReview _} = MkIsPrism %search
|
reviewToPrism @{MkIsReview _} = MkIsPrism %search
|
||||||
|
|
||||||
|
|
||||||
|
||| A review is an optic whose only capability is being flipped into a `Getter`
|
||||||
|
||| in the other direction.
|
||||||
|
|||
|
||||||
|
||| Any `Prism` or `Iso` can be used as a review.
|
||||||
public export
|
public export
|
||||||
0 Review : (s,a : Type) -> Type
|
0 Review : (s,a : Type) -> Type
|
||||||
Review s a = Optic IsReview s s a a
|
Review = Simple (Optic IsReview)
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Utilities for Reviews
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
lphantom : (Bifunctor p, Profunctor p) => p b c -> p a c
|
lphantom : (Bifunctor p, Profunctor p) => p b c -> p a c
|
||||||
lphantom = mapFst absurd . lmap {a=Void} absurd
|
lphantom = mapFst absurd . lmap {a=Void} absurd
|
||||||
|
|
||||||
|
||| Construct a review from an injection function.
|
||||||
|
||| Analogous to `to` for getters.
|
||||||
public export
|
public export
|
||||||
unto : (a -> s) -> Review s a
|
unto : (a -> s) -> Review s a
|
||||||
unto f @{MkIsReview _} = lphantom . rmap f
|
unto f @{MkIsReview _} = lphantom . rmap f
|
||||||
|
|
||||||
|
||| Flip a `Getter` to form a `Review`.
|
||||||
public export
|
public export
|
||||||
un : Getter s a -> Review a s
|
un : Getter s a -> Review a s
|
||||||
un = unto . view
|
un = unto . view
|
||||||
|
|
||||||
|
|
||||||
|
||| Turn an optic around to inject a focus value into the larger data structure
|
||||||
|
||| after applying a function to it.
|
||||||
|
||| This function takes a `Review`, which can also be a `Prism` or `Iso`.
|
||||||
public export
|
public export
|
||||||
reviews : Review s a -> (e -> a) -> (e -> s)
|
reviews : Review s a -> (e -> a) -> (e -> s)
|
||||||
reviews l = runCoforget . l . MkCoforget
|
reviews l = runCoforget . l . MkCoforget
|
||||||
|
|
||||||
|
||| Turn an optic around to inject a focus value into the larger data structure.
|
||||||
|
||| This function takes a `Review`, which can also be a `Prism` or `Iso`.
|
||||||
public export
|
public export
|
||||||
review : Review s a -> a -> s
|
review : Review s a -> a -> s
|
||||||
review l = reviews l id
|
review l = reviews l id
|
||||||
|
|
||||||
infixr 8 >.
|
infixr 8 >.
|
||||||
|
|
||||||
|
||| Turn an optic around to inject a focus value into the larger data structure.
|
||||||
|
||| This function takes a `Review`, which can also be a `Prism` or `Iso`.
|
||||||
|
|||
|
||||||
|
||| This is the operator form of `review`.
|
||||||
public export
|
public export
|
||||||
(>.) : a -> Review s a -> s
|
(>.) : a -> Review s a -> s
|
||||||
(>.) x l = review l x
|
(>.) x l = review l x
|
||||||
|
|
||||||
|
||| Flip a `Prism`, `Iso` or `Review` to form a `Getter` in the other direction.
|
||||||
public export
|
public export
|
||||||
re : Review s a -> Getter a s
|
re : Review s a -> Getter a s
|
||||||
re = to . review
|
re = to . review
|
||||||
|
|
|
@ -11,6 +11,11 @@ import Control.Lens.Traversal
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Type definitions
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
record IsSetter p where
|
record IsSetter p where
|
||||||
constructor MkIsSetter
|
constructor MkIsSetter
|
||||||
|
@ -22,32 +27,50 @@ setterToTraversal : IsSetter p => IsTraversal p
|
||||||
setterToTraversal @{MkIsSetter _} = MkIsTraversal %search
|
setterToTraversal @{MkIsSetter _} = MkIsTraversal %search
|
||||||
|
|
||||||
|
|
||||||
|
||| A setter is an optic that only supports setting, not getting.
|
||||||
|
|||
|
||||||
|
||| More specifically, a setter can modify zero or more focus elements. This
|
||||||
|
||| means that all traversals are setters.
|
||||||
|
|||
|
||||||
|
||| Setters can be thought of as a generalization of the `Functor` interface,
|
||||||
|
||| allowing one to map over the contents of a structure.
|
||||||
public export
|
public export
|
||||||
0 Setter : (s,t,a,b : Type) -> Type
|
0 Setter : (s,t,a,b : Type) -> Type
|
||||||
Setter = Optic IsSetter
|
Setter = Optic IsSetter
|
||||||
|
|
||||||
|
||| `Setter'` is the `Simple` version of `Setter`.
|
||||||
public export
|
public export
|
||||||
0 Setter' : (s,a : Type) -> Type
|
0 Setter' : (s,a : Type) -> Type
|
||||||
Setter' = Simple Setter
|
Setter' = Simple Setter
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Utilities for setters
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
||| Construct a setter from a modifying function.
|
||||||
public export
|
public export
|
||||||
sets : ((a -> b) -> s -> t) -> Setter s t a b
|
sets : ((a -> b) -> s -> t) -> Setter s t a b
|
||||||
sets f @{MkIsSetter _} = roam f
|
sets f @{MkIsSetter _} = roam f
|
||||||
|
|
||||||
|
||| Derive a setter from a `Functor` implementation.
|
||||||
public export
|
public export
|
||||||
mapped : Functor f => Setter (f a) (f b) a b
|
mapped : Functor f => Setter (f a) (f b) a b
|
||||||
mapped @{_} @{MkIsSetter _} = map'
|
mapped @{_} @{MkIsSetter _} = map'
|
||||||
|
|
||||||
|
||| Derive a setter from a `Contravariant` implementation.
|
||||||
public export
|
public export
|
||||||
contramapped : Contravariant f => Setter (f a) (f b) b a
|
contramapped : Contravariant f => Setter (f a) (f b) b a
|
||||||
contramapped = sets contramap
|
contramapped = sets contramap
|
||||||
|
|
||||||
|
|
||||||
|
||| Modify the focus or focuses of an optic.
|
||||||
public export
|
public export
|
||||||
over : Setter s t a b -> (a -> b) -> s -> t
|
over : Setter s t a b -> (a -> b) -> s -> t
|
||||||
over l = l @{MkIsSetter Function}
|
over l = l @{MkIsSetter Function}
|
||||||
|
|
||||||
|
||| Set the focus or focuses of an optic to a constant value.
|
||||||
public export
|
public export
|
||||||
set : Setter s t a b -> b -> s -> t
|
set : Setter s t a b -> b -> s -> t
|
||||||
set l = over l . const
|
set l = over l . const
|
||||||
|
|
|
@ -11,6 +11,11 @@ import Control.Lens.Optional
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Type definitions
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
record IsTraversal p where
|
record IsTraversal p where
|
||||||
constructor MkIsTraversal
|
constructor MkIsTraversal
|
||||||
|
@ -21,19 +26,28 @@ traversalToOptional : IsTraversal p => IsOptional p
|
||||||
traversalToOptional @{MkIsTraversal _} = MkIsOptional %search
|
traversalToOptional @{MkIsTraversal _} = MkIsOptional %search
|
||||||
|
|
||||||
|
|
||||||
|
||| A traversal is a lens that may have more than one focus.
|
||||||
public export
|
public export
|
||||||
0 Traversal : (s,t,a,b : Type) -> Type
|
0 Traversal : (s,t,a,b : Type) -> Type
|
||||||
Traversal = Optic IsTraversal
|
Traversal = Optic IsTraversal
|
||||||
|
|
||||||
|
||| `Traversal'` is the `Simple` version of `Traversal`.
|
||||||
public export
|
public export
|
||||||
0 Traversal' : (s,a : Type) -> Type
|
0 Traversal' : (s,a : Type) -> Type
|
||||||
Traversal' = Simple Traversal
|
Traversal' = Simple Traversal
|
||||||
|
|
||||||
|
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
-- Utilities for traversals
|
||||||
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
||| Derive a traversal from a `Traversable` implementation.
|
||||||
public export
|
public export
|
||||||
traversed : Traversable t => Traversal (t a) (t b) a b
|
traversed : Traversable t => Traversal (t a) (t b) a b
|
||||||
traversed @{_} @{MkIsTraversal _} = traverse'
|
traversed @{_} @{MkIsTraversal _} = traverse'
|
||||||
|
|
||||||
|
||| Reverse the order of a traversal's focuses.
|
||||||
public export
|
public export
|
||||||
backwards : Traversal s t a b -> Traversal s t a b
|
backwards : Traversal s t a b -> Traversal s t a b
|
||||||
backwards l @{MkIsTraversal _} = wander func
|
backwards l @{MkIsTraversal _} = wander func
|
||||||
|
@ -42,30 +56,42 @@ backwards l @{MkIsTraversal _} = wander func
|
||||||
func fn = forwards . applyStar {f = Backwards f} (l $ MkStar (MkBackwards . fn))
|
func fn = forwards . applyStar {f = Backwards f} (l $ MkStar (MkBackwards . fn))
|
||||||
|
|
||||||
|
|
||||||
|
||| Map each focus of a traversal to a computation, evaluate those computations
|
||||||
|
||| and combine the results.
|
||||||
public export
|
public export
|
||||||
traverseOf : Applicative f => Traversal s t a b -> (a -> f b) -> s -> f t
|
traverseOf : Applicative f => Traversal s t a b -> (a -> f b) -> s -> f t
|
||||||
traverseOf l = applyStar . l . MkStar {f}
|
traverseOf l = applyStar . l . MkStar {f}
|
||||||
|
|
||||||
|
||| A version of `traverseOf` but with the arguments flipped.
|
||||||
public export
|
public export
|
||||||
forOf : Applicative f => Traversal s t a b -> s -> (a -> f b) -> f t
|
forOf : Applicative f => Traversal s t a b -> s -> (a -> f b) -> f t
|
||||||
forOf l = flip $ traverseOf l
|
forOf l = flip $ traverseOf l
|
||||||
|
|
||||||
|
||| Evaluate each computation within the traversal and collect the results.
|
||||||
public export
|
public export
|
||||||
sequenceOf : Applicative f => Traversal s t (f a) a -> s -> f t
|
sequenceOf : Applicative f => Traversal s t (f a) a -> s -> f t
|
||||||
sequenceOf l = traverseOf l id
|
sequenceOf l = traverseOf l id
|
||||||
|
|
||||||
|
||| Fold across the focuses of a traversal from the leftmost focus, providing a
|
||||||
|
||| replacement value for each focus, and return the final accumulator along
|
||||||
|
||| with the new structure.
|
||||||
public export
|
public export
|
||||||
mapAccumLOf : Traversal s t a b -> (acc -> a -> (acc, b)) -> acc -> s -> (acc, t)
|
mapAccumLOf : Traversal s t a b -> (acc -> a -> (acc, b)) -> acc -> s -> (acc, t)
|
||||||
mapAccumLOf l f z =
|
mapAccumLOf l f z =
|
||||||
let g = state . flip f
|
let g = state . flip f
|
||||||
in runState z . traverseOf l g
|
in runState z . traverseOf l g
|
||||||
|
|
||||||
|
||| Fold across the focuses of a traversal from the rightmost focus, providing a
|
||||||
|
||| replacement value for each focus, and return the final accumulator along
|
||||||
|
||| with the new structure.
|
||||||
public export
|
public export
|
||||||
mapAccumROf : Traversal s t a b -> (acc -> a -> (acc, b)) -> acc -> s -> (acc, t)
|
mapAccumROf : Traversal s t a b -> (acc -> a -> (acc, b)) -> acc -> s -> (acc, t)
|
||||||
mapAccumROf l f z =
|
mapAccumROf l f z =
|
||||||
let g = MkBackwards {f=State acc} . state . flip f
|
let g = MkBackwards {f=State acc} . state . flip f
|
||||||
in runState z . forwards . traverseOf l g
|
in runState z . forwards . traverseOf l g
|
||||||
|
|
||||||
|
||| Fold across the focuses of a traversal from the left, returning each
|
||||||
|
||| intermediate value of the fold.
|
||||||
public export
|
public export
|
||||||
scanl1Of : Traversal s t a a -> (a -> a -> a) -> s -> t
|
scanl1Of : Traversal s t a a -> (a -> a -> a) -> s -> t
|
||||||
scanl1Of l f =
|
scanl1Of l f =
|
||||||
|
@ -74,6 +100,8 @@ scanl1Of l f =
|
||||||
step (Just s) x = let r = f s x in (Just r, r)
|
step (Just s) x = let r = f s x in (Just r, r)
|
||||||
in snd . mapAccumLOf l step Nothing
|
in snd . mapAccumLOf l step Nothing
|
||||||
|
|
||||||
|
||| Fold across the focuses of a traversal from the right, returning each
|
||||||
|
||| intermediate value of the fold.
|
||||||
public export
|
public export
|
||||||
scanr1Of : Traversal s t a a -> (a -> a -> a) -> s -> t
|
scanr1Of : Traversal s t a a -> (a -> a -> a) -> s -> t
|
||||||
scanr1Of l f =
|
scanr1Of l f =
|
||||||
|
|
Loading…
Reference in a new issue