packages feed

pointless-lenses (empty) → 0.0.1

raw patch · 9 files changed

+601/−0 lines, 9 filesdep +basedep +haskell98dep +pointless-haskellsetup-changed

Dependencies added: base, haskell98, pointless-haskell, process

Files

+ LICENSE view
@@ -0,0 +1,31 @@+Copyright (c) 2009, University of Minho++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * The names of contributors may not be used to endorse or promote+      products derived from this software without specific prior+      written permission. ++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README view
@@ -0,0 +1,33 @@+Pointless Lenses++This cabal package can be installed with:++$ cabal install pointless-lenses++For a manual install, execute:++$ runhaskell Setup.lhs configure+$ runhaskell Setup.lhs build+$ runhaskell Setup.lhs install++You can now start playing with the example code that comes with the library, under Language.Pointless.Examples.Examples.+The easiest way is to create a new module that imports some library modules++module Test where++import Test.QuickCheck.Test+import Generics.Pointless.Lenses+import Generics.Pointless.Lenses.Examples.Examples++and interpret it++$ ghci Test.hs++We can now test the well-behavedness of some lens, for example:++> quickCheck (wb filter_lns)++++ OK, passed 100 tests.++Or run some example and later check what it is actually doing:+> exampleT+Fst (1,'a')
+ Setup.lhs view
@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+> import Distribution.Simple+> main = defaultMain
+ Test.hs view
@@ -0,0 +1,5 @@+module Test where++import Test.QuickCheck.Test+import Generics.Pointless.Lenses+import Generics.Pointless.Lenses.Examples.Examples
+ pointless-lenses.cabal view
@@ -0,0 +1,31 @@+Name:            pointless-lenses+Version:         0.0.1+License:         BSD3+License-file:    LICENSE+Author:          Alcino Cunha <alcino@di.uminho.pt>, Hugo Pacheco <hpacheco@di.uminho.pt>+Maintainer:      Hugo Pacheco <hpacheco@di.uminho.pt>+Synopsis:        Pointless Lenses library+Description:+	Pointless Lenses is library of bidirectional lenses (<http://www.cis.upenn.edu/~bcpierce/papers/newlenses-popl.pdf>) defined in the point-free style of programming.+	Generic bidirectional lenses can be defined over inductive types by relying in a set of lifted lens combinators from the standard point-free combinators.+	Virtually any recursive lens can be defined by combining the lenses for the recursion patterns of catamorphisms and anamorphism.+	The library also provides QuickCheck procedures to test the well-behavedness of user-defined lens transformations.+Homepage:        http://haskell.di.uminho.pt/wiki/Pointless+Lenses++Category: Generics++extra-source-files: README, Test.hs++Build-type: Simple+Cabal-Version:  >= 1.2.3++Library+  Hs-Source-Dirs: src+  Build-Depends:        base >= 3 && < 5, pointless-haskell >= 0.0.2, haskell98, process+  exposed-modules:+        Generics.Pointless.Lenses.Combinators+        Generics.Pointless.Lenses.RecursionPatterns,+        Generics.Pointless.Lenses.Reader.RecursionPatterns+        Generics.Pointless.Lenses.Examples.Examples++  extensions: ScopedTypeVariables, FlexibleContexts, Rank2Types, TypeOperators, TypeFamilies
+ src/Generics/Pointless/Lenses/Combinators.hs view
@@ -0,0 +1,181 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Generics.Pointless.Lenses.Combinators+-- Copyright   :  (c) 2009 University of Minho+-- License     :  BSD3+--+-- Maintainer  :  hpacheco@di.uminho.pt+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Pointless Lenses:+-- bidirectional lenses with point-free programming+-- +-- This module lifts a standard set of point-free combinators into bidirectional lenses.+--+-----------------------------------------------------------------------------++module Generics.Pointless.Lenses.Combinators where++import Generics.Pointless.Lenses+import Generics.Pointless.Combinators++-- * Point-free lens combinators++-- | The right exponentiation combinator as a lens.+-- Applies a lens to the domain of a function.+rexp_lns :: Lens b c -> Lens (a -> b) (a -> c)+rexp_lns l = Lens get' put' create'+    where get' = curry (get l . app)+          put' = curry ((put l) . app . (split >< id))+          create' = curry (create l . app)++-- | The lens composition operator.+infixr 9 .<+(.<) :: Lens b a -> Lens c b -> Lens c a+(.<) f g = Lens get' put' create'+    where get' = get f . get g+          put' = put g . (put f . (id >< get g) /\ snd)+          create' = create g . create f++-- | The @fst@ point-free combinator.+fst_lns :: b -> Lens (a,b) a+fst_lns b = Lens get' put' create'+    where get' = fst+          put' = id >< snd+          create' = id /\ (b!)++-- | The @snd@ point-free combinator.+snd_lns :: a -> Lens (a,b) b+snd_lns a = Lens get' put' create'+    where get' = snd+          put' = swap . (id >< fst)+          create' = (a!) /\ id++-- | The @><@ point-free combinator.+infix 7 ><<+(><<) :: Lens c a -> Lens d b -> Lens (c,d) (a,b)+(><<) f g = Lens get' put' create'+    where get' = get f >< get g+          put' = (put f >< put g) . distp+          create' = create f >< create g++-- | The left-biased @\/@ point-free combinator.+-- It chooses left values over right values in the @create@ direction.+infix 4 .\/<+(.\/<) :: Lens a c -> Lens b c -> Lens (Either a b) c+(.\/<) f g = Lens get' put' create'+    where get' = get f \/ get g+          put' = (put f -|- put g) . distr+          create' = inl . create f++-- | The right-biased @\/@ point-free combinator.+-- It chooses right values over left values in the @create@ direction.+infix 4 \/.<+(\/.<) :: Lens a c -> Lens b c -> Lens (Either a b) c+(\/.<) f g = Lens get' put' create'+    where get' = get f \/ get g+          put' = (put f -|- put g) . distr+          create' = inr . create g++-- | The @-|-@ point-free combinator.+infix 5 -|-<+(-|-<) :: Lens c a -> Lens d b -> Lens (Either c d) (Either a b)+(-|-<) f g = Lens get' put' create'+    where get' = get f -|- get g+          put' = ((put f \/ create f . fst) -|- (create g . fst \/ put g)) . dists+          create' = create f -|- create g++-- | The @-|-@ point-free combinator with user-defined backward behavior.+sum_lns :: ((a,d) -> c) -> ((b,c) -> d) -> Lens c a -> Lens d b -> Lens (Either c d) (Either a b)+sum_lns h i f g = Lens get' put' create'+    where get' = get f -|- get g+          put' = (put f -|- put g) . ((id \/ (fst /\ h)) -|- ((fst /\ i) \/ id)) . dists+          create' = create f -|- create g++-- | The @pnt@ point-free combinator.+infix 0 !<+(!<) :: c -> Lens c One+(!<) c = Lens get' put' create'+    where get' = bang+          put' = snd+          create' = (c!)++-- | The @(a!) \/ f@ point-free expression, where @a@ is a constant and @f@ a function.+infix 4 !\/<+(!\/<) :: Eq a => a -> Lens c a -> Lens (Either c b) a+(!\/<) a f = Lens get' put' create'+    where get' = get f \/ (a!)+          put' = (inl \/ coswap) . (id -|- (snd -|- create f . fst)) . (put f -|- (((==a) . fst)?)) . distr+          create' = inl . create f++-- | The @f \/ (a!)@ point-free expression, where @a@ is a constant and @f@ a function.+infix 4 \/!<+(\/!<) :: Eq a => a -> Lens b a -> Lens (Either c b) a+(\/!<) a f = Lens get' put' create'+    where get' = (a!) \/ get f+          put' = (id \/ inr) . ((snd -|- create f . fst) -|- id) . ((((==a) . fst)?) -|- put f) . distr+          create' = inr . create f++-- * Point-free isomorphism combinators++-- | The lens identity combinator.+id_lns :: Lens c c+id_lns = Lens id fst id++-- | The product distribution combinator+distp :: ((c,d),(a,b)) -> ((c,a),(d,b))+distp = fst >< fst /\ snd >< snd++-- | The @distp@ point-free combinator.+distp_lns :: Lens ((c,d),(a,b)) ((c,a),(d,b))+distp_lns = Lens distp (distp . fst) distp++-- | The sum distribution combinator.+dists :: (Either a b,Either c d) -> Either (Either (a,c) (a,d)) (Either (b,c) (b,d))+dists = (distr -|- distr) . distl++-- | The @dists@ point-free combinator.+dists_lns :: Lens (Either a b,Either c d) (Either (Either (a,c) (a,d)) (Either (b,c) (b,d)))+dists_lns = (distr_lns -|-< distr_lns) .< distl_lns++-- | The @swap@ point-free combinator.+swap_lns :: Lens (a,b) (b,a)+swap_lns = Lens swap (swap . fst) swap++-- | The @coswap@ point-free combinator+coswap_lns :: Lens (Either a b) (Either b a)+coswap_lns = Lens coswap (coswap . fst) coswap++-- | The @distl@ point-free combinator.+distl_lns :: Lens (Either a b, c) (Either (a,c) (b,c))+distl_lns = Lens distl (undistl . fst) undistl++-- | The @undistl@ point-free combinator.+undistl_lns :: Lens (Either (a,c) (b,c)) (Either a b, c)+undistl_lns = Lens undistl (distl . fst) distl++-- | The @distr@ point-free combinator.+distr_lns :: Lens (c, Either a b) (Either (c,a) (c,b))+distr_lns = Lens distr (undistr . fst) undistr++-- | The @undistr@ point-free combinator.+undistr_lns :: Lens (Either (c,a) (c,b)) (c, Either a b)+undistr_lns = Lens undistr (distr . fst) distr++-- | The @assocl@ point-free combinator.+assocl_lns :: Lens (a,(b,c)) ((a,b),c)+assocl_lns = Lens assocl (assocr . fst) assocr++-- | The @assocr@ point-free combinator.+assocr_lns :: Lens ((a,b),c) (a,(b,c))+assocr_lns = Lens assocr (assocl . fst) assocl++-- | The @coassocl@ point-free combinator.+coassocl_lns :: Lens (Either a (Either b c)) (Either (Either a b) c)+coassocl_lns = Lens coassocl (coassocr . fst) coassocr++-- | The @coassocr@ point-free combinator.+coassocr_lns :: Lens (Either (Either a b) c) (Either a (Either b c))+coassocr_lns = Lens coassocr (coassocl . fst) coassocl+
+ src/Generics/Pointless/Lenses/Examples/Examples.hs view
@@ -0,0 +1,68 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Generics.Pointless.Lenses.Examples.Examples+-- Copyright   :  (c) 2009 University of Minho+-- License     :  BSD3+--+-- Maintainer  :  hpacheco@di.uminho.pt+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Pointless Lenses:+-- bidirectional lenses with point-free programming+-- +-- This module provides examples, examples and more examples.+--+-----------------------------------------------------------------------------++module Generics.Pointless.Lenses.Examples.Examples where++import Generics.Pointless.Combinators+import Generics.Pointless.Functors+import Generics.Pointless.Fctrable+import Generics.Pointless.Bifunctors+import Generics.Pointless.Bifctrable+import Generics.Pointless.Lenses+import Generics.Pointless.Lenses.Combinators+import Generics.Pointless.Lenses.RecursionPatterns+import Generics.Pointless.Lenses.Reader.RecursionPatterns++-- | List length lens.+length_lns :: a -> Lens [a] Nat+length_lns a = nat_lns _L (\x -> id_lns -|-< snd_lns a)++-- | List zipping lens.+-- The aux transformation is merely for simplifying the constant argument+zip_lns :: Either (Either One (b,[b])) (a,[a]) -> Lens ([a],[b]) [(a,b)]+zip_lns c = ana_lns _L (((!<) c .< aux -|-< distp_lns) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns))+    where aux = (fst_lns _L -|-< snd_lns _L) -|-< fst_lns _L++-- | List filtering lens.+-- The argument passed to @snd_lns@ can be undefined because it will never be used+filter_lns :: Lens [Either a b] [a]+filter_lns = cata_lns _L ((inn_lns .\/< snd_lns _L) .< coassocl_lns .< (id_lns -|-< distl_lns))++-- | List mapping lens.+map_lns :: Lens c a -> Lens [c] [a]+map_lns f = nat_lns _L (\x -> id_lns -|-< f ><< id_lns)++-- | Generic mapping example using user-defined concrete generators+data T a = Fst a | Next (T a) deriving (Eq,Show)++type instance BF T = BPar :+| BId+type instance PF (T a) = Const a :+: Id++instance Mu (T a) where+    inn (Left x) = Fst x+    inn (Right x) = Next x+    out (Fst x) = Left x+    out (Next x) = Right x++aux :: T a -> a+aux (Fst x) = x+aux (Next x) = aux x++tmap_lns l = gmap_lns' (aux . snd) snd l++exampleT = put (tmap_lns (fst_lns 'c')) (Fst 1,(Next (Fst (2,'a'))))+
+ src/Generics/Pointless/Lenses/Reader/RecursionPatterns.hs view
@@ -0,0 +1,137 @@++-----------------------------------------------------------------------------+-- |+-- Module      :  Generics.Pointless.Lenses.Reader.RecursionPatterns+-- Copyright   :  (c) 2009 University of Minho+-- License     :  BSD3+--+-- Maintainer  :  hpacheco@di.uminho.pt+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Pointless Lenses:+-- bidirectional lenses with point-free programming+-- +-- This module provides catamorphism and anamorphism bidirectional combinators for the definition of recursive lenses.+-- The implementations use a monad reader so that each lens combinator permits a more flexible environment.+--+-----------------------------------------------------------------------------++module Generics.Pointless.Lenses.Reader.RecursionPatterns where++import Prelude hiding (Functor(..),fmap)+import Control.Monad hiding (Functor(..),fmap)+import Control.Monad.Instances hiding (Functor(..),fmap)+import Generics.Pointless.Combinators+import Generics.Pointless.MonadCombinators+import Generics.Pointless.Functors+import Generics.Pointless.Fctrable+import Generics.Pointless.Bifunctors+import Generics.Pointless.Bifctrable+import Generics.Pointless.RecursionPatterns+import Generics.Pointless.Lenses+import Generics.Pointless.Lenses.Combinators+import Generics.Pointless.Lenses.RecursionPatterns++-- | The functor mapping function @fmap@ as a more relaxed lens.+-- The extra function allows user-defined behavior when creating default concrete F-values.+fmap_lns' :: Fctrable f => Fix f -> ((a,Rep f c) -> c) -> Lens c a -> Lens (Rep f c) (Rep f a)+fmap_lns' (f::Fix f) h l = Lens get' put' create'+    where get' = fmap f (get l)+          put' = fmap f (put l) . uncurry (fzip' (fctr :: Fctr f) h) . (id /\ snd)+          create' = fmap f (create l)++-- | The polytypic functor zipping combinator.+-- Gives preference to the abstract (first) F-structure.+fzip' :: Fctr f -> ((a,e) -> c) -> (Rep f a,Rep f c) -> (e -> Rep f (a,c))+fzip' I create = return+fzip' K create = return . fst+fzip' (f :*!: g) create = (fzip' f create >|< fzip' g create) . distp+fzip' (f :+!: g) create = (l -||- r) . dists+    where l = fzip' f create \/ fcre' f create . fst+          r = fcre' g create . fst \/ fzip' g create++-- | The polytypic auxiliary function for @fzip'@.+-- Similar to @fmap (id /\ create)@ but using a monad reader for the concrete reconstruction function.+fcre' :: Fctr f -> ((a,e) -> c) -> Rep f a -> (e -> Rep f (a,c))+fcre' I create = return /|\ curry create+fcre' K create = return+fcre' (f :*!: g) create = fcre' f create >|< fcre' g create+fcre' (f :+!: g) create = fcre' f create -||- fcre' g create++-- | The @ana@ recursion pattern as a more relaxed lens.+-- For @ana_lns'@ to be a well-behaved lens, we MUST prove termination of |get| for each instance.+ana_lns' :: (Mu b,Fctrable (PF b)) => ((b,a) -> a) -> Lens a (F b a) -> Lens a b+ana_lns' (h::(b,a) -> a) l = Lens get' put' create'+    where get' = ana b (get l)+          put' = accum b  (put l) (uncurry gene)+          gene = fzip' g h <=< curry (id >< get l)+          create' = cata b (create l)+          b = _L :: b+          g = fctr :: Fctr (PF b)++-- | The @cata@ recursion pattern as a more relaxed lens.+-- For @cata_lns'@ to be a well-behaved lens, we MUST prove termination of |put| and |create| for each instance.+cata_lns' :: (Mu a,Fctrable (PF a)) => ((b,a) -> a) -> (Lens (F a b) b) -> Lens a b+cata_lns' (h::(b,a) -> a) l = Lens get' put' create'+    where get' = cata a (get l)+          put' = ana a (uncurry gene)+          gene = fzip' f h <=< (lexp (fmap (fixF f) get' . out) . curry (put l) /|\ const out)+          create' = ana a (create l)+          a = _L :: a+          f = fctr :: Fctr (PF a)++-- | A more relaxed version of the recursion pattern for recursive functions that can be expressed both as anamorphisms and catamorphisms.+-- Proofs of termination are dismissed.+nat_lns' :: (Mu a,Mu b,Fctrable (PF b)) => ((b,a) -> a) -> NatLens (PF a) (PF b) -> Lens a b+nat_lns' (h::(b,a) -> a) l = ana_lns' h (l a .< out_lns)+    where a = _L :: a++-- | A more relaxed version of the bifunctor mapping function @bmap@ as a lens.+-- Cannot employ @NatLens@ because the extra function depends on the polymorphic type argument.+bmap_lns' :: Bifctrable f => x -> BFix f -> ((a,Rep (BRep f c) x) -> c) -> Lens c a -> Lens (Rep (BRep f c) x) (Rep (BRep f a) x)+bmap_lns' (x::x) (f::BFix f) h l = Lens get' put' create'+    where get' = bmap f (get l) idx+          put' = bmap f (put l) idx . uncurry (bzip' x (bctr :: Bifctr f) h) . (id /\ snd)+          create' = bmap f (create l) idx+          idx = id :: x -> x++-- | A more relaxed version of the the polytypic bifunctor zipping combinator.+bzip' :: x -> Bifctr f -> ((a,e) -> c) -> (Rep (BRep f a) x,Rep (BRep f c) x) -> (e -> Rep (BRep f (a,c)) x)+bzip' x BI create = return . fst+bzip' x BP create = return+bzip' x BK create = return . fst+bzip' x (f :*!| g) create = (bzip' x f create >|< bzip' x g create) . distp+bzip' (x::x) (f :+!| g) create = (l -||- r) . dists+    where l = bzip' x f create \/ bcre' x f create . fst+          r = bcre' x g create . fst \/ bzip' x g create+          idx = id :: x -> x++bcre' :: x -> Bifctr f -> ((a,e) -> c) -> Rep (BRep f a) x -> (e -> (Rep (BRep f (a,c)) x))+bcre' x BI create = return+bcre' x BP create = return /|\ curry create+bcre' x BK create = return+bcre' x (f :*!| g) create = bcre' x f create >|< bcre' x g create+bcre' x (f :+!| g) create = bcre' x f create -||- bcre' x g create++-- | A more relaxed version of the generic mapping lens for parametric types with one polymorphic parameter.+-- We do not define @gmap_lns'@ as a recursion pattern lens because we want to provide more control in the auxiliary functions.+-- Using @bmap_lns'@ we would not get @(a,d c) -> c@ but instead @(a,B d c (d a)) -> c@.+gmap_lns' :: (Mu (d a),Mu (d c),Fctrable (PF (d c)),Fctrable (PF (d a)),Bifctrable (BF d),+              F (d a) (d c) ~ B d a (d c), F (d c) (d c) ~ B d c (d c),+              F (d a) (d a) ~ B d a (d a),F (d c) (d a) ~ B d c (d a))+          => ((a,d c) -> c) -> ((d a,d c) -> d c) -> Lens c a -> Lens (d c) (d a)+gmap_lns' (h::(a,d c) -> c) i l = Lens get' put' create'+    where get' = cata dc (inn . bmap (fixB b) (get l) idda)+          put' = accum da gene (uncurry tau)+          gene = inn . bmap (fixB b) (put l) iddc . uncurry (bzip' dc b h <=< curry (id >< out))+          tau = fzip' f i <=< curry (id >< bmap (fixB b) (get l) iddc . out)+          create' = cata da (inn . bmap (fixB b) (create l) iddc)+          b = bctr :: Bifctr (BF d)+          f = fctr :: Fctr (PF (d a))+          da = _L :: d a+          dc = _L :: d c+          idda = id :: d a -> d a+          iddc = id :: d c -> d c++
+ src/Generics/Pointless/Lenses/RecursionPatterns.hs view
@@ -0,0 +1,112 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Generics.Pointless.Lenses.RecursionPatterns+-- Copyright   :  (c) 2009 University of Minho+-- License     :  BSD3+--+-- Maintainer  :  hpacheco@di.uminho.pt+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Pointless Lenses:+-- bidirectional lenses with point-free programming+-- +-- This module provides catamorphism and anamorphism bidirectional combinators for the definition of recursive lenses.+--+-----------------------------------------------------------------------------++module Generics.Pointless.Lenses.RecursionPatterns where++import Prelude hiding (Functor(..),fmap)++import Generics.Pointless.Combinators+import Generics.Pointless.Functors+import Generics.Pointless.Fctrable+import Generics.Pointless.Bifunctors+import Generics.Pointless.Bifctrable+import Generics.Pointless.RecursionPatterns+import Generics.Pointless.Lenses+import Generics.Pointless.Lenses.Combinators++inn_lns :: Mu a => Lens (F a a) a+inn_lns = Lens inn (out . fst) out++out_lns :: Mu a => Lens a (F a a)+out_lns = Lens out (inn . fst) inn++-- | The functor mapping function @fmap@ as a lens.+fmap_lns :: Fctrable f => Fix f -> Lens c a -> Lens (Rep f c) (Rep f a)+fmap_lns (f::Fix f) l = Lens get' put' create'+    where get' = fmap f (get l)+          put' = fmap f (put l) . fzip (fctr :: Fctr f) (create l)+          create' = fmap f (create l)++-- | The polytypic functor zipping combinator.+-- Gives preference to the abstract (first) F-structure.+fzip :: Fctr f -> (a -> c) -> (Rep f a,Rep f c) -> Rep f (a,c)+fzip I create = id+fzip K create = fst+fzip (f :*!: g) create = (fzip f create >< fzip g create) . distp+fzip (f :+!: g) create = (l -|- r) . dists+    where l = fzip f create \/ fmap (fixF f) (id /\ create) . fst+          r = fmap (fixF g) (id /\ create) . fst \/ fzip g create++-- | The @ana@ recursion pattern as a lens.+-- For @ana_lns@ to be a well-behaved lens, we MUST prove termination of |get| for each instance.+ana_lns :: (Mu b,Fctrable (PF b)) => b -> Lens a (F b a) -> Lens a b+ana_lns (b::b) l = Lens get' put' create'+    where get' = ana b (get l)+          put' = accum b  (put l) (fzip g create' . (id >< get l))+          create' = cata b (create l)+          g = fctr :: Fctr (PF b)++-- | The @cata@ recursion pattern as a lens.+-- For @cata_lns@ to be a well-behaved lens, we MUST prove termination of |put| and |create| for each instance.+cata_lns :: (Mu a,Fctrable (PF a)) => a -> (Lens (F a b) b) -> Lens a b+cata_lns (a::a) l = Lens get' put' create'+    where get' = cata a (get l)+          put' = ana a (fzip f create' . (put l . (id >< fmap (fixF f) get') /\ snd) . (id >< out))+          create' = ana a (create l)+          f = fctr :: Fctr (PF a)++-- | The recursion pattern for recursive functions that can be expressed both as anamorphisms and catamorphisms.+-- Proofs of termination are dismissed.+nat_lns :: (Mu a,Mu b,Fctrable (PF b)) => a -> NatLens (PF a) (PF b) -> Lens a b+nat_lns a l = ana_lns _L (l a .< out_lns)++binn_lns :: Bimu d => Lens (B d a (d a)) (d a)+binn_lns = Lens binn (bout . fst) bout++bout_lns :: Bimu d => Lens (d a) (B d a (d a))+bout_lns = Lens bout (binn . fst) binn++-- | The bifunctor mapping function @bmap@ as a lens.+bmap_lns :: Bifctrable f => BFix f -> Lens c a -> NatLens (BRep f c) (BRep f a)+bmap_lns (f::BFix f) l (x::x) = Lens get' put' create'+    where get' = bmap f (get l) idx+          put' = bmap f (put l) idx . bzip x (bctr :: Bifctr f) (create l)+          create' = bmap f (create l) idx+          idx = id :: x -> x++-- | The polytypic bifunctor zipping combinator.+-- Just maps over the polymorphic parameter. To map over the recursive parameter we can use @fzip@.+bzip :: x -> Bifctr f -> (a -> c) -> (Rep (BRep f a) x,Rep (BRep f c) x) -> Rep (BRep f (a,c)) x+bzip x BI create = fst+bzip x BP create = id+bzip x BK create = fst+bzip x (f :*!| g) create = (bzip x f create >< bzip x g create) . distp+bzip (x::x) (f :+!| g) create = (l -|- r) . dists+    where l = bzip x f create \/ bmap (fixB f) (id /\ create) idx . fst+          r = bmap (fixB g) (id /\ create) idx . fst \/ bzip x g create+          idx = id :: x -> x++-- | Generic mapping lens for parametric types with one polymorphic parameter.+-- Cannot be defined using @nat_lns@ because of the required equality constraints between functors and bifunctors.+-- This could, however, be overcome by defining specific recursive combinators for bifunctors.+gmap_lns :: (Mu (d c),Mu (d a),Fctrable (PF (d c)),Bifctrable (BF d),+             F (d a) (d a) ~ B d a (d a),+             F (d c) (d a) ~ B d c (d a))+         => d a -> Lens c a -> Lens (d c) (d a)+gmap_lns (da::d a) l = cata_lns _L (inn_lns .< (bmap_lns (fixB f) l) da)+    where f = bctr :: Bifctr (BF d)+