Initial optics

Plutarch/Core.hs

@@ -28,6 +28,7 @@ module Plutarch.Core (
   EDelay (EDelay),
   EPair (EPair),
   EEither (ELeft, ERight),
+  peither,
   EForall (EForall),
   ESome (ESome),
   EFix (EFix),
@@ -36,6 +37,7 @@ module Plutarch.Core (
   ESOP,
   EIsSOP (..),
   EUnit (EUnit),
+  punit,
   EDSL,
   ELC,
   unTerm,
@@ -175,12 +177,24 @@ instance EIsNewtype (EFix f) where type EIsNewtype' _ = False
 data EUnit (f :: ETypeF) = EUnit deriving stock (Generic)
 instance EIsNewtype EUnit where type EIsNewtype' _ = False
 
+punit :: (EConstructable edsl EUnit) => Term edsl EUnit
+punit = econ EUnit
+
 data EPair a b ef = EPair (ef /$ a) (ef /$ b) deriving stock (Generic)
 instance EIsNewtype (EPair a b) where type EIsNewtype' _ = False
 
 data EEither a b f = ELeft (Ef f a) | ERight (Ef f b) deriving stock (Generic)
 instance EIsNewtype (EEither a b) where type EIsNewtype' _ = False
 
+peither :: (ESOP edsl, IsEType edsl a, IsEType edsl b, IsEType edsl c) =>
+  (Term edsl a -> Term edsl c) ->
+  (Term edsl b -> Term edsl c) ->
+  Term edsl (EEither a b) ->
+  Term edsl c
+peither f g te = ematch te \case
+  ELeft x -> f x
+  ERight x -> g x
+
 type ELC :: EDSLKind -> Constraint
 type ELC edsl = forall a b. (IsEType edsl a, IsEType edsl b) => EConstructable edsl (a #-> b)
 

Plutarch/Optics.hs

@@ -0,0 +1,71 @@
+module Plutarch.Optics where
+
+import Data.Profunctor
+
+import Fresnel.Lens
+import Fresnel.Optic
+
+import Plutarch.Core
+
+type PLens edsl s t a b =
+  Lens (Term edsl s) (Term edsl t) (Term edsl a) (Term edsl b)
+
+type PLens' edsl s a = PLens edsl s s a a
+
+class Profunctor p => PChoice p where
+  pleft' :: p (Term edsl a) (Term edsl b) -> p (Term edsl (EEither a c)) (Term edsl (EEither b c))
+  pright' :: p (Term edsl a) (Term edsl b) -> p (Term edsl (EEither c a)) (Term edsl (EEither c b))
+
+type PPrism edsl s t a b =
+  forall p. PChoice p =>
+    Optic p (Term edsl s) (Term edsl t) (Term edsl a) (Term edsl b)
+
+type PPrism' edsl s a = PPrism edsl s s a a
+
+pprism ::
+  (ESOP edsl, IsEType edsl t, IsEType edsl b) =>
+  (Term edsl b -> Term edsl t) ->
+  (Term edsl s -> Term edsl (EEither t a)) ->
+  PPrism edsl s t a b
+pprism inj prj = dimap prj (peither id inj) . pright'
+
+pprism' ::
+  (ESOP edsl, IsEType edsl s, IsEType edsl a, IsEType edsl b) =>
+  (Term edsl b -> Term edsl s) ->
+  (Term edsl s -> Term edsl (EEither EUnit a)) ->
+  PPrism edsl s s a b
+pprism' inj prj = pprism inj (\ts -> ematch (prj ts) \case
+  ELeft _-> econ $ ELeft ts
+  ERight b -> econ $ ERight b)
+
+pfst_ ::
+  (ESOP edsl, IsEType edsl a, IsEType  edsl b, IsEType edsl a') =>
+  PLens edsl (EPair a b) (EPair a' b) a a'
+pfst_ =
+  lens
+    (\tp -> ematch tp \(EPair a _) -> a)
+    (\tp a -> ematch tp \(EPair _ b) -> econ $ EPair a b)
+
+psnd_ ::
+  (ESOP edsl, IsEType edsl a, IsEType  edsl b, IsEType edsl b') =>
+  PLens edsl (EPair a b) (EPair a b') b b'
+psnd_ =
+  lens
+    (\tp -> ematch tp \(EPair _ b) -> b)
+    (\tp b -> ematch tp \(EPair a _) -> econ $ EPair a b)
+
+_ELeft ::
+  (ESOP edsl, IsEType edsl a, IsEType edsl b, IsEType edsl a') =>
+  PPrism edsl (EEither a b) (EEither a' b) a a'
+_ELeft =
+  pprism
+    (econ . ELeft)
+    (peither (econ . ERight) (econ . ELeft . econ . ERight))
+
+_ERight ::
+  (ESOP edsl, IsEType edsl a, IsEType edsl b, IsEType edsl b') =>
+  PPrism edsl (EEither a b) (EEither a b') b b'
+_ERight =
+  pprism
+    (econ . ERight)
+    (peither (econ . ELeft . econ . ELeft) (econ . ERight))

plutarch-core.cabal

@@ -100,12 +100,14 @@ library
     Plutarch.Core
     Plutarch.EType
     Plutarch.Experimental
-    Plutarch.Lens
+    Plutarch.Optics
     Plutarch.Reduce
     Plutarch.STLC
     Plutarch.SystemF
 
   build-depends:
     , base
     , data-fix
+    , fresnel
     , generics-sop
+    , profunctors