on master help sign in
Add an `_R` prism which is useful with `modifyRoute`

Write it and rewrite the existing `rPrism` in terms of some more general optics. This will hopefully aid future attempts to put the most general mechanisms in `dependent-sum` itself.

commit381f904818d753de4b24afe04488c96e733b7913 authorJohn Ericson <John.Ericson@Obsidian.Systems> dateTue 11 Jun 2019, 11:41 (7 years ago) parentde99fc6
1 file changed+94−5
lib/route/src/Obelisk/Route.hs+94−5
lib/route/src/Obelisk/Route.hs+94−5
@@ -61,6 +61,7 @@ module Obelisk.Route
6161 , shadowEncoder
6262 , prismEncoder
6363 , rPrism
64+ , _R
6465 , obeliskRouteEncoder
6566 , obeliskRouteSegment
6667 , pageNameEncoder
@@ -95,7 +96,24 @@ import qualified Control.Categorical.Functor as Cat
9596import Control.Categorical.Bifunctor
9697import Control.Category.Associative
9798import Control.Category.Monoidal
98−import Control.Lens (Identity (..), Prism', makePrisms, itraverse, imap, prism, (^.), re, matching, (^?), _Just, _Nothing, Iso', from, view, Wrapped (..))
99+import Control.Lens
100+ ( Identity (..)
101+ , (^.)
102+ , (^?)
103+ , Iso'
104+ , Prism'
105+ , Wrapped (..)
106+ , _Just
107+ , _Nothing
108+ , from
109+ , imap
110+ , iso
111+ , itraverse
112+ , makePrisms
113+ , prism'
114+ , re
115+ , view
116+ )
99117import Control.Monad.Except
100118import Data.Dependent.Sum (DSum (..))
101119import Data.Dependent.Map (DMap)
@@ -657,10 +675,81 @@ joinPairTextEncoder = Encoder . \case
657675 _ -> return (kt, T.drop (T.length separator) vt)
658676 }
659677
660−--TODO: Rewrite this by composing the given prism with a lens on the first element of the DSum
661−-- Or, more likely, the user can compose it themselves
662−rPrism :: forall f g. (forall a. Prism' (f a) (g a)) -> Prism' (R f) (R g)
663−rPrism p = prism (\(g :/ x) -> g ^. re p :/ x) (\(f :/ x) -> bimap (:/ x) (:/ x) $ matching p f)
678+-- -- | Like '_2' but for DSum not '(,)'.
679+-- dSumFirstLensLike
680+-- :: forall f g g' h
681+-- . Functor f
682+-- => (forall a. g a -> f (g' a))
683+-- -> (DSum g h) -> f (DSum g' h)
684+-- dSumFirstLensLike f (l :=> r) = (:=> r) <$> f l
685+--
686+-- -- | Like '_2' but for DSum not '(,)'.
687+-- dSumSecondLensLike
688+-- :: forall f g h h'
689+-- . Functor f
690+-- => (forall a. h a -> f (h' a))
691+-- -> (DSum g h) -> f (DSum g h')
692+-- dSumSecondLensLike f (l :=> r) = (l :=>) <$> f r
693+
694+-- TODO: Rewrite this by composing the given prism with a lens on the first
695+-- element of the DSum Or, more likely, the user can compose it themselves
696+--
697+-- TODO I (@Ericson2314) think this previous comment is wrong. I wrote the lenses above.
698+-- It didn't help. Combining lenses and prisms yields (affine) traversals, not
699+-- prisms. Perhaps If we had "DStrong", like, 'Strong' but for 'DSum', not '(,)', we
700+-- could get something like:
701+--
702+-- > dSumFirstOptic
703+-- > :: forall f g g' h
704+-- > . DStrong p
705+-- > => (forall a. p (g a) (g' a))
706+-- > -> p (DSum g h) (DSum g' h)
707+-- > dSumFirstOptic = ???
708+--
709+-- That is certainly a science project, and I don't anticipate any additional
710+-- generality between that and what is written.
711+
712+-- This slight generalization of 'rPrism' happens to be enough to write all our
713+-- prism combinators so far.
714+dSumPrism
715+ :: forall f f' g
716+ . (forall a. Prism' (f a) (f' a))
717+ -> Prism' (DSum f g) (DSum f' g)
718+dSumPrism p = prism'
719+ (\(f' :=> x) -> f' ^. re p :=> x)
720+ (\(f :=> x) -> (:=> x) <$> (f ^? p))
721+
722+-- already in obelisk
723+rPrism
724+ :: forall f f'
725+ . (forall a. Prism' (f a) (f' a))
726+ -> Prism' (R f) (R f')
727+rPrism p = dSumPrism p
728+
729+dSumPrism'
730+ :: forall f g a
731+ . (forall b. Prism' (f b) (a :~: b))
732+ -> Prism' (DSum f g) (g a)
733+dSumPrism' p = dSumPrism p . iso (\(Refl :=> b) -> b) (Refl :=>)
734+
735+dSumGEqPrism
736+ :: GEq f
737+ => f a
738+ -> Prism' (DSum f g) (g a)
739+dSumGEqPrism variant = dSumPrism' $ prism' (\Refl -> variant) (\x -> geq variant x)
740+
741+-- | Given a 'tag :: f a', make a prism for 'R f'. This generalizes the usual
742+-- prisms for a sum type (the ones that 'mkPrisms' would make), just as 'R'
743+-- generalized a usual sum type.
744+--
745+-- [This is given the '_R' name of the "cannonical" prism not because it is the
746+-- most general, but because it seems the most useful for routes, and 'R' itself
747+-- trades generality for route-specificity.]
748+_R
749+ :: GEq f
750+ => f a
751+ -> Prism' (R f) a
752+_R variant = dSumGEqPrism variant . iso runIdentity Identity
664753
665754-- | An encoder that only works on the items available via the prism. An error will be thrown in the parse monad
666755-- if the prism doesn't match.