rewrite using polymorphic lens type and closer operators

Lens.idr

@@ -1,125 +1,85 @@
 module Lens
 
-import Control.Category
+import Effect.State
+import Effects
 
 %access public
 
--- Store comonad
+Lens : (s : Type) ->
+       (t : Type) ->
+       (a : Type) ->
+       (b : Type) ->
+       {default id f : Type -> Type} ->
+       Type
+Lens s t a b {f} = (a -> f b) -> s -> f t
 
-data Store s a = MkStore (s -> a) s
+Lens' : (s : Type) ->
+        (a : Type) ->
+        {default id f : Type -> Type} ->
+        Type
+Lens' s a {f} = Lens s s a a {f}
 
-class Functor w => Comonad (w : Type -> Type) where
-  extract : w a -> a
-  extend : (w a -> b) -> w a -> w b
+lens : Functor f => (s -> a) -> (s -> b -> t) -> Lens s t a b {f}
+lens sa sbt afb s = sbt s <$> afb (sa s)
 
-class Comonad w => VerifiedComonad (w : Type -> Type) where
-  comonadLaw1 : (wa : w a) ->
-                extend extract wa = wa
-  comonadLaw2 : (f : w a -> b) ->
-                (wa : w a) ->
-                extract (extend f wa) = f wa
-  comonadLaw3 : (f : w b -> c) ->
-                (g : w a -> b) ->
-                (wa : w a) ->
-                extend f (extend g wa) = extend (\d => f (extend g d)) wa
+iso : Functor f => (s -> a) -> (b -> t) -> Lens s t a b {f}
+iso f g afb s = g <$> afb (f s)
 
-instance Functor (Store s) where
-  map f (MkStore g a) = MkStore (f . g) a
+infixl 8 ^.
 
-instance Comonad (Store s) where
-  extract (MkStore f a) = f a
-  extend f (MkStore g a) = MkStore (\b => f (MkStore g b)) a
+(^.) : s -> Lens' s a {f = const a} -> a
+s ^. l = l id s
 
-instance VerifiedComonad (Store s) where
-  comonadLaw1 (MkStore f a) = ?storeIdentityProof
-  comonadLaw2 f (MkStore g a) = Refl
-  comonadLaw3 f g (MkStore h a) = Refl
+use : Lens' s a {f = const a} -> { [STATE s] } Eff a
+use l = [| (^. l) get |]
 
--- TODO: This is evil.
--- Supposedly (jonsterling) this definition used to work without the believe_me.
-private
-eta : (f : a -> b) -> f = (\c => f c)
-eta g = believe_me Refl {g}
-
-storeIdentityProof = proof
-  intros
-  rewrite eta f
-  trivial
-
-pos : Store s a -> s
-pos (MkStore _ s) = s
-
-peek : s -> Store s a -> a
-peek s (MkStore f _) = f s
-
-peeks : (s -> s) -> Store s a -> a
-peeks f (MkStore g s) = g (f s)
-
--- Lenses
+_1 : Functor f => Lens (a, c) (b, c) a b {f}
+_1 = lens fst (\(_, y) => \x => (x, y))
 
-data Lens a b = MkLens (a -> Store b a)
+_2 : Functor f => Lens (a, b) (a, c) b c {f}
+_2 = lens snd (\(x, _) => \y => (x, y))
 
-instance Category Lens where
-  id = MkLens (MkStore id)
-  (.) (MkLens f) (MkLens g) = MkLens (\a => case g a of
-    MkStore ba b => case f b of
-      MkStore cb c => MkStore (Prelude.Basics.(.) ba cb) c)
+infixr 4 $~
 
-lens : (a -> b) -> (b -> a -> a) -> Lens a b
-lens f g = MkLens (\a => MkStore (\b => g b a) (f a))
+($~) : Lens s t a b -> (a -> b) -> s -> t
+($~) = id
 
-iso : (a -> b) -> (b -> a) -> Lens a b
-iso f g = MkLens (\a => MkStore g (f a))
+infixr 4 .~
 
-getL : Lens a b -> a -> b
-getL (MkLens f) a = pos (f a)
+(.~) : Lens s t a b -> b -> s -> t
+(.~) = (. const)
 
-setL : Lens a b -> b -> a -> a
-setL (MkLens f) b = peek b . f
+infixr 4 <$~
 
-modL : Lens a b -> (b -> b) -> a -> a
-modL (MkLens f) g = peeks g . f
+(<$~) : Lens s t a b {f = Pair b} -> (a -> b) -> s -> (b, t)
+(<$~) l f = l (\x => (f x, f x))
 
-mergeL : Lens a c -> Lens b c -> Lens (Either a b) c
-mergeL (MkLens f) (MkLens g) = MkLens $ either (\a => map Left $ f a)
-                                               (\b => map Right $ g b)
+infixr 4 <.~
 
-infixr 0 ^$
-(^$) : Lens a b -> a -> b
-(^$) = getL
+(<.~) : Lens s t a b {f = Pair b} -> b -> s -> (b, t)
+(<.~) l x = l <$~ const x
 
-infixr 4 ^=
-(^=) : Lens a b -> b -> a -> a
-(^=) = setL
+infix 4 $=
 
-infixr 4 ^%=
-(^%=) : Lens a b -> (b -> b) -> a -> a
-(^%=) = modL
+($=) : Lens s t a b -> (a -> b) -> { [STATE s] ==> [STATE t] } Eff ()
+l $= f = updateM (l $~ f)
 
-fstLens : Lens (a,b) a
-fstLens = MkLens $ \(a,b) => MkStore (\ a' => (a', b)) a
+infix 4 .=
+(.=) : Lens s t a b -> b -> { [STATE s] ==> [STATE t] } Eff ()
+l .= x = updateM (l .~ x)
 
-sndLens : Lens (a,b) b
-sndLens = MkLens $ \(a,b) => MkStore (\ b' => (a, b')) b
+infix 4 <$=
+(<$=) : Lens s t a b {f = Pair b} ->
+        (a -> b) ->
+        { [STATE s] ==> [STATE t] } Eff b
+l <$= f = case (l <$~ f) !get of
+    (r, s) => do putM s
+                 return r
 
--- Partial lenses
+infix 4 <.=
+(<.=) : Lens s t a b {f = Pair b} -> b -> { [STATE s] ==> [STATE t] } Eff b
+l <.= x = l <$= const x
 
-data PLens a b = MkPLens (a -> Maybe (Store b a))
-
-instance Category PLens where
-  id = MkPLens (Just . MkStore id)
-  (.) (MkPLens f) (MkPLens g) = MkPLens (\a => do
-    MkStore wba b <- g a
-    MkStore wcb c <- f b
-    return (MkStore (wba . wcb) c))
-
-plens : (a -> Either a (Store b a)) -> PLens a b
-plens f = MkPLens $ either (const Nothing) Just . f
-
-getPL : PLens a b -> a -> Maybe b
-getPL (MkPLens f) a = map pos (f a)
-
-justPL : PLens (Maybe a) a
-justPL = MkPLens (\ma => do
-  a <- ma
-  return (MkStore Just a))
+private
+example : runPure (id <$= (+ 10)) = 10
+example = Refl

lens.ipkg

@@ -1,3 +1,5 @@
 package lens
 
 modules = Lens
+
+opts = "-p effects"