diff --git a/README b/README --- a/README +++ b/README @@ -29,5 +29,5 @@ +++ OK, passed 100 tests. Or run some example and later check what it is actually doing: -> exampleT -Fst (1,'a') +> put filter_left_lns ([1,2,3],[Left 0,Right 'a',Left 4]) +[Left 1,Right 'a',Left 2,Left 3] diff --git a/Test.hs b/Test.hs --- a/Test.hs +++ b/Test.hs @@ -1,5 +1,8 @@ module Test where +import Generics.Pointless.Lenses.PartialCombinators import Generics.Pointless.Lenses.Examples.Examples import Generics.Pointless.Lenses.Examples.Imdb import Generics.Pointless.Lenses.Examples.MapExamples +import Generics.Pointless.Functors +import Generics.Pointless.Lenses diff --git a/pointless-lenses.cabal b/pointless-lenses.cabal --- a/pointless-lenses.cabal +++ b/pointless-lenses.cabal @@ -1,5 +1,5 @@ Name: pointless-lenses -Version: 0.0.7 +Version: 0.0.8 License: BSD3 License-file: LICENSE Author: Alcino Cunha , Hugo Pacheco @@ -8,8 +8,10 @@ Description: Pointless Lenses is library of bidirectional lenses () 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. + Recursive lenses can be defined by combining the lenses for the recursion patterns of catamorphisms and anamorphism. + More refined lens behavior can be achieved a more operation-based variant of delta-lenses (<>). The library also provides QuickCheck procedures to test the well-behavedness of user-defined lens transformations. + More details can be found in the accompanying papers and Homepage: http://haskell.di.uminho.pt/wiki/Pointless+Lenses Category: Generics @@ -21,15 +23,23 @@ Library Hs-Source-Dirs: src - Build-Depends: base >= 3 && < 5, pointless-haskell >= 0.0.2, haskell98, process + Build-Depends: base >= 3 && < 5, derive >= 2.5.4, pointless-haskell >= 0.0.7, containers >= 0.4.0.0, QuickCheck >= 2.4.0.1, haskell98, process exposed-modules: - Generics.Pointless.Lenses.Combinators, - Generics.Pointless.Lenses.RecursionPatterns, - Generics.Pointless.Lenses.Reader.RecursionPatterns, - Generics.Pointless.Lenses.Examples.Examples, - Generics.Pointless.Lenses.Examples.Imdb, - Generics.Pointless.Lenses.Examples.Recs, - Generics.Pointless.Lenses.Examples.MapExamples, - Generics.Pointless.Lenses + Generics.Pointless.Lenses.Combinators, + Generics.Pointless.Lenses.RecursionPatterns, + Generics.Pointless.Lenses.Examples.Examples, + Generics.Pointless.Lenses.Examples.Imdb, + Generics.Pointless.Lenses.Examples.Recs, + Generics.Pointless.Lenses.Examples.MapExamples, + Generics.Pointless.Lenses.PartialCombinators, + Generics.Pointless.Lenses, + Generics.Pointless.DLenses, + Generics.Pointless.DLenses.Combinators, + Generics.Pointless.DLenses.RecursionPatterns, + Generics.Pointless.DLenses.ShapeCombinators, + Generics.Pointless.DLenses.Examples.Examples, + Data.Diff, + Data.Relation, + Data.Shape - extensions: ScopedTypeVariables, FlexibleContexts, Rank2Types, TypeOperators, TypeFamilies, GADTs + extensions: MultiParamTypeClasses, ScopedTypeVariables, FlexibleInstances, FlexibleContexts, TypeOperators, TypeFamilies, GADTs, Rank2Types diff --git a/src/Data/Diff.hs b/src/Data/Diff.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diff.hs @@ -0,0 +1,110 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.Diff +-- Copyright : (c) 2011 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 defines provides some value differencing algorithms that produce deltas estimaating a view update. +-- +----------------------------------------------------------------------------- + +module Data.Diff where + +import Data.Relation +import Data.Shape +import Generics.Pointless.HFunctors + +import Generics.Pointless.Functors + +import Data.List as List +import Data.Set (Set) +import qualified Data.Set as Set + +type Delta a b = Pos a :->: Pos b + +type Diff v = v -> v -> Delta v v + +class (Shapely s) => Differable s where + -- | Positional differencing algorithm + positional :: Diff (s a) + -- | A generic version of a minimal edit distance differencing algorithm + s2sc :: Eq a => Diff (s a) + -- | Converting a list differencing algorithm into a generic differencing algorithm + listDiff :: Diff [a] -> Diff (s a) + -- | Differencing based on a key projection function + keyDiff :: Shapely s => (b -> k) -> Diff (s k) -> Diff (s b) + + -- default definitions + s2sc = listDiff s2scList + listDiff diff v s = diff (data_ v) (data_ s) + keyDiff proj diff v' v = diff (smap proj v') (smap proj v) + +instance Differable Id where + positional x y = mkRel [(0,0)] +instance Differable (Const t) where + positional x y = emptyR +instance (Differable f,Differable g) => Differable (f :+: g) where + positional (InlF x) (InlF y) = positional x y + positional (InrF x) (InrF y) = positional x y + positional x y = emptyR +instance (Differable f,Differable g) => Differable (f :*: g) where + positional x@(ProdF x1 x2) y@(ProdF y1 y2) = + (inv (fstPosR (x1,x2)) .~ positional x1 y1 .~ fstPosR (y1,y2)) + `unionR` (inv (sndPosR (x1,x2)) .~ positional x2 y2 .~ sndPosR (y1,y2)) +instance (Differable f,Differable g) => Differable (f :@: g) where + positional x y = zipR $ Set.toList $ positional fxi fyi + where (CompF fxi) = recover (shape x,Set.toList $ locs x) + (CompF fyi) = recover (shape y,Set.toList $ locs y) + zipR [] = emptyR + zipR ((i,j):rs) = aux (data_(fxi)!!i,data_(fyi)!!j) `unionR` zipR rs + aux (gx,gy) = mkRel [ (data_(gy)!!j,data_(gx)!!i) | (i,j) <- Set.elems $ positional gx gy ] +instance Differable [] where + positional x y = positional (hout x) (hout y) + +-- * The string to string correction problem with block moves + +-- | A list different algorithm inspired in the string-to-string correction problem that computes a minimal edit sequence +-- The used algorithm can be found in +s2scList :: Eq a => Diff [a] +s2scList v s = movesDelta (s2scAlg s v) +movesDelta :: [Move] -> Delta [a] [a] +movesDelta [] = emptyR +movesDelta (m:ms) = moveDelta m `Set.union` movesDelta ms +moveDelta :: Move -> Delta [a] [a] +moveDelta (s,v,m) = mkRel $ zip [v..v+m-1] [s..s+m-1] + +-- position in src, position in view, length +type Move = (Int,Int,Int) + +-- First argument is the original list and the second the modified list, and returns a sequence ov edit operations +s2scAlg :: Eq a => [a] -> [a] -> [Move] +s2scAlg s t = s2scAlg' 0 s t + +s2scAlg' :: Eq a => Int -> [a] -> [a] -> [Move] +s2scAlg' _ s [] = [] +s2scAlg' tpos s t = case findLongestPrefix t s of + Just (plen,spos) -> (spos,tpos,plen) : s2scAlg' (tpos+plen) s (drop plen t) + otherwise -> s2scAlg' (tpos+1) s (tail t) + +-- finds the first list in the second returning the index at which it appears +findL :: Eq a => [a] -> [a] -> Maybe Int +findL l [] = Nothing +findL l s = if isPrefixOf l s then Just 0 else mapMaybe succ $ findL l (tail s) + +mapMaybe :: (a -> b) -> Maybe a -> Maybe b +mapMaybe f Nothing = Nothing +mapMaybe f (Just a) = Just (f a) + +-- length of prefix, starting position in the second list +findLongestPrefix :: Eq a => [a] -> [a] -> Maybe (Int,Int) +findLongestPrefix [] s = Nothing +findLongestPrefix l s = case findL l s of + Just i -> Just (length l,i) + otherwise -> findLongestPrefix (init l) s diff --git a/src/Data/Relation.hs b/src/Data/Relation.hs new file mode 100644 --- /dev/null +++ b/src/Data/Relation.hs @@ -0,0 +1,139 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.Relation +-- Copyright : (c) 2011 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 defines relations as sets of pairs and provides some typical point-free combinators for their manipulation. +-- +----------------------------------------------------------------------------- + +module Data.Relation where + +import qualified Data.Set as Set +import Data.Set (Set) + +----------------------------------------------------------------------------- +-- * Representation + +-- | Type of relations +type Rel a b = Set (a,b) +infixr 8 :<-: +type b :<-: a = Rel a b +infixr 8 :->: +type a :->: b = Rel a b + +-- | Build a relation from a list of pairs. +mkRel :: (Ord a, Ord b) => [(a,b)] -> Rel a b +mkRel pairs = Set.fromList pairs + +-- | Convert relation to a list of pairs. +pairs :: (Ord a, Ord b) => Rel a b -> [(a,b)] +pairs r = Set.elems r + +-- | Obtain the domain of a relation +dom :: (Ord a, Ord b) => Rel a b -> Set a +dom xs = Set.map fst xs + +-- | Obtain the range of a relation +rng :: (Ord a, Ord b) => Rel a b -> Set b +rng xs = Set.map snd xs + +-- | domain for a specific range value +domOf :: (Eq b,Ord a) => b -> Rel a b -> Set a +domOf b r = Set.fromList [ x | (x,y) <- Set.elems r, y == b ] + +-- | range for a specific doman value +rngOf :: (Eq a,Ord b) => a -> Rel a b -> Set b +rngOf a r = Set.fromList [ y | (x,y) <- Set.elems r, x == a] + +-- * Relational combinators + +-- | Build an empty relation. +emptyR :: Rel a b +emptyR = Set.empty + +-- | Build identity relation, which contains an edge from each node to itself. +idR :: Ord a => Set a -> Rel a a +idR s = Set.map (\x -> (x,x)) s + +-- | Build total relation, which contains an edge from each node to +-- each other node and to itself. +total :: Ord a => Set a -> Rel a a +total s = Set.fromList [ (x,y) | x <- l, y <- l ] + where l = Set.elems s + +-- | Take the inverse of a relation +inv :: (Ord a, Ord b) => Rel a b -> Rel b a +inv xs = Set.map (\(x,y) -> (y,x)) xs + +-- | Union of two relations +unionR :: (Ord a,Ord b) => Rel a b -> Rel a b -> Rel a b +unionR r s = Set.union r s + +-- | Intersection of two relations +intersectionR :: (Ord a,Ord b) => Rel a b -> Rel a b -> Rel a b +intersectionR r s = Set.intersection r s + +-- | Compose two relations +infixr 8 .~ +(.~) :: (Ord a, Eq b, Ord c) => Rel b c -> Rel a b -> Rel a c +(.~) r s = mkRel [ (x,z) | (x,y) <- Set.elems s , (y',z) <- Set.elems r , y==y' ] + +funR :: (Ord a,Ord b) => (a -> b) -> Set a -> Rel a b +funR f sa = mkRel [ (x,f x) | x <- Set.elems sa ] + +infixr 9 <.~ +(<.~) :: (Ord a, Ord b, Ord b') => (b -> b') -> Rel a b -> Rel a b' +f <.~ r = Set.map (\(x,y) -> (x,f y)) r + +infixr 9 ~.> +(~.>) :: (Ord a, Ord b, Ord a') => Rel a b -> (a -> a') -> Rel a' b +r ~.> f = Set.map (\(x,y) -> (f x,y)) r + +inlR :: (Ord a,Ord b) => Set a -> Rel a (Either a b) +inlR s = mkRel [ (x,Left x) | x <- Set.elems s ] + +inrR :: (Ord a,Ord b) => Set b -> Rel b (Either a b) +inrR s = mkRel [ (x,Right x) | x <- Set.elems s ] + +-- | The infix either combinator. +infixr 4 \/~ +(\/~) :: (Ord a,Ord b,Ord c) => Rel b a -> Rel c a -> Rel (Either b c) a +(\/~) r s = (r .~ inv (inlR (dom r))) `unionR` (s .~ inv (inrR (dom s))) + +-- | The infix sum combinator. +infix 5 -|-~ +(-|-~) :: (Ord a,Ord b,Ord c,Ord d) => Rel a b -> Rel c d -> Rel (Either a c) (Either b d) +f -|-~ g = inlR (rng f) .~ f \/~ inrR (rng g) .~ g + +fstR :: (Ord a,Ord b) => Set (a,b) -> Rel (a,b) a +fstR s = mkRel [((x,y),x) | (x,y) <- Set.elems s ] + +sndR :: (Ord a,Ord b) => Set (a,b) -> Rel (a,b) b +sndR s = mkRel [((x,y),y) | (x,y) <- Set.elems s ] + +infix 6 /\~ +(/\~) :: (Ord a,Ord b,Ord c) => Rel a b -> Rel a c -> Rel a (b,c) +r /\~ s = (inv (fstR bc) .~ r) `intersectionR` (inv (sndR bc) .~ s) + where bc = Set.fromList [ (x,y) | x <- Set.elems (rng r) , y <- Set.elems (rng s) ] + +infix 7 ><~ +(><~) :: (Ord a,Ord b,Ord c,Ord d) => Rel a c -> Rel b d -> Rel (a,b) (c,d) +r ><~ s = r .~ fstR ab /\~ s .~ sndR ab + where ab = Set.fromList [ (x,y) | x <- Set.elems (dom r) , y <- Set.elems (dom s) ] + +-- | Kernel of a relation. +ker :: (Ord a, Ord b) => Rel a b -> Rel a a +ker r = inv r .~ r + +-- | Image of a relation. +img :: (Ord a, Ord b) => Rel a b -> Rel b b +img r = r .~ inv r diff --git a/src/Data/Shape.hs b/src/Data/Shape.hs new file mode 100644 --- /dev/null +++ b/src/Data/Shape.hs @@ -0,0 +1,112 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.Shape +-- Copyright : (c) 2011 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 defines a class of shapely functors that separate shape and data for polymorphic data types. +-- +----------------------------------------------------------------------------- + +module Data.Shape where + +import Data.Relation +import Generics.Pointless.HFunctors + +import Generics.Pointless.Functors +import Generics.Pointless.Combinators + +import Data.Set as Set + +-- | The type of positions (not a dependent type since it is not supported in Haskell) +type Pos a = Int + +-- * The class of shapely functors and corresponding operations + +-- | Class of shapely functors +class Shapely (s :: * -> *) where + -- operations + traverse :: ((a,x) -> (b,x)) -> (s a,x) -> (s b,x) + smap :: (a -> b) -> s a -> s b + shape :: s a -> s One + data_ :: s a -> [a] + recover :: (s One,[a]) -> s a + arity :: s a -> Int + locs :: s a -> Set (Pos (s a)) + -- default definitions + smap f = fst . traverse (\(a,x) -> (f a,x)) . (id /\ bang) + shape = fst . traverse (bang >< id) . (id /\ bang) + data_ = snd . traverse (\(v,l) -> (v,l++[v])) . (id /\ const []) + recover = fst . traverse f + where f (v,[]) = error "recover undefined: insuficient elements" + f (v,x:xs) = (x,xs) + arity = snd . traverse (\(v,n) -> (v,succ n)) . (id /\ const 0) + locs s = Set.fromList $ [0..pred (arity s)] + +instance Shapely Id where + traverse f (IdF v,p) = (IdF >< id) $ f (v,p) + +instance Shapely (Const c) where + traverse f (ConsF b,p) = (ConsF b,p) + +instance (Shapely f,Shapely g) => Shapely (f :*: g) where + traverse f (ProdF fa ga,p) = (ProdF fb gb,p'') + where (fb,p') = traverse f (fa,p) + (gb,p'') = traverse f (ga,p') + +instance (Shapely f,Shapely g) => Shapely (f :+: g) where + traverse f (InlF fa,p) = (InlF >< id) $ traverse f (fa,p) + traverse f (InrF ga,p) = (InrF >< id) $ traverse f (ga,p) + +instance (Shapely f,Shapely g) => Shapely (f :@: g) where + traverse f (CompF fga,p) = (CompF >< id) $ traverse (traverse f) (fga,p) + +-- * The class of shapely higher-order functors, simply to avoid recursive definitions of Shapely +instance Shapely [] where + traverse f = (hinn >< id) . traverse f . (hout >< id) + +-- | Shapely instance that should be automatically generated +--instance (Hu f,Shapely (H f f)) => Shapely f where +-- traverse f = (hinn >< id) . traverse f . (hout >< id) + +-- ** Special relations over shapes + +-- | Correflexive with the locations of a value +locsR :: Shapely s => s a -> Pos (s a) :->: Pos (s a) +locsR = idR . locs + +-- | Relation between the positions of a pair and positions of left elements +fstPosR :: (Shapely f,Shapely g) => (f a,g b) -> Pos (f a,g b) :->: Pos (f a) +fstPosR (fa,gb) = locsR fa + +-- | Relation between the positions of a pair and positions of right elements +sndPosR :: (Shapely f,Shapely g) => (f a,g b) -> Pos (f a,g b) :->: Pos (g b) +sndPosR (fa,gb) = inv $ funR (+arity fa) (locs gb) + +inlPosR :: (Shapely f,Shapely g) => (f a,g b) -> Pos (f a) :->: Pos (f a,g b) +inlPosR p = inv (fstPosR p) + +inrPosR :: (Shapely f,Shapely g) => (f a,g b) -> Pos (g b) :->: Pos (f a,g b) +inrPosR p = inv (sndPosR p) + +-- | Isomorphism between the positions of a pair and the sum of left and right positions +posPairR :: (Shapely f,Shapely g) => (f a,g b) -> Pos (f a,g b) :->: Either (Pos (f a)) (Pos (g b)) +posPairR p@(fa,gb) = ((inlR (locs fa) .~ fstPosR p) `unionR` (inrR (locs gb) .~ sndPosR p)) + +-- | Either relation applied to the left and right locations of a pair +eitherPosR :: (Shapely f,Shapely g) + => (f a,g b) -> (Pos (f a) :->: Pos (h c)) -> (Pos (g b) :->: Pos (h c)) -> (Pos (f a,g b) :->: Pos (h c)) +eitherPosR p@(fa,gb) r s = (r \/~ s) .~ posPairR p + +-- | Sum relation applied to pairs +sumPosR :: (Shapely f,Shapely g,Shapely h,Shapely i) + => (f a,g b) -> (h c,i d) -> (Pos (f a) :->: Pos (h c)) -> (Pos (g b) :->: Pos (i d)) -> (Pos (f a,g b) :->: Pos (h c,i d)) +sumPosR p p' r s = inv (posPairR p') .~ (r -|-~ s) .~ posPairR p + diff --git a/src/Generics/Pointless/DLenses.hs b/src/Generics/Pointless/DLenses.hs new file mode 100644 --- /dev/null +++ b/src/Generics/Pointless/DLenses.hs @@ -0,0 +1,115 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Generics.Pointless.DLenses +-- Copyright : (c) 2011 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 defines the structure of delta lenses and provides Quickcheck procedures to test delta-lens well-behavedness. +-- +----------------------------------------------------------------------------- + +module Generics.Pointless.DLenses where + +import Data.Relation +import Data.Shape +import Data.Diff +import Generics.Pointless.Lenses (Lens) +import qualified Generics.Pointless.Lenses as Lns + +import qualified Data.Set as Set +import Test.QuickCheck.Gen +import Test.QuickCheck.Arbitrary +import Test.QuickCheck + +-- | The data type of Diskin's et al delta lenses (http://dx.doi.org/10.5381/jot.2011.10.1.a6) +data DeltaLens s a v b = DeltaLens { get0 :: s a -> v b + , getdelta :: s a -> s a -> Delta (s a) (s a) -> Delta (v b) (v b) + , put0 :: (v b,s a) -> Delta (v b) (v b) -> s a + , putdelta :: v b -> s a -> Delta (v b) (v b) -> Delta (s a) (s a) } + +delta_lns :: (Shapely s,Shapely v) => DLens s a v b -> DeltaLens s a v b +delta_lns l = DeltaLens get0' getdelta' put0' putdelta' + where get0' s = get l s + getdelta' s' s dS = inv (getd l s) .~ dS .~ getd l s' + put0' (v,s) dV = put l (v,s) dV + putdelta' v s dV = eitherPosR (v,s) (getd l s .~ dV) (locsR s) .~ putd l v s dV + +-- | The data type of (horizontal) delta lenses +data DLens s a v b = DLens { get :: s a -> v b + , getd :: s a -> Delta (v b) (s a) -- delta (get s) s + , put :: (v b,s a) -> Delta (v b) (v b) -> s a -- (v,s) -> delta v (get s) -> S + , putd :: v b -> s a -> Delta (v b) (v b) -> Delta (s a) (v b,s a) -- v -> s -> d:delta v (get s) -> delta (put (v,s) d) (v,s) + , create :: v b -> s a + , created :: v b -> Delta (s a) (v b) -- v -> delta (create v) v + } + +-- | The type of natural delta lenses. +type NatDLens s v = forall a. DLens s a v a + +-- | Converts a delta lens, for a specific differencing operation, to a normal lens +embed_lns :: Shapely v => Diff (v b) -> DLens s a v b -> Lens (s a) (v b) +embed_lns diff l = Lns.Lens get' put' create' + where get' = get l + put' (v,s) = put l (v,s) (diff v (get l s) .~ getd l s) + create' = create l + +-- ** QuickCheck testing for well-behaved delta lenses + +data TestArgs s a v b = TestArgs (v b) (s a) (Delta (v b) (v b)) deriving Show + +-- | Generates a view, source and delta update triple +testGen :: (Arbitrary (s a),Arbitrary (v b),Shapely s,Shapely v) => DLens s a v b -> Gen (TestArgs s a v b) +testGen l = do + v <- arbitrary + s <- arbitrary + dV <- deltaGen v (get l s) + return $ TestArgs v s dV + +-- | Generates a delta update (a partial function from positions to positions) between two values +deltaGen :: Shapely v => v b -> v b -> Gen (Delta (v b) (v b)) +deltaGen v' v = locsGen (Set.toList $ locs v') (Set.toList $ locs v) +locsGen :: [Int] -> [Int] -> Gen (Int :->: Int) +locsGen [] l = return Set.empty +locsGen (i:is) l = do { x <- locGen i l; y <- locsGen is l; return (Set.union x y) } +locGen :: Int -> [Int] -> Gen (Int :->: Int) +locGen iv [] = return Set.empty +locGen iv l = oneof [do { is <- elements l; return (Set.singleton (iv,is)) },return Set.empty] + +testDLens l = quickCheck $ forAll (testGen l) (wbDelta l) + where wbDelta l (TestArgs v s dV) = wb l v s dV + +-- | QuickCheck procedure to test if a lens is well-behaved. +wb :: (Eq (s a),Eq (v b),Shapely s,Shapely v) => DLens s a v b -> v b -> s a -> Delta (v b) (v b) -> Bool +wb l v s dV = putget l v s dV && getput l s && createget l v && putgetd l v s dV && getputd l s && creategetd l v + +-- | QuickCheck procedure to test if a lens satisfies the PutGet law. +putget :: (Eq (s a),Eq (v b),Shapely s,Shapely v) => DLens s a v b -> v b -> s a -> Delta (v b) (v b) -> Bool +putget l v s dV = get l (put l (v,s) dV) == v + +-- | QuickCheck procedure to test if a lens satisfies the GetPut law. +getput :: (Eq (s a),Shapely s,Shapely v) => DLens s a v b -> s a -> Bool +getput l s = let v = get l s in put l (get l s,s) (locsR v) == s + +-- | QuickCheck procedure to test if a lens satisfies the CreateGet law. +createget :: (Eq (v b),Shapely s,Shapely v) => DLens s a v b -> v b -> Bool +createget l v = get l (create l v) == v + +-- | QuickCheck procedure to test if a lens satisfies the PutGetDelta law. +putgetd :: (Shapely s,Shapely v) => DLens s a v b -> v b -> s a -> Delta (v b) (v b) -> Bool +putgetd l v s dV = let s' = put l (v,s) dV in putd l v s dV .~ getd l s' == inlPosR (v,s) + +-- | QuickCheck procedure to test if a lens satisfies the GetPutDelta law. +getputd :: (Shapely s,Shapely v) => DLens s a v b -> s a -> Bool +getputd l s = let v = get l s in (eitherPosR (v,s) (getd l s) (locsR s)) .~ putd l (get l s) s (locsR v) == locsR s + +-- | QuickCheck procedure to test if a lens satisfies the CreateGetDelta law. +creategetd :: (Shapely s,Shapely v) => DLens s a v b -> v b -> Bool +creategetd l v = let s = create l v in created l v .~ getd l s == locsR v + diff --git a/src/Generics/Pointless/DLenses/Combinators.hs b/src/Generics/Pointless/DLenses/Combinators.hs new file mode 100644 --- /dev/null +++ b/src/Generics/Pointless/DLenses/Combinators.hs @@ -0,0 +1,174 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Generics.Pointless.DLenses.Combinators +-- Copyright : (c) 2011 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 delta-lenses. +-- +----------------------------------------------------------------------------- + +module Generics.Pointless.DLenses.Combinators where + +import Data.Relation +import Data.Shape +import Generics.Pointless.DLenses +import Generics.Pointless.DLenses.ShapeCombinators +import Generics.Pointless.Lenses (Lens) +import qualified Generics.Pointless.Lenses as Lns +import Generics.Pointless.Lenses.Combinators + +import Generics.Pointless.Functors +import Generics.Pointless.Combinators + +-- | Delta lens composition +infixr 9 .<~ +(.<~) :: (Shapely s,Shapely v,Shapely u) => DLens v b u c -> DLens s a v b -> DLens s a u c +f .<~ g = DLens get' getd' put' putd' create' created' + where get' s = get f (get g s) + getd' s = getd g s .~ getd f (get g s) + put' (u,s) dU = put g (put f (u,get g s) dU,s) dV + where dV = eitherPosR (u,s) (getd f v .~ dU) (locsR v) .~ putd f u v dU + v = get g s + putd' u s dU = eitherPosR (v',s) + (sumPosR (u,v) (u,s) (locsR u) (getd g s) .~ putd f u v dU) + (inrPosR (u,s)) + .~ putd g v' s dV + where dV = eitherPosR (u,s) (getd f v .~ dU) (locsR v) .~ putd f u v dU + (v,v') = (get g s,put f (u,v) dV) + create' u = create g (create f u) + created' u = created f u .~ created g (create f u) + +-- | Delta lens identity +id_dlns :: Shapely s => DLens s a s a +id_dlns = DLens get' getd' put' putd' create' created' + where get' s = s + getd' s = locsR s + put' (s',s) dS = s' + putd' s' s dS = inlPosR (s',s) + create' s' = s' + created' s' = locsR s' + +-- | Delta lens bang +bang_dlns :: Shapely s => (Const One b -> s a) -> DLens s a (Const One) b +bang_dlns f = DLens get' getd' put' putd' create' created' + where get' s = ConsF _L + getd' s = emptyR + put' (v,s) dV = s + putd' v s dV = inlPosR (v,s) + create' v = f v + created' v = emptyR + +-- | Delta lens left projection +fst_dlns :: (Shapely f,Shapely g) => (f a -> g a) -> DLens (f :*: g) a f a +fst_dlns h = DLens get' getd' put' putd' create' created' + where get' (ProdF x y) = x + getd' (ProdF x y) = inlPosR (x,y) + put' (x',ProdF x y) dF = ProdF x' y + putd' x' p@(ProdF x y) dF = sumPosR (x',y) (x',p) (locsR x') (inrPosR (x,y)) + create' x' = ProdF x' (h x') + created' x' = inv (inlPosR (x',h x')) + +-- | Delta lens right projection +snd_dlns :: (Shapely f,Shapely g) => (g a -> f a) -> DLens (f :*: g) a g a +snd_dlns h = DLens get' getd' put' putd' create' created' + where get' (ProdF x y) = y + getd' (ProdF x y) = inrPosR (x,y) + put' (y',ProdF x y) dF = ProdF x y' + putd' y' p@(ProdF x y) dF = eitherPosR (x,y') (inrPosR (y',p) .~ inlPosR (x,y)) (inlPosR (y',p)) + create' y' = ProdF (h y') y' + created' y' = inv (inrPosR (h y',y')) + +-- | Delta lens product +infix 7 ><<~ +(><<~) :: (Shapely f,Shapely g,Shapely h,Shapely i) => DLens f a h b -> DLens g a i b -> DLens (f :*: g) a (h :*: i) b +f ><<~ g = DLens get' getd' put' putd' create' created' + where get' (ProdF x y) = ProdF (get f x) (get g y) + getd' (ProdF x y) = sumPosR (get f x,get g y) (x,y) (getd f x) (getd g y) + put' (ProdF z w,ProdF x y) dV = ProdF (put f (z,x) d1) (put g (w,y) d2) + where d1 = inv (inlPosR (get f x,get g y)) .~ dV .~ inlPosR (z,w) + d2 = inv (inrPosR (get f x,get g y)) .~ dV .~ inrPosR (z,w) + putd' p1@(ProdF z w) p2@(ProdF x y) dV = eitherPosR (put f (z,x) d1,put g (w,y) d2) + (sumPosR (z,x) (p1,p2) (inlPosR (z,w)) (inlPosR (x,y)) .~ putd f z x d1) + (sumPosR (w,y) (p1,p2) (inrPosR (z,w)) (inrPosR (x,y)) .~ putd g w y d2) + where d1 = inv (inlPosR (get f x,get g y)) .~ dV .~ inlPosR (z,w) + d2 = inv (inrPosR (get f x,get g y)) .~ dV .~ inrPosR (z,w) + create' (ProdF z w) = ProdF (create f z) (create g w) + created' (ProdF z w) = sumPosR (create f z,create g w) (z,w) (created f z) (created g w) + +-- | Delta lens either +infix 4 \/<~ +(\/<~) :: (Shapely f,Shapely g,Shapely h) => (h b -> Either One One) -> DLens f a h b -> DLens g a h b -> DLens (f :+: g) a h b +(\/<~) p f g = DLens get' getd' put' putd' create' created' + where get' (InlF x) = get f x + get' (InrF y) = get g y + getd' (InlF x) = getd f x + getd' (InrF y) = getd g y + put' (z,InlF x) dV = InlF (put f (z,x) dV) + put' (z,InrF y) dV = InrF (put g (z,y) dV) + putd' z (InlF x) dV = putd f z x dV + putd' z (InrF y) dV = putd g z y dV + create' z = case (p z) of { Left _ -> InlF (create f z) ; Right _ -> InrF (create g z) } + created' z = case (p z) of { Left _ -> created f z ; Right _ -> created g z } + +-- | Delta lens sum +infix 5 -|-<~ +(-|-<~) :: (Shapely f,Shapely g,Shapely h,Shapely i) => DLens f a h b -> DLens g a i b -> DLens (f :+: g) a (h :+: i) b +f -|-<~ g = DLens get' getd' put' putd' create' created' + where get' (InlF x) = InlF (get f x) + get' (InrF y) = InrF (get g y) + getd' (InlF x) = getd f x + getd' (InrF y) = getd g y + put' (InlF z,InlF x) dV = InlF (put f (z,x) dV) + put' (InlF z,InrF y) dV = InlF (create f z) + put' (InrF w,InlF x) dV = InrF (create g w) + put' (InrF w,InrF y) dV = InrF (put g (w,y) dV) + putd' (InlF z) (InlF x) dV = putd f z x dV + putd' (InlF z) (InrF y) dV = inlPosR (z,y) .~ created f z + putd' (InrF w) (InlF x) dV = inlPosR (w,x) .~ created g w + putd' (InrF w) (InrF y) dV = putd g w y dV + create' (InlF z) = InlF (create f z) + create' (InrF w) = InrF (create g w) + created' (InlF z) = created f z + created' (InrF w) = created g w + +swap_dlns :: (Shapely f,Shapely g,ToRep f,ToRep g) => DLens (f :*: g) a (g :*: f) a +swap_dlns = nat_dlns (\a -> swap_lns) + +coswap_dlns :: (Shapely f,Shapely g,ToRep f,ToRep g) => DLens (f :+: g) a (g :+: f) a +coswap_dlns = nat_dlns (\a -> coswap_lns) + +distl_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens ((f :+: g) :*: h) a ((f :*: h) :+: (g :*: h)) a +distl_dlns = nat_dlns (\a -> distl_lns) + +undistl_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens ((f :*: h) :+: (g :*: h)) a ((f :+: g) :*: h) a +undistl_dlns = nat_dlns (\a -> undistl_lns) + +distr_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens (f :*: (g :+: h)) a ((f :*: g) :+: (f :*: h)) a +distr_dlns = nat_dlns (\a -> distr_lns) + +undistr_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens ((f :*: g) :+: (f :*: h)) a (f :*: (g :+: h)) a +undistr_dlns = nat_dlns (\a -> undistr_lns) + +assocl_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens (f :*: (g :*: h)) a ((f :*: g) :*: h) a +assocl_dlns = nat_dlns (\a -> assocl_lns) + +assocr_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens ((f :*: g) :*: h) a (f :*: (g :*: h)) a +assocr_dlns = nat_dlns (\a -> assocr_lns) + +coassocl_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens (f :+: (g :+: h)) a ((f :+: g) :+: h) a +coassocl_dlns = nat_dlns (\a -> coassocl_lns) + +coassocr_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens ((f :+: g) :+: h) a (f :+: (g :+: h)) a +coassocr_dlns = nat_dlns (\a -> coassocr_lns) + + + + diff --git a/src/Generics/Pointless/DLenses/Examples/Examples.hs b/src/Generics/Pointless/DLenses/Examples/Examples.hs new file mode 100644 --- /dev/null +++ b/src/Generics/Pointless/DLenses/Examples/Examples.hs @@ -0,0 +1,270 @@ +{-# LANGUAGE TemplateHaskell #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Generics.Pointless.DLenses.Examples.Examples +-- Copyright : (c) 2011 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 of delta-lenses. +-- +----------------------------------------------------------------------------- + +module Generics.Pointless.DLenses.Examples.Examples where + +import Data.Shape +import Generics.Pointless.DLenses.Combinators +import Generics.Pointless.DLenses.ShapeCombinators +import Generics.Pointless.DLenses +import Generics.Pointless.DLenses.RecursionPatterns +import Generics.Pointless.HFunctors +import Generics.Pointless.Lenses (Lens) +import qualified Generics.Pointless.Lenses as Lns +import Generics.Pointless.Lenses.Combinators +import Generics.Pointless.Lenses.Examples.Examples + +import Generics.Pointless.Combinators +import Generics.Pointless.Functors + +import qualified Data.Set as Set +import Test.QuickCheck hiding ((><)) +import Data.DeriveTH + +-- * Mapping + +srcMap = [(1,'a'),(2,'b'),(3,'c')] +lnsMap :: DLens [] (Int,Char) [] Int +lnsMap = map_dlns (fst_lns (const 'x')) +getMap = get lnsMap srcMap +tgtMap = [0,3,1] +putMap = put lnsMap (tgtMap,srcMap) dV + where dV = Set.fromList [(1,2),(2,0)] + +checkMap = testDLens lnsMap + +-- * Semantic + +halve_dlns :: a -> DLens [] a [] a +halve_dlns d = sem_dlns d rear_bias skel halve + where halve :: [a] -> [a] + halve [] = [] + halve (x:xs) = x : halve' (xs,xs) + halve' :: ([a],[a]) -> [a] + halve' (xs,[]) = [] + halve' (xs,[y]) = [] + halve' (x:xs,y:z:zs) = x : halve' (xs,zs) + skel = halve_lns _L + +srcHalve = [1,2,3,4] +lnsHalve :: DLens [] Int [] Int +lnsHalve = halve_dlns (-1) +getHalve = get lnsHalve srcHalve +tgtHalve = [0,2,1] +createHalve = create lnsHalve tgtHalve +putHalve = put lnsHalve (tgtHalve,srcHalve) dV + where dV = Set.fromList [(1,0),(2,1)] + +invHalve = quickCheck (\s -> shape (Lns.get (halve_lns (_L::Int)) s) == shape (get (halve_dlns _L) s)) +checkHalve = testDLens lnsHalve + +-- * Filtering (user-defined) + +data LE a = NilE | ConsE (Either a a) (LE a) deriving (Eq,Show) +$( derive makeArbitrary ''LE ) +instance FMonoid LE where + fzero = NilE + fplus NilE l = l + fplus l NilE = l + fplus (ConsE x xs) r = ConsE x (fplus xs r) +type instance HF LE = HConst One :+~: (HParam :+~: HParam) :*~: HId +instance Hu LE where + hout NilE = InlF $ ConsF _L + hout (ConsE (Left x) xs) = InrF $ ProdF (InlF $ IdF x) xs + hout (ConsE (Right x) xs) = InrF $ ProdF (InrF $ IdF x) xs + hinn (InlF (ConsF _)) = NilE + hinn (InrF (ProdF (InlF (IdF x)) xs)) = ConsE (Left x) xs + hinn (InrF (ProdF (InrF (IdF x)) xs)) = ConsE (Right x) xs +instance Shapely LE where + traverse f = (hinn >< id) . traverse f . (hout >< id) + +filter_dlns :: DLens LE a [] a +filter_dlns = cata_dlns _L (((\/<~) p hinn_dlns (snd_dlns _L)) .<~ coassocl_dlns .<~ (id_dlns -|-<~ distl_dlns)) + where p _ = Left _L + +srcFilter = ConsE (Left 1) $ ConsE (Right 5) $ ConsE (Left 2) $ ConsE (Right 6) NilE +tgtFilter = [0,1] +lnsFilter :: DLens LE Int [] Int +lnsFilter = filter_dlns +getFilter = get lnsFilter srcFilter +putFilter = put lnsFilter (tgtFilter,srcFilter) dV + where dV = Set.fromList [(1,0)] + +checkFilter = testDLens lnsFilter + +-- * Filtering (composition fixed point) + +instance (Arbitrary (f (g a))) => Arbitrary ((f :@: g) a) where + arbitrary = do {x <- arbitrary; return (CompF x)} +instance (Arbitrary (f a),Arbitrary (g a)) => Arbitrary ((f :+: g) a) where + arbitrary = oneof [do {x <- arbitrary; return (InlF x)},do {x <- arbitrary; return (InrF x)}] +instance (Arbitrary (f a),Arbitrary (g a)) => Arbitrary ((f :*: g) a) where + arbitrary = do {x <- arbitrary; y <- arbitrary; return (ProdF x y)} +instance Arbitrary a => Arbitrary (Id a) where + arbitrary = do {x <- arbitrary; return (IdF x)} +instance Arbitrary c => Arbitrary ((Const c) a) where + arbitrary = do {x <- arbitrary; return (ConsF x)} + +instance Hu ([] :@: (Id :+: Id)) where + hout (CompF []) = InlF $ ConsF _L + hout (CompF (x:xs)) = InrF $ ProdF x (CompF xs) + hinn (InlF (ConsF _)) = CompF [] + hinn (InrF (ProdF x (CompF xs))) = CompF (x:xs) + +filter'_dlns :: DLens ([] :@: (Id :+: Id)) a [] a +filter'_dlns = cata_dlns _L (((\/<~) p hinn_dlns (snd_dlns _L)) .<~ coassocl_dlns .<~ (id_dlns -|-<~ distl_dlns)) + where p _ = Left _L + +srcFilter' = CompF [InlF (IdF 1),InrF (IdF 5),InlF (IdF 2),InrF (IdF 6)] +tgtFilter' = [0,1] +lnsFilter' :: DLens ([] :@: (Id :+: Id)) Int [] Int +lnsFilter' = filter'_dlns +getFilter' = get lnsFilter' srcFilter' +putFilter' = put lnsFilter' (tgtFilter',srcFilter') dV + where dV = Set.fromList [(1,0)] + +checkFilter' = testDLens lnsFilter' + +-- * Tree left spine (fold) + +data Tree a = Empty | Node a (Tree a) (Tree a) deriving (Eq,Show) +$( derive makeArbitrary ''Tree ) +instance Shapely Tree where + traverse f = (hinn >< id) . traverse f . (hout >< id) +type instance HF Tree = HConst One :+~: HParam :*~: (HId :*~: HId) +instance Hu Tree where + hout Empty = InlF $ ConsF _L + hout (Node x l r) = InrF $ ProdF (IdF x) (ProdF l r) + hinn (InlF (ConsF _)) = Empty + hinn (InrF (ProdF (IdF x) (ProdF l r))) = Node x l r +instance FMonoid Tree where + fzero = Empty + fplus t Empty = t + fplus t (Node x l r) = Node x (fplus t l) r + +lspine_dlns :: DLens Tree a [] a +lspine_dlns = cata_dlns _L f + where f = hinn_dlns .<~ (id_dlns -|-<~ id_dlns ><<~ fst_dlns g) + g = const [] + +lnsSpine :: DLens Tree Int [] Int +lnsSpine = lspine_dlns +srcSpine = Node 1 (Node 2 Empty Empty) (Node 3 Empty Empty) +tgtSpine = [0,1,2] +getSpine = get lnsSpine srcSpine +putSpine = put lnsSpine (tgtSpine,srcSpine) dV + where dV = Set.fromList [(1,0),(2,1)] + +checkSpine = testDLens lnsSpine + +-- * Tree left spine (unfold) + +lspine'_dlns :: DLens Tree a [] a +lspine'_dlns = ana_dlns _L f + where f = (id_dlns -|-<~ id_dlns ><<~ fst_dlns g) .<~ hout_dlns + g = const Empty + +lnsSpine' :: DLens Tree Int [] Int +lnsSpine' = lspine'_dlns +srcSpine' = Node 1 (Node 2 Empty Empty) (Node 3 Empty Empty) +tgtSpine' = [0,1,2] +getSpine' = get lnsSpine' srcSpine' +putSpine' = put lnsSpine' (tgtSpine',srcSpine') dV + where dV = Set.fromList [(1,0),(2,1)] + +checkSpine' = testDLens lnsSpine' + +-- * Sieve + +sieve_dlns :: a -> DLens [] a [] a +sieve_dlns a = ana_dlns _L f + where f = (((\/<~) p id_dlns id_dlns) -|-<~ id_dlns) + .<~ coassocl_dlns + .<~ (id_dlns -|-<~ (snd_dlns _L -|-<~ snd_dlns g) .<~ distr_dlns .<~ (id_dlns ><<~ hout_dlns)) + .<~ hout_dlns + p _ = Left _L + g _ = IdF a + +srcSieve = [0,1,2,3] +lnsSieve :: DLens [] Int [] Int +lnsSieve = sieve_dlns (-1) +getSieve = get lnsSieve srcSieve +tgtSieve = [5,1,3] +putSieve = put lnsSieve (tgtSieve,srcSieve) dV + where dV = Set.fromList [(1,0),(2,1)] + +checkSieve = testDLens lnsSieve + +-- * List concatenation + +data NeList a = NeNil [a] | NeCons a (NeList a) deriving (Eq,Show) +type instance HF NeList = HFun [] :+~: HParam :*~: HId +instance Hu NeList where + hout (NeNil l) = InlF l + hout (NeCons x xs) = InrF $ ProdF (IdF x) xs + hinn (InlF l) = NeNil l + hinn (InrF (ProdF (IdF x) xs)) = NeCons x xs +instance FMonoid NeList where + fzero = NeNil [] + fplus (NeNil xs) (NeNil ys) = NeNil (xs++ys) + fplus (NeNil []) y = y + fplus (NeNil xs) (NeCons y ys) = fplus (NeNil (xs++[y])) ys + fplus x (NeNil []) = x + fplus (NeCons x xs) y = NeCons x (fplus xs y) +instance Shapely NeList where + traverse f = (hinn >< id) . traverse f . (hout >< id) + +cat_dlns :: DLens ([] :*: []) a [] a +cat_dlns = cata_dlns nelist g .<~ ana_dlns nelist h + where g = hinn_dlns + .<~ (id_dlns -|-<~ ((\/<~) p id_dlns id_dlns)) + .<~ coassocr_dlns + .<~ (hout_dlns -|-<~ id_dlns) + h = (snd_dlns aux -|-<~ assocr_dlns) + .<~ distl_dlns + .<~ (hout_dlns ><<~ id_dlns) + aux _ = ConsF _L + p _ = Right _L + nelist = ann :: Ann (Fix NeList) + +srcCat = ProdF [1] [3] +tgtCat = [0,1,3,4] +lnsCat :: DLens ([] :*: []) Int [] Int +lnsCat = cat_dlns +getCat = get lnsCat srcCat +putCat = put lnsCat (tgtCat,srcCat) dV + where dV = Set.fromList [(1,0),(2,1)] + +checkCat = testDLens lnsCat + +-- * Tree flatten + +flatten_dlns :: DLens Tree a [] a +flatten_dlns = cata_dlns _L f + where f = hinn_dlns .<~ (id_dlns -|-<~ id_dlns ><<~ cat_dlns) + +srcFlatten = Node 1 (Node 2 Empty Empty) (Node 3 Empty Empty) +lnsFlatten :: DLens Tree Int [] Int +lnsFlatten = flatten_dlns +tgtFlatten = [0,1,2,3] +getFlatten = get lnsFlatten srcFlatten +putFlatten = put lnsFlatten (tgtFlatten,srcFlatten) dV + where dV = Set.fromList [(1,0),(2,1),(3,2)] + +checkFlatten = testDLens lnsFlatten diff --git a/src/Generics/Pointless/DLenses/RecursionPatterns.hs b/src/Generics/Pointless/DLenses/RecursionPatterns.hs new file mode 100644 --- /dev/null +++ b/src/Generics/Pointless/DLenses/RecursionPatterns.hs @@ -0,0 +1,236 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Generics.Pointless.DLenses.RecursionPatterns +-- Copyright : (c) 2011 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 delta-lenses. +-- +----------------------------------------------------------------------------- + +module Generics.Pointless.DLenses.RecursionPatterns where + +import Data.Relation +import Data.Shape +import Data.Diff +import Generics.Pointless.DLenses +import Generics.Pointless.DLenses.Combinators +import Generics.Pointless.DLenses.ShapeCombinators +import Generics.Pointless.HFunctors + +import Generics.Pointless.Functors +import Generics.Pointless.Combinators + +import Data.Set (Set) +import qualified Data.Set as Set + +-- | Inn isomorphism delta lens +hinn_dlns :: (Hu s,Shapely s,Shapely (H s s)) => DLens (H s s) a s a +hinn_dlns = DLens get' getd' put' putd' create' created' + where get' s = hinn s + getd' s = locsR s + put' (v,s) dV = hout v + putd' v s dV = inlPosR (v,s) + create' v = hout v + created' v = locsR v + +-- | Out isomorphism delta lens +hout_dlns :: (Hu s,Shapely s,Shapely (H s s)) => DLens s a (H s s) a +hout_dlns = DLens get' getd' put' putd' create' created' + where get' s = hout s + getd' s = locsR s + put' (v,s) dV = hinn v + putd' v s dV = inlPosR (v,s) + create' v = hinn v + created' v = locsR v + +class SHFunctor (f :: (* -> *) -> (* -> *)) (g :: * -> *) (h :: * -> *) where + -- | Higher-order functor mapping (on shapes) + hmap_dlns :: (Shapely (HRep f g),Shapely (HRep f h)) => AnnH f -> DLens g a h a -> DLens (HRep f g) a (HRep f h) a + -- | Higher-order functor strength (on shapes) + hstrength :: Shapely g => AnnH f -> ((HRep f h) a,g a) -> DLens g a h a -> Delta ((HRep f h) a) (h a) -> (HRep f g) a + -- | Horizontal delta produced by the higher-order functor strength combinator + hstrengthd :: Shapely g => AnnH f -> (HRep f h) a -> g a -> DLens g a h a -> Delta ((HRep f h) a) (h a) -> Delta ((HRep f g) a) ((HRep f h) a,g a) + +instance SHFunctor HId x y where + hmap_dlns _ l = l + hstrength _ (fv,s) l dV = put l (fv,s) dV + hstrengthd _ fv s l dV = putd l fv s dV +instance SHFunctor (HConst c) x y where + hmap_dlns _ l = id_dlns + hstrength _ (fv,s) l dV = fv + hstrengthd _ fv s l dV = inlPosR (fv,s) +instance SHFunctor HParam x y where + hmap_dlns _ l = id_dlns + hstrength _ (fv,s) l dV = fv + hstrengthd _ fv s l dV = inlPosR (fv,s) +instance Shapely f => SHFunctor (HFun f) x y where + hmap_dlns _ l = id_dlns + hstrength _ (fv,s) l dV = fv + hstrengthd _ fv s l dV = inlPosR (fv,s) +instance (Shapely (HRep f y),Shapely (HRep f x),Shapely (HRep g y),Shapely (HRep g x),SHFunctor f x y,SHFunctor g x y) => SHFunctor (f :*~: g) x y where + hmap_dlns (_::AnnH (f:*~:g)) l = hmap_dlns (ann::AnnH f) l ><<~ hmap_dlns (ann::AnnH g) l + hstrength (_::AnnH (f:*~:g)) (ProdF fv gv,s) l dV = ProdF (hstrength (ann::AnnH f) (fv,s) l d1) (hstrength (ann::AnnH g) (gv,s) l d2) + where d1 = dV .~ inlPosR (fv,gv) + d2 = dV .~ inrPosR (fv,gv) + hstrengthd (_::AnnH (f:*~:g)) p@(ProdF fv gv) s l dV = eitherPosR (hstrength (ann::AnnH f) (fv,s) l d1,hstrength (ann::AnnH g) (gv,s) l d2) + (sumPosR (fv,s) (p,s) (inlPosR (fv,gv)) (locsR s) .~ hstrengthd (ann::AnnH f) fv s l d1) + (sumPosR (gv,s) (p,s) (inrPosR (fv,gv)) (locsR s) .~ hstrengthd (ann::AnnH g) gv s l d2) + where d1 = dV .~ inlPosR (fv,gv) + d2 = dV .~ inrPosR (fv,gv) +instance (Shapely (HRep f y),Shapely (HRep f x),Shapely (HRep g y),Shapely (HRep g x),SHFunctor f x y,SHFunctor g x y) => SHFunctor (f :+~: g) x y where + hmap_dlns (_::AnnH (f:+~:g)) l = hmap_dlns (ann::AnnH f) l -|-<~ hmap_dlns (ann::AnnH g) l + hstrength (_::AnnH (f:+~:g)) (InlF fv,s) l dV = InlF $ hstrength (ann::AnnH f) (fv,s) l dV + hstrength (_::AnnH (f:+~:g)) (InrF gv,s) l dV = InrF $ hstrength (ann::AnnH g) (gv,s) l dV + hstrengthd (_::AnnH (f:+~:g)) (InlF fv) s l dV = hstrengthd (ann::AnnH f) fv s l dV + hstrengthd (_::AnnH (f:+~:g)) (InrF gv) s l dV = hstrengthd (ann::AnnH g) gv s l dV + +-- | Higher-order catamorphism delta lens +cata_dlns :: ( FMonoid s,HFoldable (HF s),Hu s,Shapely s,Shapely v + , SHFunctor (HF s) s v,SHFunctor (HF s) s (Const One),SHFunctor (HF s) v (Const One) + , Shapely (H s s),Shapely (H s v),Shapely (HRep (HF s) (Const One)) + ) + => Ann (Fix s) -> DLens (H s v) a v a -> DLens s a v a +cata_dlns (anns::Ann (Fix s)) l = DLens get' getd' put' putd' create' created' + where get' x = get cata x + getd' x = getd cata x + put' (y::v a,x) dV | Set.size setS > 0 && Set.null (setS `Set.intersection` (rng dV)) = shrink_cata anns l (y,x) dV + | Set.size setV > 0 && Set.null (setV `Set.intersection` (dom dV)) = grow_cata anns l (y,x) dV + | otherwise = put cata (y,x) dV + where -- all the elements at the head of the original source not deleted by get + setS = rng $ inv (getd' x) .~ getd (hmap_dlns annf (bang_dlns (_L :: Const One a -> s a))) (hout x) + -- all the elements at the head of the modified view + setV = rng $ created l y .~ getd (hmap_dlns annf (bang_dlns (_L :: Const One a -> v a))) (create l y) + putd' (y::v a) x dV | Set.size setS > 0 && Set.null (setS `Set.intersection` (rng dV)) = shrinkd_cata anns l y x dV + | Set.size setV > 0 && Set.null (setV `Set.intersection` (dom dV)) = growd_cata anns l y x dV + | otherwise = putd cata y x dV + where setS = rng $ inv (getd' x) .~ getd (hmap_dlns annf (bang_dlns (_L :: Const One a -> s a))) (hout x) + setV = rng $ created l y .~ getd (hmap_dlns annf (bang_dlns (_L :: Const One a -> v a))) (create l y) + create' y = create cata y + created' y = created cata y + cata = l .<~ hmap_dlns annf (cata_dlns anns l) .<~ hout_dlns + annf = ann :: AnnH (HF s) + +shrink_cata :: ( FMonoid s,HFoldable (HF s),Hu s,Shapely s,Shapely v + , SHFunctor (HF s) s v,SHFunctor (HF s) v (Const One),SHFunctor (HF s) s (Const One) + , Shapely (HRep (HF s) v),Shapely (HRep (HF s) (Const One)),Shapely (HRep (HF s) s) + ) + => Ann (Fix s) -> DLens (H s v) a v a -> (v a,s a) -> Delta (v a) (v a) -> s a +shrink_cata (anns::Ann (Fix s)) l (y,x) dG = put (cata_dlns anns l) (y,x') dV + where -- reduced source + x' = reduce' annf anns (hout x) + reduceh = dnat (reduce' annf anns) (hout x) + dV = inv (getd (cata_dlns anns l) x') .~ inv reduceh .~ getd (cata_dlns anns l) x .~ dG + annf = ann :: AnnH (HF s) + +shrinkd_cata :: ( FMonoid s,HFoldable (HF s),Hu s,Shapely s,Shapely v + , SHFunctor (HF s) s v,SHFunctor (HF s) v (Const One),SHFunctor (HF s) s (Const One) + , Shapely (HRep (HF s) v),Shapely (HRep (HF s) (Const One)),Shapely (HRep (HF s) s) + ) + => Ann (Fix s) -> DLens (H s v) a v a -> v a -> s a -> Delta (v a) (v a) -> Delta (s a) (v a,s a) +shrinkd_cata (anns::Ann (Fix s)) l y x dG = sumPosR (y,x') (y,hout x) (locsR y) reduceh .~ putd (cata_dlns anns l) y x' dV + where -- reduced source + x' = reduce' annf anns (hout x) + reduceh = dnat (reduce' annf anns) (hout x) + dV = inv (getd (cata_dlns anns l) x') .~ inv reduceh .~ getd (cata_dlns anns l) x .~ dG + annf = ann :: AnnH (HF s) + +grow_cata :: ( FMonoid s,HFoldable (HF s),Hu s,Shapely s,Shapely v + , SHFunctor (HF s) s v,SHFunctor (HF s) s (Const One),SHFunctor (HF s) v (Const One) + , Shapely (H s s),Shapely (H s v),Shapely (H s (Const One)) + ) + => Ann (Fix s) -> DLens (H s v) a v a -> (v a,s a) -> Delta (v a) (v a) -> s a +grow_cata (anns::Ann (Fix s)) l (y,x) dG = hinn $ hstrength annf (create l y,x) (cata_dlns anns l) dG + where dV = dG .~ created l y + annf = ann :: AnnH (HF s) + +growd_cata :: ( FMonoid s,HFoldable (HF s),Hu s,Shapely s,Shapely v + , SHFunctor (HF s) s v,SHFunctor (HF s) s (Const One),SHFunctor (HF s) v (Const One) + , Shapely (HRep (HF s) s),Shapely (HRep (HF s) v),Shapely (HRep (HF s) (Const One)) + ) + => Ann (Fix s) -> DLens (H s v) a v a -> v a -> s a -> Delta (v a) (v a) -> Delta (s a) (v a,s a) +growd_cata (anns::Ann (Fix s)) l y x dG = sumPosR (create l y,x) (y,x) (created l y) (locsR x) .~ hstrengthd annf (create l y) x (cata_dlns anns l) dG + where dV = dG .~ created l y + annf = ann :: AnnH (HF s) + +-- | Higher-order anamorphism delta lens +ana_dlns :: ( Hu v,Shapely s,Shapely v,FMonoid s,HFoldable (HF v) + , SHFunctor (HF v) s v,SHFunctor (HF v) v (Const One),SHFunctor (HF v) s (Const One) + , Shapely (H v s),Shapely (H v v),Shapely (H v (Const One)) + ) + => Ann (Fix v) -> DLens s a (H v s) a -> DLens s a v a +ana_dlns (annv::Ann (Fix v)) l = DLens get' getd' put' putd' create' created' + where get' x = get ana x + getd' x = getd ana x + put' (y,x::s a) dV | Set.size setS > 0 && Set.null (setS `Set.intersection` (rng dV)) = shrink_ana annv l (y,x) dV + | Set.size setV > 0 && Set.null (setV `Set.intersection` (dom dV)) = grow_ana annv l (y,x) dV + | otherwise = put ana (y,x) dV + where -- all the elements at the head of the original source not abstracted by get + setS = rng $ inv (getd ana x) .~ getd l x .~ getd (hmap_dlns anng (bang_dlns (_L :: Const One a -> s a))) (get l x) + -- all the elements at the head of the modified view + setV = rng $ getd (hmap_dlns anng (bang_dlns (_L :: Const One a -> v a))) (hout y) + putd' y (x::s a) dV | Set.size setS > 0 && Set.null (setS `Set.intersection` (rng dV)) = shrinkd_ana annv l y x dV + | Set.size setV > 0 && Set.null (setV `Set.intersection` (dom dV)) = growd_ana annv l y x dV + | otherwise = putd ana y x dV + where setS = rng $ inv (getd ana x) .~ getd l x .~ getd (hmap_dlns anng (bang_dlns (_L :: Const One a -> s a))) (get l x) + setV = rng $ getd (hmap_dlns anng (bang_dlns (_L :: Const One a -> v a))) (hout y) + create' y = create ana y + created' y = created ana y + ana = hinn_dlns .<~ hmap_dlns anng (ana_dlns annv l) .<~ l + anng = ann :: AnnH (HF v) + +shrink_ana :: ( Hu v,FMonoid s,HFoldable (HF v),Shapely s,Shapely v + , SHFunctor (HF v) s v,SHFunctor (HF v) s (Const One),SHFunctor (HF v) v (Const One) + , Shapely (H v s),Shapely (H v v),Shapely (H v (Const One)) + ) + => Ann (Fix v) -> DLens s a (H v s) a -> (v a,s a) -> Delta (v a) (v a) -> s a +shrink_ana (annv::Ann (Fix v)) l (y,x::s a) dG = put (ana_dlns annv l) (y,x') dV + where -- reduced source + x' = reduce' anng anns (get l x) + reduceh = dnat (reduce' anng anns) (get l x) + dV = inv (getd (ana_dlns annv l) x') .~ inv reduceh .~ inv (getd l x) .~ getd (ana_dlns annv l) x .~ dG + anng = ann :: AnnH (HF v) + anns = ann :: Ann (Fix s) + +shrinkd_ana :: ( Hu v,FMonoid s,HFoldable (HF v),Shapely s,Shapely v + , SHFunctor (HF v) s v,SHFunctor (HF v) s (Const One),SHFunctor (HF v) v (Const One) + , Shapely (H v s),Shapely (H v v),Shapely (H v (Const One)) + ) + => Ann (Fix v) -> DLens s a (H v s) a -> v a -> s a -> Delta (v a) (v a) -> Delta (s a) (v a,s a) +shrinkd_ana (annv::Ann (Fix v)) l y (x::s a) dG = sumPosR (y,x') (y,x) (locsR y) (getd l x .~ reduceh) .~ putd (ana_dlns annv l) y x' dV + where -- reduced source + x' = reduce' anng anns (get l x) + reduceh = dnat (reduce' anng anns) (get l x) + dV = inv (getd (ana_dlns annv l) x') .~ inv reduceh .~ inv (getd l x) .~ getd (ana_dlns annv l) x .~ dG + anng = ann :: AnnH (HF v) + anns = ann :: Ann (Fix s) + +grow_ana :: ( Hu v,Shapely s,Shapely v,FMonoid s,HFoldable (HF v) + , SHFunctor (HF v) s (Const One),SHFunctor (HF v) v (Const One),SHFunctor (HF v) s v + , Shapely (H v s),Shapely (H v v),Shapely (H v (Const One)) + ) + => Ann (Fix v) -> DLens s a (H v s) a -> (v a,s a) -> Delta (v a) (v a) -> s a +grow_ana (annv::Ann (Fix v)) l (y,x) dG = create l $ hstrength anng (hout y,x) (ana_dlns annv l) dV + where dV = dG + anng = ann :: AnnH (HF v) + +growd_ana :: ( Hu v,Shapely s,Shapely v,FMonoid s,HFoldable (HF v) + , SHFunctor (HF v) s (Const One),SHFunctor (HF v) v (Const One),SHFunctor (HF v) s v + , Shapely (H v s),Shapely (H v v),Shapely (H v (Const One)) + ) + => Ann (Fix v) -> DLens s a (H v s) a -> v a -> s a -> Delta (v a) (v a) -> Delta (s a) (v a,s a) +growd_ana (annv::Ann (Fix v)) l y x dG = hstrengthd anng (hout y) x (ana_dlns annv l) dV .~ created l y' + where -- grown view + y' = hstrength anng (hout y,x) (ana_dlns annv l) dV + dV = dG + anng = ann :: AnnH (HF v) + + + diff --git a/src/Generics/Pointless/DLenses/ShapeCombinators.hs b/src/Generics/Pointless/DLenses/ShapeCombinators.hs new file mode 100644 --- /dev/null +++ b/src/Generics/Pointless/DLenses/ShapeCombinators.hs @@ -0,0 +1,154 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Generics.Pointless.DLenses.ShapeCombinators +-- Copyright : (c) 2011 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 specific delta-lens combinators over shapes. +-- +----------------------------------------------------------------------------- + +module Generics.Pointless.DLenses.ShapeCombinators where + +import Data.Shape +import Data.Relation +import Data.Diff +import Generics.Pointless.Lenses (Lens) +import qualified Generics.Pointless.Lenses as Lns +import Generics.Pointless.DLenses +import Generics.Pointless.HFunctors + +import Generics.Pointless.Functors +import Generics.Pointless.Combinators + +import Data.List as List +import qualified Data.Set as Set +import qualified Data.IntMap as IntMap + +-- | Lifts a regular lens to a lens on structure +liftConst_dlns :: Lens s v -> DLens (Const s) a (Const v) b +liftConst_dlns l = DLens get' getd' put' putd' create' created' + where get' (ConsF s) = ConsF (Lns.get l s) + getd' s = emptyR + put' (ConsF v,ConsF s) dV = ConsF (Lns.put l (v,s)) + putd' v s dV = emptyR + create' (ConsF v) = ConsF (Lns.create l v) + created' v = emptyR + +-- | Lifts a regular lens to a lens on data elements +liftId_dlns :: Lens a b -> DLens Id a Id b +liftId_dlns l = map_dlns l + +-- | Maps a normal lens over a functor +-- This combinator uses the update delta to infer insertions, deletions and reorderings +map_dlns :: Shapely s => Lens a b -> DLens s a s b +map_dlns l = DLens get' getd' put' putd' create' created' + where get' s = smap (Lns.get l) s + getd' s = locsR s + put' (v,s) dV = fst (traverse aux (v,0)) + where aux (b,i) | Set.size js > 0 = (Lns.put l (b,a),succ i) + | otherwise = (Lns.create l b,succ i) + where js = rngOf i dV + a = data_(s)!!(Set.findMin js) + putd' v s dV = inlPosR (v,s) + create' v = smap (Lns.create l) v + created' v = locsR v + +-- | Converts a natural transformation of Reps to a natural transformation on functors +repnat :: (ToRep s,ToRep v) => Ann (Fix v) -> (forall a. Ann a -> Rep s a -> Rep v a) -> (s :~> v) +repnat v f sa = unrep v (val sa) $ f (val sa) (rep sa) + +-- | Infers an horizontal delta from a natural transformation +dnat :: (Shapely s,Shapely v) => (s :~> v) -> s a -> Delta (v a) (s a) +dnat f sa = mkRel $ zip vi (data_ (f si)) + where va = f sa + si = recover (shape sa,Set.toList (locs sa)) + vi = Set.toList (locs va) + +-- | Lifts a regular natural transformation lens into a shapely lens +nat_dlns :: (Shapely s,Shapely v,ToRep s,ToRep v) => Lns.NatLens s v -> NatDLens s v +nat_dlns l = DLens get' getd' put' putd' create' created' + where get' s = repnat annv (\a -> Lns.get (l a)) s + getd' s = dnat (repnat annv (\a -> Lns.get (l a))) s + put' (v,s) dV = repnat anns (\a -> Lns.put (l a)) (ProdF v s) + putd' v s dV = dnat (repnat anns (\a -> Lns.put (l a))) (ProdF v s) + create' v = repnat anns (\a -> Lns.create (l a)) v + created' v = dnat (repnat anns (\a -> Lns.create (l a))) v + anns = ann :: Ann (Fix s) + annv = ann :: Ann (Fix v) + +-- | Explicti bias for semantic bidirectionalization (needs to be a reordering on lists, i.e., preserve the chunks) +type Bias = forall a. [a] -> [a] +rear_bias = id +front_bias = reverse + +-- | Combinators that simulates the mixed syntactic and semantic bidirectional approach +-- We require that shape . f = get skel . shape +sem_dlns :: (Shapely s,Shapely v) => a -> Bias -> Lens (s One) (v One) -> (s :~> v) -> DLens s a v a +sem_dlns d bias skel f = DLens get' getd' put' putd' create' created' + where get' s = f s + getd' s = dnat f s + put' (v,s) dV = recover (shapeS',IntMap.elems $ IntMap.union gv gs) + where shapeV = smap bang v + shapeS = smap bang s + shapeS' = Lns.put skel (shapeV,shapeS) + locsS = Set.toList (locs shapeS) + locsS' = Set.toList (locs shapeS') + si = recover (shapeS,locsS) + si' = recover (shapeS',locsS') + -- elements of the original view that are copied to the new source + gv = IntMap.fromDistinctAscList $ zip (data_ $ f si') (data_ v) + -- elements retrieved from the original source (just the ones not abstracted by get) and defaults + -- the new source values are put positionally, but may be generalized into a bias + gs = IntMap.fromDistinctAscList $ zip + (bias $ locsS' \\ (data_ $ f si')) + (map (data_ s!!) (bias $ locsS \\ (data_ $ f si)) ++ repeat d) + putd' v s dV = (inlPosR (v,s) .~ viewR) `unionR` (inrPosR (v,s) .~ srcR) + where shapeV = smap bang v + shapeS = smap bang s + shapeS' = Lns.put skel (shapeV,shapeS) + locsS = Set.toList (locs shapeS) + locsV = Set.toList (locs shapeV) + locsS' = Set.toList (locs shapeS') + si = recover (shapeS,locsS) + si' = recover (shapeS',locsS') + viewR = mkRel $ zip (data_ $ f si') locsV + srcR = mkRel $ zip (bias $ locsS' \\ (data_ $ f si')) (bias $ locsS \\ (data_ $ f si)) + create' v = recover (shapeS,IntMap.elems $ IntMap.union gv gs) + where shapeV = smap bang v + shapeS = Lns.create skel shapeV + locsS = Set.toList (locs shapeS) + si = recover (shapeS,locsS) + -- elements of the original view that are copied to the created source + -- the trick is to know that f . create skel = id + gv = IntMap.fromDistinctAscList $ zip (data_ $ f si) (data_ v) + -- new default elements + gs = IntMap.fromDistinctAscList $ zip locsS (repeat d) + -- only the non-default elements are relevant to the horizontal delta + created' v = mkRel $ zip (data_ $ f si) locsV + where shapeV = smap bang v + shapeS = Lns.create skel shapeV + locsV = Set.toList (locs shapeV) + locsS = Set.toList (locs shapeS) + si = recover (shapeS,locsS) + +-- | Transformation between isomorphic functors applied to the same data +-- if they have the same shape then they must have the same locations +-- we also need the same data to be able to convert losslessly between them +coerce_dlns :: (Shapely s,Shapely v,ToRep s, ToRep v,Rep s One ~ Rep v One,Rep s a ~ Rep v a) => DLens s a v a +coerce_dlns = DLens get' getd' put' putd' create' created' + where get' s = unrep annv (val s) (rep s) + getd' s = locsR s + put' (v,s) dV = create' v + putd' v s dV = inlPosR (v,s) + create' v = unrep anns (val v) (rep v) + created' v = locsR v + anns = ann :: Ann (Fix s) + annv = ann :: Ann (Fix v) diff --git a/src/Generics/Pointless/Lenses.hs b/src/Generics/Pointless/Lenses.hs --- a/src/Generics/Pointless/Lenses.hs +++ b/src/Generics/Pointless/Lenses.hs @@ -17,6 +17,7 @@ module Generics.Pointless.Lenses where +import Generics.Pointless.Combinators import Generics.Pointless.Functors -- | The data type of lenses @@ -27,7 +28,24 @@ -- | The type of natural lenses. -- Lenses that encode bidirectional natural transformations. -type NatLens f g = forall x. x -> Lens (Rep f x) (Rep g x) +type NatLens f g = forall a. Ann a -> Lens (Rep f a) (Rep g a) + +rep_lns :: (ToRep s,ToRep v) => Lens (s a) (v b) -> Lens (Rep s a) (Rep v b) +rep_lns (l::Lens (s a) (v b)) = Lens get' put' create' + where get' = rep . get l . unrep anns anna + put' = rep . put l . (unrep annv annb >< unrep anns anna) + create' = rep . create l . unrep annv annb + anns = ann :: Ann (Fix s) + annv = ann :: Ann (Fix v) + anna = ann :: Ann a + annb = ann :: Ann b + +-- Lens where we use the whole view to help computing the function parameters to create +varlens :: (v -> Lens c a) -> v -> (a -> v) -> Lens c a +varlens l v f = Lens get' put' create' + where get' c = get (l v) c + put' (a,c) = put (l (f a)) (a,c) + create' a = create (l (f a)) a -- | Increment a number. inc_lns :: Enum a => Lens a a diff --git a/src/Generics/Pointless/Lenses/Combinators.hs b/src/Generics/Pointless/Lenses/Combinators.hs --- a/src/Generics/Pointless/Lenses/Combinators.hs +++ b/src/Generics/Pointless/Lenses/Combinators.hs @@ -27,13 +27,8 @@ ap_lns :: Eq a => (b -> a) -> Lens ((a -> b),a) b ap_lns f = Lens get' put' create' where get' = app - --put' = (ext /\ fst . snd) . assocr . swap put' (y,(g,x)) = let h x' = if x == x' then y else g x in (h,x) create' = const /\ f - ---ext :: Eq a => ((a -> b),(a,b)) -> (a -> b) ---ext = curry f --- where f = (snd . snd . fst \/ app . (fst >< id)) . ((eq . (fst . snd >< id))?) -- | Predicate application is a lens. infix 0 ?< diff --git a/src/Generics/Pointless/Lenses/Examples/Examples.hs b/src/Generics/Pointless/Lenses/Examples/Examples.hs --- a/src/Generics/Pointless/Lenses/Examples/Examples.hs +++ b/src/Generics/Pointless/Lenses/Examples/Examples.hs @@ -1,7 +1,7 @@ ----------------------------------------------------------------------------- -- | -- Module : Generics.Pointless.Lenses.Examples.Examples --- Copyright : (c) 2009 University of Minho +-- Copyright : (c) 2011 University of Minho -- License : BSD3 -- -- Maintainer : hpacheco@di.uminho.pt @@ -19,11 +19,15 @@ import Generics.Pointless.Combinators import Generics.Pointless.Functors +import Generics.Pointless.RecursionPatterns import Generics.Pointless.Bifunctors import Generics.Pointless.Examples.Examples import Generics.Pointless.Lenses import Generics.Pointless.Lenses.Combinators +import Generics.Pointless.Lenses.PartialCombinators import Generics.Pointless.Lenses.RecursionPatterns +import Debug.Trace +import Prelude hiding (replicate) {-# RULES "mapId" @@ -59,7 +63,7 @@ #-} {-# RULES "lengthConcat" forall c. - length_lns c .< concat_lns = suml_lns .< map_lns (length_lns c) + length_lns c .< concat_lns = sumn_lns .< map_lns (length_lns c) #-} {-# RULES "filterMap" forall l1 l2. @@ -88,14 +92,6 @@ length_lns :: a -> Lens [a] Nat length_lns a = nat_lns _L (\_ -> id_lns -|-< snd_lns (a!)) -zipWith_lns :: Lens (a,b) c -> Lens ([a],[b]) [c] -zipWith_lns f = ana_lns _L (((!<) c -|-< (f ><< id_lns) .< distp_lns) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns)) - where - -- 1st option: do nothing - -- 2nd option: append to the left source list - -- 3rd option: append to right source list - c = const $ Left (Left (_L,_L)) - -- | List zipping lens. zip_lns :: Lens ([a],[b]) [(a,b)] zip_lns = ana_lns _L (((!<) c -|-< distp_lns) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns)) @@ -115,49 +111,53 @@ -- 3rd option: increment the source number by c = const $ Left (Left (_L,_L)) --- | List filtering lens. +-- | Left list filtering lens. -- The argument passed to @snd_lns@ can be undefined because it will never be used filter_left_lns :: Lens [Either a b] [a] filter_left_lns = cata_lns _L ((inn_lns .\/< snd_lns _L) .< coassocl_lns .< (id_lns -|-< distl_lns)) +-- | Right list filtering lens. +-- The argument passed to @snd_lns@ can be undefined because it will never be used filter_right_lns :: Lens [Either a b] [b] filter_right_lns = cata_lns _L ((inn_lns .\/< snd_lns _L) .< coassocl_lns .< (id_lns -|-< coswap_lns .< distl_lns)) -- | Binary list concatenation. -- Lens hylomorphisms can be defined as the composition of a catamorphism after an anamorphism. -cat_lns :: Lens ([a],[a]) [a] -cat_lns = hylo_lns (_L :: NeList [a] a) g h - where g = inn_lns .< (out_lns \/$< id_lns) +cat_lns' :: ((a,[a]) -> Bool) -> Lens ([a],[a]) [a] +cat_lns' p = hylo_lns (ann :: Ann (NeList [a] a)) g h + where g = inn_lns .< (id_lns -|-< ((\/<) f id_lns id_lns)) .< coassocr_lns .< (out_lns -|-< id_lns) h = (snd_lns bang -|-< assocr_lns) .< distl_lns .< (out_lns ><< id_lns) + f = (bang -|- bang) . coswap . (p?) +cat_lns = cat_lns' (const False) -- | Binary list transposition. --- Binary version of @transpose@. transpose_lns :: Lens ([a],[a]) [a] transpose_lns = hylo_lns t g h where g = inn_lns .< (out_lns \/$< id_lns) h = (snd_lns _L -|-< (id_lns ><< swap_lns) .< assocr_lns) .< distl_lns .< (out_lns ><< id_lns) - t = _L :: K [a] :+!: (K a :*!: I) + t = ann :: Ann (K [a] :+!: (K a :*!: I)) -- | Addition of two natural numbers. plus_lns :: Lens (Nat,Nat) Nat -plus_lns = hylo_lns (_L::From Nat) f g +plus_lns = hylo_lns (ann::Ann (From Nat)) f g where f = inn_lns .< (out_lns \/$< id_lns) g = (snd_lns bang -|-< id_lns) .< distl_lns .< (out_lns ><< id_lns) -suml_lns :: Lens [Nat] Nat -suml_lns = cata_lns _L g +-- | Sums a list of natural numbers. +sumn_lns :: Lens [Nat] Nat +sumn_lns = cata_lns _L g where g = inn_lns .< (id_lns #\/< (out_lns .< plus_lns)) -concatMap_lns :: Lens a [b] -> Lens [a] [b] -concatMap_lns l = cata_lns _L f - where f = inn_lns .< (id_lns #\/< out_lns .< cat_lns .< (l ><< id_lns)) - -- | List concatenation. concat_lns :: Lens [[a]] [a] concat_lns = cata_lns _L (inn_lns .< (id_lns #\/< out_lns .< cat_lns)) +-- | @concat_lns .< map_lns l@ +concatMap_lns :: Lens a [b] -> Lens [a] [b] +concatMap_lns l = cata_lns _L f + where f = inn_lns .< (id_lns #\/< out_lns .< cat_lns .< (l ><< id_lns)) + -- | Partitions a list of options into two lists. --- Note that this imposes some redefinement of the traditional definition in order to fit our framework. partition_lns :: Lens [Either a b] ([a],[b]) partition_lns = cata_lns _L f where f = (inn_lns ><< id_lns) .< undistl_lns .< ((!/\<) id_lns -|-< (id_lns ><< g) .< undistr_lns) .< coassocr_lns @@ -169,17 +169,33 @@ map_lns :: Lens c a -> Lens [c] [a] map_lns f = nat_lns _L (\_ -> id_lns -|-< f ><< id_lns) -head_lns :: [a] -> Lens [a] (Either One a) -head_lns l = (id_lns -|-< fst_lns (l!)) .< out_lns +-- | Safe head lens. +shead_lns :: [a] -> Lens [a] (Either One a) +shead_lns l = (id_lns -|-< fst_lns (l!)) .< out_lns -tail_lns :: a -> Lens [a] (Either One [a]) -tail_lns v = (id_lns -|-< snd_lns (v!)) .< out_lns +-- | Safe tail lens. +stail_lns :: a -> Lens [a] (Either One [a]) +stail_lns v = (id_lns -|-< snd_lns (v!)) .< out_lns +-- ** Halve + +-- | Splits a list in half. +halve_lns :: a -> Lens [a] [a] +halve_lns v = ana_lns _L g + where g = (id_lns -|-< id_lns ><< nil_lns .< (id_lns -|-< fst_lns (const v)) .< last_lns) .< out_lns + +nil_lns :: Lens (Either One [a]) [a] +nil_lns = inn_lns .< (id_lns #\/< id_lns) .< (id_lns -|-< out_lns) + +last_lns :: Lens [a] (Either One ([a],a)) +last_lns = cata_lns _L g + where g = (id_lns -|-< (inn_lns ><< id_lns) .< undistl_lns .< (swap_lns -|-< assocl_lns) .< distr_lns) + -- ** Reverse -- | Inserts an element at the end of a list, thus making it non-empty. snoc_lns :: Lens (a,[a]) (Some a) -snoc_lns = hylo_lns (_L :: NeList a a) f g +snoc_lns = hylo_lns (ann :: Ann (NeList a a)) f g where f = inn_lns g = (fst_lns _L -|-< subr_lns) .< distr_lns .< (id_lns ><< out_lns) @@ -212,7 +228,7 @@ len_lns = hylo_lns t g h where g = id_lns .\/< id_lns h = (snd_lns _L -|-< snd_lns _L .< assocr_lns .< (id_lns ><< inc_lns)) .< distl_lns .< (out_lns ><< id_lns) - t = _L :: K Int :+!: I + t = ann :: Ann (K Int :+!: I) -- Integer addition add_lns :: Lens (Int,Int) Int @@ -227,13 +243,52 @@ sumInt_lns :: Lens [Int] Int sumInt_lns = cata_lns _L ((0 !\/< add_lns) _L) --- | Incremental summation of a list. --- Since general splitting is not a lens, we need to provide user-defined put and create functions that serve our purpose and construct a valid lens. -isum_lns :: Lens [Int] [Int] -isum_lns = cata_lns _L f - where f = inn_lns .< (id_lns -|-< fstmapadd) - fstmapadd :: Lens (Int,[Int]) (Int,[Int]) - fstmapadd = Lens get' put' create' - where get' = fst /\ (\(i,l) -> map (+i) l) - put' = create' . fst - create' (i,l) = (i,map (\x -> x-i) l) +-- * Partial lenses + +-- | Replicate a value n times. +-- Fails when the target list is not a replication. +replicate_lns :: Eq a => a -> Lens (a,Nat) [a] +replicate_lns v = varlens l v gen + where l x = ana_lns _L $ (snd_lns (const x) -|-< assocr_lns .< ((id_lns /\< id_lns) ><< id_lns)) .< distr_lns .< (id_lns ><< out_lns) + gen [] = v + gen (x:xs) = x + +-- Concatenates lists of replicated values. +replicatel_lns :: (Show a,Eq a) => Lens [(a,Nat)] [a] +replicatel_lns = hylo_lns (ann :: Ann (NeList One [a])) g h + where g = inn_lns .< (id_lns #\/< out_lns) .< (id_lns -|-< catrep_lns) + h = (id_lns -|-< replicate_lns _L ><< id_lns) .< out_lns + +-- | List concatenation with a special create. +-- For create, split to the left all equal values from the beginning of the list +catrep_lns :: Eq a => Lens ([a],[a]) [a] +catrep_lns = varlens l _L gen + where l x = cat_lns' ((==x) . fst) + gen [] = _L + gen (x:xs) = x + +-- ** Sieving to keep only each second element of a list + +sieve_lns :: a -> Lens [a] [a] +sieve_lns x = ana_lns _L g + where g = ((id_lns .\/< snd_lns _L) -|-< snd_lns (const x)) .< coassocl_lns .< (id_lns -|-< distr_lns .< (id_lns ><< out_lns)) .< out_lns + +-- ** Insertion sort + +-- | Sorts a list. +-- Fails when the target list is not sorted. +isort_lns :: Ord a => Lens [a] [a] +isort_lns = cata_lns _L f + where f = inn_lns .< (id_lns -|-< insert_lns) + +insert_lns :: Ord a => Lens (a,[a]) (a,[a]) +insert_lns = hylo_lns (ann :: Ann (NeList (a,[a]) a)) g h + where g = (id_lns ><< neecons_lns) .< undistr_lns + --inn_lns .< inr_lns .< (id_lns .\/< id_lns) + h = ((id_lns ><< inn_lns) .< undistr_lns -|-< subr_lns) .< coassocl_lns + .< (id_lns -|-< (?.<) p) .< distr_lns .< (id_lns ><< out_lns) + p = le . (id >< fst) + le = uncurry (<=) + +neecons_lns :: Lens (Either [a] (a,[a])) [a] +neecons_lns = inn_lns .< (id_lns -|-< (id_lns .\/< id_lns)) .< coassocr_lns .< (out_lns -|-< id_lns) diff --git a/src/Generics/Pointless/Lenses/Examples/Imdb.hs b/src/Generics/Pointless/Lenses/Examples/Imdb.hs --- a/src/Generics/Pointless/Lenses/Examples/Imdb.hs +++ b/src/Generics/Pointless/Lenses/Examples/Imdb.hs @@ -23,6 +23,7 @@ import Generics.Pointless.Lenses.Combinators import Generics.Pointless.Lenses import Generics.Pointless.Lenses.Examples.Recs +import Generics.Pointless.Lenses.Examples.Examples type Imdb = ([Show],[Actor]) type Show = (((Year,Title),[Review]),Either Movie TV) @@ -77,7 +78,7 @@ g = id_lns ><< (movie -|-< tv) boxoffices :: (Lens [BoxOffice] Value) -boxoffices = suml_pf .< filter_right_pf .< map_pf (outMaybe_lns .< snd_lns dcountry) +boxoffices = sumn_lns .< filter_right_pf .< map_pf (outMaybe_lns .< snd_lns dcountry) reviews :: (Lens [Review] Nat) reviews = length_pf dcomment .< concat_pf .< map_pf (snd_lns duser) diff --git a/src/Generics/Pointless/Lenses/Examples/MapExamples.hs b/src/Generics/Pointless/Lenses/Examples/MapExamples.hs --- a/src/Generics/Pointless/Lenses/Examples/MapExamples.hs +++ b/src/Generics/Pointless/Lenses/Examples/MapExamples.hs @@ -81,7 +81,7 @@ create' (Succ n) = ("woman",F) : create' n put' (Zero,[]) = [] put' (n,(nm,M):ps) = (nm,M) : put' (n,ps) - put' (Zero,_) = [] + put' (Zero,(nm,F):ps) = put' (Zero,ps) put' (Succ n,[]) = ("woman",F) : create' n put' (Succ n,(nm,F):ps) = (nm,F) : put' (n,ps) diff --git a/src/Generics/Pointless/Lenses/Examples/Recs.hs b/src/Generics/Pointless/Lenses/Examples/Recs.hs --- a/src/Generics/Pointless/Lenses/Examples/Recs.hs +++ b/src/Generics/Pointless/Lenses/Examples/Recs.hs @@ -187,8 +187,8 @@ where f = innNat_lns .< (outNat_lns \/$< id_lns) g = (snd_lns bang -|-< id_lns) .< distl_lns .< (outNat_lns ><< id_lns) -suml_pf :: Lens [Nat] Nat -suml_pf = cataList_lns (innNat_lns .< (id_lns #\/< (outNat_lns .< plus_pf))) +sum_pf :: Lens [Nat] Nat +sum_pf = cataList_lns (innNat_lns .< (id_lns #\/< (outNat_lns .< plus_pf))) cat_pf :: Lens ([a],[a]) [a] cat_pf = hyloNeList_lns g h diff --git a/src/Generics/Pointless/Lenses/PartialCombinators.hs b/src/Generics/Pointless/Lenses/PartialCombinators.hs new file mode 100644 --- /dev/null +++ b/src/Generics/Pointless/Lenses/PartialCombinators.hs @@ -0,0 +1,65 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Generics.Pointless.Lenses.PartialCombinators +-- Copyright : (c) 2011 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 provides unsafe, non-total point-free combinators as lenses. +-- +----------------------------------------------------------------------------- + +module Generics.Pointless.Lenses.PartialCombinators where + +import Generics.Pointless.Lenses +import Generics.Pointless.Lenses.Combinators +import Generics.Pointless.Lenses.RecursionPatterns +import Generics.Pointless.Combinators + +-- | Split +infix 6 /\< +(/\<) :: Eq a => (Lens a b) -> (Lens a c) -> Lens a (b,c) +(/\<) f g = Lens get' put' create' + where get' = get f /\ get g + put' = aux . (put f . (fst >< id) /\ put g . (snd >< id)) + create' = aux . (create f >< create g) + aux = (fst \/ error "/\\<: failed equality test") . (eq?) + +-- | Left Injection +inl_lns :: Lens a (Either a b) +inl_lns = Lens inl put' create' + where put' = create' . fst + create' = id \/ error "inl_lns: branching changed" + +-- | Right injection +inr_lns :: Lens b (Either a b) +inr_lns = Lens inr put' create' + where put' = create' . fst + create' = error "inr_lns: branching changed" \/ id + +-- | The converse of a left injection +inlconv_lns :: Lens (Either a b) a +inlconv_lns = Lens (id \/ error "inlconv_lns") put' create' + where put' = create' . fst + create' = inl + +-- | The converse of a right injection +inrconv_lns :: Lens (Either a b) b +inrconv_lns = Lens (error "inrconv_lns" \/ id) put' create' + where put' = create' . fst + create' = inr + +-- | Conditional lens +infix 0 ?.< +(?.<) :: (a -> Bool) -> Lens a (Either a a) +(?.<) p = Lens get' put' create' + where get' = (p?) + put' = create' . fst + create' (Left l) = if p l then l else error "?.<: branching changed" + create' (Right r) = if p r then error "?.<: branching changed" else r diff --git a/src/Generics/Pointless/Lenses/Reader/RecursionPatterns.hs b/src/Generics/Pointless/Lenses/Reader/RecursionPatterns.hs deleted file mode 100644 --- a/src/Generics/Pointless/Lenses/Reader/RecursionPatterns.hs +++ /dev/null @@ -1,137 +0,0 @@ - ------------------------------------------------------------------------------ --- | --- 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 - - diff --git a/src/Generics/Pointless/Lenses/RecursionPatterns.hs b/src/Generics/Pointless/Lenses/RecursionPatterns.hs --- a/src/Generics/Pointless/Lenses/RecursionPatterns.hs +++ b/src/Generics/Pointless/Lenses/RecursionPatterns.hs @@ -32,52 +32,48 @@ inn_lns :: Mu a => Lens (F a a) a inn_lns = Lens inn (out . fst) out +inn_lns' :: Mu a => Ann a -> Lens (F a a) a +inn_lns' _ = Lens inn (out . fst) out + -- | The @out@ point-free combinator. out_lns :: Mu a => Lens a (F a a) out_lns = Lens out (inn . fst) inn +out_lns' :: Mu a => Ann 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' +fmap_lns :: Fctrable f => Ann (Fix f) -> Lens c a -> Lens (Rep f c) (Rep f a) +fmap_lns f l = Lens get' put' create' where get' = fmap f (get l) - put' = fmap f (put l) . fzip (fctr :: Fctr f) (create l) + put' = fmap f (put l) . fzip 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 @hylo@ recursion pattern as the composition of a lens catamorphism after a lens anamorphism . -hylo_lns :: (Mu b,Fctrable (PF b)) => b -> Lens (F b c) c -> Lens a (F b a) -> Lens a c +hylo_lns :: (Mu b,Fctrable (PF b)) => Ann b -> Lens (F b c) c -> Lens a (F b a) -> Lens a c hylo_lns b g h = cata_lns b g .< ana_lns b h -- | 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' +ana_lns :: (Mu b,Fctrable (PF b)) => Ann b -> Lens a (F b a) -> Lens a b +ana_lns (b::Ann 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) + g = ann :: Ann (Fix (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' +cata_lns :: (Mu a,Fctrable (PF a)) => Ann a -> (Lens (F a b) b) -> Lens a b +cata_lns (a::Ann 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)) + put' = ana a (fzip f create' . (put l . (id >< fmap f get') /\ snd) . (id >< out)) create' = ana a (create l) - f = fctr :: Fctr (PF a) + f = ann :: Ann (Fix (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 :: (Mu a,Mu b,Fctrable (PF b)) => Ann 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) @@ -87,32 +83,20 @@ 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' +bmap_lns :: Bifctrable f => Ann (BFix f) -> Lens c a -> NatLens (BRep f c) (BRep f a) +bmap_lns (f::Ann (BFix f)) l (x::Ann 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) + put' = bmap f (put l) idx . bzip x 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) + => Ann (d a) -> Lens c a -> Lens (d c) (d a) +gmap_lns (da::Ann (d a)) l = cata_lns _L (inn_lns .< (bmap_lns f l) da) + where f = ann :: Ann (BFix (BF d))