CartesianStore as a zipper.

multiplatezipper2.hs

{-# LANGUAGE TypeOperators, RankNTypes, GADTs #-}

import Control.Applicative
import Data.Type.Equality
import Control.Monad
import Control.Monad.Free
import Control.Comonad
import Control.Comonad.Trans.Store
import Data.Functor.Identity
import Data.Functor.Compose


type Plate fam f = forall x. fam x -> x -> f x

class EqT fam => Multiplate fam where
  multiplate :: Applicative f => Plate fam f -> Plate fam f


data Zipper fam a where
  Unit :: a -> Zipper fam a
  Battery :: Zipper fam (b -> a) -> fam b -> b -> Zipper fam a

instance Functor (Zipper fam) where
  fmap f (Unit a) = Unit (f a)
  fmap f (Battery v w b) = Battery (fmap (f .) v) w b

instance Applicative (Zipper fam) where
  pure = Unit
  f <*> Unit a = fmap ($ a) f
  f <*> Battery v w b = Battery ((.) <$> f <*> v) w b


zipperPlate :: Multiplate fam => Plate fam (Zipper fam)
zipperPlate = multiplate (Battery (Unit id))

enter :: Multiplate fam => fam a -> a -> Zipper fam a
enter = zipperPlate

next :: Zipper fam a -> Zipper fam a
next (Unit a) = Unit a
next (Battery v _ b) = v <*> pure b

leave :: Zipper fam a -> a
leave (Unit a) = a
leave (Battery v _ b) = leave (v <*> pure b)

get :: Multiplate fam => fam b -> Zipper fam a -> Maybe b
get _ (Unit _) = Nothing
get w (Battery _ w' b) = (\Refl -> b) <$> (w `eqT` w')

set :: Multiplate fam => fam b -> b -> Zipper fam a -> Zipper fam a
set w b = modify w (const b)

modify :: Multiplate fam => fam b -> (b -> b) -> Zipper fam a -> Zipper fam a
modify _ _ (Unit a) = Unit a
modify w f (Battery v w' b) = Battery v w' (maybe b (\Refl -> f b) (w `eqT` w'))

visit :: Multiplate fam => fam a -> (Zipper fam a -> Zipper fam a) -> a -> a
visit w f = leave . f . enter w

modVisit :: Multiplate fam => fam b -> (Zipper fam b -> Zipper fam b) -> Zipper fam a -> Zipper fam a
modVisit w = modify w . visit w



data Expr = Con Int
          | Add Expr Expr
          | Mul Expr Expr
          | EVar Var
          | Let Decl Expr
          deriving (Eq, Show)

data Decl = Var := Expr
          | Seq Decl Decl
          deriving (Eq, Show)

type Var = String

data Fam a where
  Expr :: Fam Expr
  Decl :: Fam Decl

instance EqT Fam where

  eqT Expr Expr = Just Refl
  eqT Decl Decl = Just Refl
  eqT _ _ = Nothing

instance Multiplate Fam where

  multiplate child Expr (Add e1 e2) = Add <$> child Expr e1 <*> child Expr e2
  multiplate child Expr (Mul e1 e2) = Mul <$> child Expr e1 <*> child Expr e2
  multiplate child Expr (Let d e)   = Let <$> child Decl d <*> child Expr e
  multiplate _     Expr e           = pure e
  
  multiplate child Decl (v := e)    = (v :=) <$> child Expr e
  multiplate child Decl (Seq d1 d2) = Seq <$> child Decl d1 <*> child Decl d2


expr1 :: Expr
expr1 = Let ("x" := Con 42) (Let ("y" := Con 1) (Add (EVar "x") (EVar "x")))

expr2 :: Expr
expr2 = visit Expr (modVisit Expr (modVisit Decl (set Expr $ Con 2) . next)) expr1