{-| A zipper is a structure for walking a value and manipulating it in constant time. This module was inspired by the paper: /Michael D. Adams. Scrap Your Zippers: A Generic Zipper for Heterogeneous Types, Workshop on Generic Programming 2010/. -} module Data.Generics.Uniplate.Zipper( -- * Create a zipper and get back the value Zipper, zipper, zipperBi, fromZipper, -- * Navigate within a zipper left, right, up, down, -- * Manipulate the zipper hole hole, replaceHole ) where import Data.Generics.Uniplate.Operations import Data.Generics.Str import Control.Monad import Data.Maybe -- | Create a zipper, focused on the top-left value. zipper :: Uniplate to => to -> Zipper to to zipper :: to -> Zipper to to zipper = Maybe (Zipper to to) -> Zipper to to forall a. HasCallStack => Maybe a -> a fromJust (Maybe (Zipper to to) -> Zipper to to) -> (to -> Maybe (Zipper to to)) -> to -> Zipper to to forall b c a. (b -> c) -> (a -> b) -> a -> c . (to -> (Str to, Str to -> to)) -> to -> Maybe (Zipper to to) forall to from. Uniplate to => (from -> (Str to, Str to -> from)) -> from -> Maybe (Zipper from to) toZipper (\to x -> (to -> Str to forall a. a -> Str a One to x, \(One to x) -> to x)) -- | Create a zipper with a different focus type from the outer type. Will return -- @Nothing@ if there are no instances of the focus type within the original value. zipperBi :: Biplate from to => from -> Maybe (Zipper from to) zipperBi :: from -> Maybe (Zipper from to) zipperBi = (from -> (Str to, Str to -> from)) -> from -> Maybe (Zipper from to) forall to from. Uniplate to => (from -> (Str to, Str to -> from)) -> from -> Maybe (Zipper from to) toZipper from -> (Str to, Str to -> from) forall from to. Biplate from to => from -> (Str to, Str to -> from) biplate -- | Zipper structure, whose root type is the first type argument, and whose -- focus type is the second type argument. data Zipper from to = Zipper {Zipper from to -> Str to -> from reform :: Str to -> from ,Zipper from to -> ZipN to zipp :: ZipN to } rezipp :: (ZipN to -> f (ZipN to)) -> Zipper from to -> f (Zipper from to) rezipp ZipN to -> f (ZipN to) f (Zipper Str to -> from a ZipN to b) = (ZipN to -> Zipper from to) -> f (ZipN to) -> f (Zipper from to) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap ((Str to -> from) -> ZipN to -> Zipper from to forall from to. (Str to -> from) -> ZipN to -> Zipper from to Zipper Str to -> from a) (f (ZipN to) -> f (Zipper from to)) -> f (ZipN to) -> f (Zipper from to) forall a b. (a -> b) -> a -> b $ ZipN to -> f (ZipN to) f ZipN to b instance (Eq from, Eq to) => Eq (Zipper from to) where Zipper from to a == :: Zipper from to -> Zipper from to -> Bool == Zipper from to b = Zipper from to -> from forall from to. Zipper from to -> from fromZipper Zipper from to a from -> from -> Bool forall a. Eq a => a -> a -> Bool == Zipper from to -> from forall from to. Zipper from to -> from fromZipper Zipper from to b Bool -> Bool -> Bool && Zipper from to -> ZipN to forall from to. Zipper from to -> ZipN to zipp Zipper from to a ZipN to -> ZipN to -> Bool forall a. Eq a => a -> a -> Bool == Zipper from to -> ZipN to forall from to. Zipper from to -> ZipN to zipp Zipper from to b toZipper :: Uniplate to => (from -> (Str to, Str to -> from)) -> from -> Maybe (Zipper from to) toZipper :: (from -> (Str to, Str to -> from)) -> from -> Maybe (Zipper from to) toZipper from -> (Str to, Str to -> from) biplate from x = (ZipN to -> Zipper from to) -> Maybe (ZipN to) -> Maybe (Zipper from to) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap ((Str to -> from) -> ZipN to -> Zipper from to forall from to. (Str to -> from) -> ZipN to -> Zipper from to Zipper Str to -> from gen) (Maybe (ZipN to) -> Maybe (Zipper from to)) -> Maybe (ZipN to) -> Maybe (Zipper from to) forall a b. (a -> b) -> a -> b $ Str to -> Maybe (ZipN to) forall x. Str x -> Maybe (ZipN x) zipN Str to cs where (Str to cs,Str to -> from gen) = from -> (Str to, Str to -> from) biplate from x -- | From a zipper take the whole structure, including any modifications. fromZipper :: Zipper from to -> from fromZipper :: Zipper from to -> from fromZipper Zipper from to x = Zipper from to -> Str to -> from forall from to. Zipper from to -> Str to -> from reform Zipper from to x (Str to -> from) -> Str to -> from forall a b. (a -> b) -> a -> b $ Zip1 to -> Str to forall a. Zip1 a -> Str a top1 (Zip1 to -> Str to) -> Zip1 to -> Str to forall a b. (a -> b) -> a -> b $ ZipN to -> Zip1 to forall a. ZipN a -> Zip1 a topN (ZipN to -> Zip1 to) -> ZipN to -> Zip1 to forall a b. (a -> b) -> a -> b $ Zipper from to -> ZipN to forall from to. Zipper from to -> ZipN to zipp Zipper from to x -- | Move one step left from the current position. left :: Zipper from to -> Maybe (Zipper from to) left :: Zipper from to -> Maybe (Zipper from to) left = (ZipN to -> Maybe (ZipN to)) -> Zipper from to -> Maybe (Zipper from to) forall (f :: * -> *) to from. Functor f => (ZipN to -> f (ZipN to)) -> Zipper from to -> f (Zipper from to) rezipp ZipN to -> Maybe (ZipN to) forall a. ZipN a -> Maybe (ZipN a) leftN -- | Move one step right from the current position. right :: Zipper from to -> Maybe (Zipper from to) right :: Zipper from to -> Maybe (Zipper from to) right = (ZipN to -> Maybe (ZipN to)) -> Zipper from to -> Maybe (Zipper from to) forall (f :: * -> *) to from. Functor f => (ZipN to -> f (ZipN to)) -> Zipper from to -> f (Zipper from to) rezipp ZipN to -> Maybe (ZipN to) forall a. ZipN a -> Maybe (ZipN a) rightN -- | Move one step down from the current position. down :: Uniplate to => Zipper from to -> Maybe (Zipper from to) down :: Zipper from to -> Maybe (Zipper from to) down = (ZipN to -> Maybe (ZipN to)) -> Zipper from to -> Maybe (Zipper from to) forall (f :: * -> *) to from. Functor f => (ZipN to -> f (ZipN to)) -> Zipper from to -> f (Zipper from to) rezipp ZipN to -> Maybe (ZipN to) forall x. Uniplate x => ZipN x -> Maybe (ZipN x) downN -- | Move one step up from the current position. up :: Zipper from to -> Maybe (Zipper from to) up :: Zipper from to -> Maybe (Zipper from to) up = (ZipN to -> Maybe (ZipN to)) -> Zipper from to -> Maybe (Zipper from to) forall (f :: * -> *) to from. Functor f => (ZipN to -> f (ZipN to)) -> Zipper from to -> f (Zipper from to) rezipp ZipN to -> Maybe (ZipN to) forall a. ZipN a -> Maybe (ZipN a) upN -- | Retrieve the current focus of the zipper.. hole :: Zipper from to -> to hole :: Zipper from to -> to hole = ZipN to -> to forall a. ZipN a -> a holeN (ZipN to -> to) -> (Zipper from to -> ZipN to) -> Zipper from to -> to forall b c a. (b -> c) -> (a -> b) -> a -> c . Zipper from to -> ZipN to forall from to. Zipper from to -> ZipN to zipp -- | Replace the value currently at the focus of the zipper. replaceHole :: to -> Zipper from to -> Zipper from to replaceHole :: to -> Zipper from to -> Zipper from to replaceHole to x Zipper from to z = Zipper from to z{zipp :: ZipN to zipp=to -> ZipN to -> ZipN to forall a. a -> ZipN a -> ZipN a replaceN to x (Zipper from to -> ZipN to forall from to. Zipper from to -> ZipN to zipp Zipper from to z)} --------------------------------------------------------------------- -- N LEVEL ZIPPER ON Str data ZipN x = ZipN [Str x -> Zip1 x] (Zip1 x) instance Eq x => Eq (ZipN x) where x :: ZipN x x@(ZipN [Str x -> Zip1 x] _ Zip1 x xx) == :: ZipN x -> ZipN x -> Bool == y :: ZipN x y@(ZipN [Str x -> Zip1 x] _ Zip1 x yy) = Zip1 x xx Zip1 x -> Zip1 x -> Bool forall a. Eq a => a -> a -> Bool == Zip1 x yy Bool -> Bool -> Bool && ZipN x -> Maybe (ZipN x) forall a. ZipN a -> Maybe (ZipN a) upN ZipN x x Maybe (ZipN x) -> Maybe (ZipN x) -> Bool forall a. Eq a => a -> a -> Bool == ZipN x -> Maybe (ZipN x) forall a. ZipN a -> Maybe (ZipN a) upN ZipN x y zipN :: Str x -> Maybe (ZipN x) zipN :: Str x -> Maybe (ZipN x) zipN Str x x = (Zip1 x -> ZipN x) -> Maybe (Zip1 x) -> Maybe (ZipN x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap ([Str x -> Zip1 x] -> Zip1 x -> ZipN x forall x. [Str x -> Zip1 x] -> Zip1 x -> ZipN x ZipN []) (Maybe (Zip1 x) -> Maybe (ZipN x)) -> Maybe (Zip1 x) -> Maybe (ZipN x) forall a b. (a -> b) -> a -> b $ Str x -> Maybe (Zip1 x) forall x. Str x -> Maybe (Zip1 x) zip1 Str x x leftN :: ZipN a -> Maybe (ZipN a) leftN (ZipN [Str a -> Zip1 a] p Zip1 a x) = (Zip1 a -> ZipN a) -> Maybe (Zip1 a) -> Maybe (ZipN a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap ([Str a -> Zip1 a] -> Zip1 a -> ZipN a forall x. [Str x -> Zip1 x] -> Zip1 x -> ZipN x ZipN [Str a -> Zip1 a] p) (Maybe (Zip1 a) -> Maybe (ZipN a)) -> Maybe (Zip1 a) -> Maybe (ZipN a) forall a b. (a -> b) -> a -> b $ Zip1 a -> Maybe (Zip1 a) forall a. Zip1 a -> Maybe (Zip1 a) left1 Zip1 a x rightN :: ZipN a -> Maybe (ZipN a) rightN (ZipN [Str a -> Zip1 a] p Zip1 a x) = (Zip1 a -> ZipN a) -> Maybe (Zip1 a) -> Maybe (ZipN a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap ([Str a -> Zip1 a] -> Zip1 a -> ZipN a forall x. [Str x -> Zip1 x] -> Zip1 x -> ZipN x ZipN [Str a -> Zip1 a] p) (Maybe (Zip1 a) -> Maybe (ZipN a)) -> Maybe (Zip1 a) -> Maybe (ZipN a) forall a b. (a -> b) -> a -> b $ Zip1 a -> Maybe (Zip1 a) forall a. Zip1 a -> Maybe (Zip1 a) right1 Zip1 a x holeN :: ZipN a -> a holeN (ZipN [Str a -> Zip1 a] _ Zip1 a x) = Zip1 a -> a forall a. Zip1 a -> a hole1 Zip1 a x replaceN :: a -> ZipN a -> ZipN a replaceN a v (ZipN [Str a -> Zip1 a] p Zip1 a x) = [Str a -> Zip1 a] -> Zip1 a -> ZipN a forall x. [Str x -> Zip1 x] -> Zip1 x -> ZipN x ZipN [Str a -> Zip1 a] p (Zip1 a -> ZipN a) -> Zip1 a -> ZipN a forall a b. (a -> b) -> a -> b $ Zip1 a -> a -> Zip1 a forall a. Zip1 a -> a -> Zip1 a replace1 Zip1 a x a v upN :: ZipN a -> Maybe (ZipN a) upN (ZipN [] Zip1 a x) = Maybe (ZipN a) forall a. Maybe a Nothing upN (ZipN (Str a -> Zip1 a p:[Str a -> Zip1 a] ps) Zip1 a x) = ZipN a -> Maybe (ZipN a) forall a. a -> Maybe a Just (ZipN a -> Maybe (ZipN a)) -> ZipN a -> Maybe (ZipN a) forall a b. (a -> b) -> a -> b $ [Str a -> Zip1 a] -> Zip1 a -> ZipN a forall x. [Str x -> Zip1 x] -> Zip1 x -> ZipN x ZipN [Str a -> Zip1 a] ps (Zip1 a -> ZipN a) -> Zip1 a -> ZipN a forall a b. (a -> b) -> a -> b $ Str a -> Zip1 a p (Str a -> Zip1 a) -> Str a -> Zip1 a forall a b. (a -> b) -> a -> b $ Zip1 a -> Str a forall a. Zip1 a -> Str a top1 Zip1 a x topN :: ZipN a -> Zip1 a topN (ZipN [] Zip1 a x) = Zip1 a x topN ZipN a x = ZipN a -> Zip1 a topN (ZipN a -> Zip1 a) -> ZipN a -> Zip1 a forall a b. (a -> b) -> a -> b $ Maybe (ZipN a) -> ZipN a forall a. HasCallStack => Maybe a -> a fromJust (Maybe (ZipN a) -> ZipN a) -> Maybe (ZipN a) -> ZipN a forall a b. (a -> b) -> a -> b $ ZipN a -> Maybe (ZipN a) forall a. ZipN a -> Maybe (ZipN a) upN ZipN a x downN :: Uniplate x => ZipN x -> Maybe (ZipN x) downN :: ZipN x -> Maybe (ZipN x) downN (ZipN [Str x -> Zip1 x] ps Zip1 x x) = (Zip1 x -> ZipN x) -> Maybe (Zip1 x) -> Maybe (ZipN x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap ([Str x -> Zip1 x] -> Zip1 x -> ZipN x forall x. [Str x -> Zip1 x] -> Zip1 x -> ZipN x ZipN ([Str x -> Zip1 x] -> Zip1 x -> ZipN x) -> [Str x -> Zip1 x] -> Zip1 x -> ZipN x forall a b. (a -> b) -> a -> b $ Zip1 x -> x -> Zip1 x forall a. Zip1 a -> a -> Zip1 a replace1 Zip1 x x (x -> Zip1 x) -> (Str x -> x) -> Str x -> Zip1 x forall b c a. (b -> c) -> (a -> b) -> a -> c . Str x -> x gen (Str x -> Zip1 x) -> [Str x -> Zip1 x] -> [Str x -> Zip1 x] forall a. a -> [a] -> [a] : [Str x -> Zip1 x] ps) (Maybe (Zip1 x) -> Maybe (ZipN x)) -> Maybe (Zip1 x) -> Maybe (ZipN x) forall a b. (a -> b) -> a -> b $ Str x -> Maybe (Zip1 x) forall x. Str x -> Maybe (Zip1 x) zip1 Str x cs where (Str x cs,Str x -> x gen) = x -> (Str x, Str x -> x) forall on. Uniplate on => on -> (Str on, Str on -> on) uniplate (x -> (Str x, Str x -> x)) -> x -> (Str x, Str x -> x) forall a b. (a -> b) -> a -> b $ Zip1 x -> x forall a. Zip1 a -> a hole1 Zip1 x x --------------------------------------------------------------------- -- 1 LEVEL ZIPPER ON Str data Diff1 a = TwoLeft (Str a) | TwoRight (Str a) deriving Diff1 a -> Diff1 a -> Bool (Diff1 a -> Diff1 a -> Bool) -> (Diff1 a -> Diff1 a -> Bool) -> Eq (Diff1 a) forall a. Eq a => Diff1 a -> Diff1 a -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Diff1 a -> Diff1 a -> Bool $c/= :: forall a. Eq a => Diff1 a -> Diff1 a -> Bool == :: Diff1 a -> Diff1 a -> Bool $c== :: forall a. Eq a => Diff1 a -> Diff1 a -> Bool Eq undiff1 :: Str a -> Diff1 a -> Str a undiff1 Str a r (TwoLeft Str a l) = Str a -> Str a -> Str a forall a. Str a -> Str a -> Str a Two Str a l Str a r undiff1 Str a l (TwoRight Str a r) = Str a -> Str a -> Str a forall a. Str a -> Str a -> Str a Two Str a l Str a r -- Warning: this definition of Eq may look too strong (Str Left/Right is not relevant) -- but you don't know what the uniplate.gen function will do data Zip1 a = Zip1 [Diff1 a] a deriving Zip1 a -> Zip1 a -> Bool (Zip1 a -> Zip1 a -> Bool) -> (Zip1 a -> Zip1 a -> Bool) -> Eq (Zip1 a) forall a. Eq a => Zip1 a -> Zip1 a -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Zip1 a -> Zip1 a -> Bool $c/= :: forall a. Eq a => Zip1 a -> Zip1 a -> Bool == :: Zip1 a -> Zip1 a -> Bool $c== :: forall a. Eq a => Zip1 a -> Zip1 a -> Bool Eq zip1 :: Str x -> Maybe (Zip1 x) zip1 :: Str x -> Maybe (Zip1 x) zip1 = Bool -> [Diff1 x] -> Str x -> Maybe (Zip1 x) forall a. Bool -> [Diff1 a] -> Str a -> Maybe (Zip1 a) insert1 Bool True [] insert1 :: Bool -> [Diff1 a] -> Str a -> Maybe (Zip1 a) insert1 :: Bool -> [Diff1 a] -> Str a -> Maybe (Zip1 a) insert1 Bool leftmost [Diff1 a] c Str a Zero = Maybe (Zip1 a) forall a. Maybe a Nothing insert1 Bool leftmost [Diff1 a] c (One a x) = Zip1 a -> Maybe (Zip1 a) forall a. a -> Maybe a Just (Zip1 a -> Maybe (Zip1 a)) -> Zip1 a -> Maybe (Zip1 a) forall a b. (a -> b) -> a -> b $ [Diff1 a] -> a -> Zip1 a forall a. [Diff1 a] -> a -> Zip1 a Zip1 [Diff1 a] c a x insert1 Bool leftmost [Diff1 a] c (Two Str a l Str a r) = if Bool leftmost then Maybe (Zip1 a) ll Maybe (Zip1 a) -> Maybe (Zip1 a) -> Maybe (Zip1 a) forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a `mplus` Maybe (Zip1 a) rr else Maybe (Zip1 a) rr Maybe (Zip1 a) -> Maybe (Zip1 a) -> Maybe (Zip1 a) forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a `mplus` Maybe (Zip1 a) ll where ll :: Maybe (Zip1 a) ll = Bool -> [Diff1 a] -> Str a -> Maybe (Zip1 a) forall a. Bool -> [Diff1 a] -> Str a -> Maybe (Zip1 a) insert1 Bool leftmost (Str a -> Diff1 a forall a. Str a -> Diff1 a TwoRight Str a rDiff1 a -> [Diff1 a] -> [Diff1 a] forall a. a -> [a] -> [a] :[Diff1 a] c) Str a l rr :: Maybe (Zip1 a) rr = Bool -> [Diff1 a] -> Str a -> Maybe (Zip1 a) forall a. Bool -> [Diff1 a] -> Str a -> Maybe (Zip1 a) insert1 Bool leftmost (Str a -> Diff1 a forall a. Str a -> Diff1 a TwoLeft Str a lDiff1 a -> [Diff1 a] -> [Diff1 a] forall a. a -> [a] -> [a] :[Diff1 a] c) Str a r left1, right1 :: Zip1 a -> Maybe (Zip1 a) left1 :: Zip1 a -> Maybe (Zip1 a) left1 = Bool -> Zip1 a -> Maybe (Zip1 a) forall a. Bool -> Zip1 a -> Maybe (Zip1 a) move1 Bool True right1 :: Zip1 a -> Maybe (Zip1 a) right1 = Bool -> Zip1 a -> Maybe (Zip1 a) forall a. Bool -> Zip1 a -> Maybe (Zip1 a) move1 Bool False move1 :: Bool -> Zip1 a -> Maybe (Zip1 a) move1 :: Bool -> Zip1 a -> Maybe (Zip1 a) move1 Bool leftward (Zip1 [Diff1 a] p a x) = [Diff1 a] -> Str a -> Maybe (Zip1 a) forall a. [Diff1 a] -> Str a -> Maybe (Zip1 a) f [Diff1 a] p (Str a -> Maybe (Zip1 a)) -> Str a -> Maybe (Zip1 a) forall a b. (a -> b) -> a -> b $ a -> Str a forall a. a -> Str a One a x where f :: [Diff1 a] -> Str a -> Maybe (Zip1 a) f [Diff1 a] p Str a x = [Maybe (Zip1 a)] -> Maybe (Zip1 a) forall (t :: * -> *) (m :: * -> *) a. (Foldable t, MonadPlus m) => t (m a) -> m a msum ([Maybe (Zip1 a)] -> Maybe (Zip1 a)) -> [Maybe (Zip1 a)] -> Maybe (Zip1 a) forall a b. (a -> b) -> a -> b $ [Bool -> [Diff1 a] -> Str a -> Maybe (Zip1 a) forall a. Bool -> [Diff1 a] -> Str a -> Maybe (Zip1 a) insert1 Bool False (Str a -> Diff1 a forall a. Str a -> Diff1 a TwoRight Str a xDiff1 a -> [Diff1 a] -> [Diff1 a] forall a. a -> [a] -> [a] :[Diff1 a] ps) Str a l | TwoLeft Str a l:[Diff1 a] ps <- [[Diff1 a] p], Bool leftward] [Maybe (Zip1 a)] -> [Maybe (Zip1 a)] -> [Maybe (Zip1 a)] forall a. [a] -> [a] -> [a] ++ [Bool -> [Diff1 a] -> Str a -> Maybe (Zip1 a) forall a. Bool -> [Diff1 a] -> Str a -> Maybe (Zip1 a) insert1 Bool True (Str a -> Diff1 a forall a. Str a -> Diff1 a TwoLeft Str a xDiff1 a -> [Diff1 a] -> [Diff1 a] forall a. a -> [a] -> [a] :[Diff1 a] ps) Str a r | TwoRight Str a r:[Diff1 a] ps <- [[Diff1 a] p], Bool -> Bool not Bool leftward] [Maybe (Zip1 a)] -> [Maybe (Zip1 a)] -> [Maybe (Zip1 a)] forall a. [a] -> [a] -> [a] ++ [[Diff1 a] -> Str a -> Maybe (Zip1 a) f [Diff1 a] ps (Str a x Str a -> Diff1 a -> Str a forall a. Str a -> Diff1 a -> Str a `undiff1` Diff1 a p) | Diff1 a p:[Diff1 a] ps <- [[Diff1 a] p]] top1 :: Zip1 a -> Str a top1 :: Zip1 a -> Str a top1 (Zip1 [Diff1 a] p a x) = [Diff1 a] -> Str a -> Str a forall a. [Diff1 a] -> Str a -> Str a f [Diff1 a] p (a -> Str a forall a. a -> Str a One a x) where f :: [Diff1 a] -> Str a -> Str a f :: [Diff1 a] -> Str a -> Str a f [] Str a x = Str a x f (Diff1 a p:[Diff1 a] ps) Str a x = [Diff1 a] -> Str a -> Str a forall a. [Diff1 a] -> Str a -> Str a f [Diff1 a] ps (Str a x Str a -> Diff1 a -> Str a forall a. Str a -> Diff1 a -> Str a `undiff1` Diff1 a p) hole1 :: Zip1 a -> a hole1 :: Zip1 a -> a hole1 (Zip1 [Diff1 a] _ a x) = a x -- this way round so the a can be disguarded quickly replace1 :: Zip1 a -> a -> Zip1 a replace1 :: Zip1 a -> a -> Zip1 a replace1 (Zip1 [Diff1 a] p a _) = [Diff1 a] -> a -> Zip1 a forall a. [Diff1 a] -> a -> Zip1 a Zip1 [Diff1 a] p