Zipper Comonads, ogólnie

Biorąc pod uwagę dowolny typ kontenera, możemy utworzyć (skoncentrowany na elementach) Zipper i wiedzieć, że ta struktura jest Comonad. Zostało to niedawno zbadane ze wspaniałymi szczegółami w innym pytaniu o przepełnienie stosu dla następującego typu:

data Bin a = Branch (Bin a) a (Bin a) | Leaf a deriving Functor

z następującym zamkiem błyskawicznym

data Dir = L | R
data Step a = Step a Dir (Bin a)   deriving Functor
data Zip  a = Zip [Step a] (Bin a) deriving Functor
instance Comonad Zip where ...

To jest tak, że Zipto Comonadjednak budowa jego przykład jest trochę owłosione. To powiedziawszy, Zipmożna całkowicie wyprowadzić mechanicznie z Treei (jak sądzę) każdy typ wyprowadzony w ten sposób jest automatycznie a Comonad, więc uważam, że powinno być tak, że możemy konstruować te typy i ich kombinacje generalnie i automatycznie.

Jedną z metod uzyskania ogólnej konstrukcji zamka błyskawicznego jest użycie następującej klasy i rodziny typów

data Zipper t a = Zipper { diff :: D t a, here :: a }

deriving instance Diff t => Functor (Zipper t)

class (Functor t, Functor (D t)) => Diff t where
  data D t :: * -> *
  inTo  :: t a -> t (Zipper t a)
  outOf :: Zipper t a -> t a

które (mniej więcej) pojawiło się w wątkach Haskell Cafe i na blogu Conala Elliotta. Ta klasa może być utworzona dla różnych podstawowych typów algebraicznych, a tym samym zapewnia ogólne ramy do mówienia o pochodnych ADT.

Więc ostatecznie moje pytanie brzmi, czy możemy pisać, czy nie

instance Diff t => Comonad (Zipper t) where ...

które można wykorzystać do podciągnięcia określonej instancji Comonad opisanej powyżej:

instance Diff Bin where
  data D Bin a = DBin { context :: [Step a], descend :: Maybe (Bin a, Bin a) }
  ...

Niestety nie udało mi się napisać takiej instancji. Czy inTo/ outOfpodpis jest wystarczający? Czy jest coś innego, aby ograniczyć typy? Czy ta instancja jest w ogóle możliwa?

Podobnie jak łapacz dzieci w Chitty-Chitty-Bang-Bang wabiąc dzieci do niewoli słodyczami i zabawkami, rekruterzy do studiów licencjackich lubią wygłupiać się bańkami mydlanymi i bumerangami, ale kiedy drzwi się zatrzaskują, to „Dobra, dzieci, czas się uczyć o częściowym różniczkowaniu! ”. Ja też. Nie mów, że cię nie ostrzegałem.

Oto kolejne ostrzeżenie: następujący kod wymaga {-# LANGUAGE KitchenSink #-}, a raczej

{-# LANGUAGE TypeFamilies, FlexibleContexts, TupleSections, GADTs, DataKinds,
    TypeOperators, FlexibleInstances, RankNTypes, ScopedTypeVariables,
    StandaloneDeriving, UndecidableInstances #-}

w przypadkowej kolejności.

Funktory różniczkowalne dają komonadyczne zamki błyskawiczne

Czym właściwie jest różniczkowalny funktor?

class (Functor f, Functor (DF f)) => Diff1 f where
  type DF f :: * -> *
  upF      ::  ZF f x  ->  f x
  downF    ::  f x     ->  f (ZF f x)
  aroundF  ::  ZF f x  ->  ZF f (ZF f x)

data ZF f x = (:<-:) {cxF :: DF f x, elF :: x}

Jest to funktor, który ma pochodną, ​​która jest jednocześnie funktorem. Pochodna reprezentuje kontekst jednej dziury dla elementu . Typ zamka błyskawicznegoZF f x reprezentuje parę kontekstu z jednym otworem i element w otworze.

Operacje Diff1opisujące rodzaje nawigacji, jakie możemy wykonywać na zamkach błyskawicznych (bez pojęcia „w lewo” i „w prawo”, o których mowa w moim artykule Clowns and Jokers ). Możemy iść „w górę”, składając konstrukcję ponownie, wpinając element w jego otwór. Możemy zejść „w dół”, znajdując każdy sposób, aby odwiedzić element w podanej strukturze: dekorujemy każdy element jego kontekstem. Możemy chodzić „dookoła”, biorąc istniejący zamek błyskawiczny i dekorując każdy element jego kontekstem, aby znaleźć wszystkie sposoby ponownego ustawienia ostrości (i tego, jak zachować obecną koncentrację).

Teraz ten typ aroundFmoże niektórym z was przypominać

class Functor c => Comonad c where
  extract    :: c x -> x
  duplicate  :: c x -> c (c x)

i masz rację, aby otrzymać przypomnienie! Mamy, z przeskokiem i skokiem,

instance Diff1 f => Functor (ZF f) where
  fmap f (df :<-: x) = fmap f df :<-: f x

instance Diff1 f => Comonad (ZF f) where
  extract    = elF
  duplicate  = aroundF

i nalegamy na to

extract . duplicate == id
fmap extract . duplicate == id
duplicate . duplicate == fmap duplicate . duplicate

Tego też potrzebujemy

fmap extract (downF xs) == xs              -- downF decorates the element in position
fmap upF (downF xs) = fmap (const xs) xs   -- downF gives the correct context

Funktory wielomianowe są różniczkowalne

Stałe funktory są różniczkowalne.

data KF a x = KF a
instance Functor (KF a) where
  fmap f (KF a) = KF a

instance Diff1 (KF a) where
  type DF (KF a) = KF Void
  upF (KF w :<-: _) = absurd w
  downF (KF a) = KF a
  aroundF (KF w :<-: _) = absurd w

Nie ma gdzie umieścić elementu, więc nie można utworzyć kontekstu. Nie ma dokąd pójść upFani downFskąd, i łatwo nie znajdujemy żadnej drogi, do której można się udać downF.

Tożsamość funktor jest różniczkowalna.

data IF x = IF x
instance Functor IF where
  fmap f (IF x) = IF (f x)

instance Diff1 IF where
  type DF IF = KF ()
  upF (KF () :<-: x) = IF x
  downF (IF x) = IF (KF () :<-: x)
  aroundF z@(KF () :<-: x) = KF () :<-: z

Jest jeden element w trywialnym kontekście, downFznajduje go, upFprzepakowuje i aroundFmoże tylko pozostać na miejscu.

Suma zachowuje zróżnicowanie.

data (f :+: g) x = LF (f x) | RF (g x)
instance (Functor f, Functor g) => Functor (f :+: g) where
  fmap h (LF f) = LF (fmap h f)
  fmap h (RF g) = RF (fmap h g)

instance (Diff1 f, Diff1 g) => Diff1 (f :+: g) where
  type DF (f :+: g) = DF f :+: DF g
  upF (LF f' :<-: x) = LF (upF (f' :<-: x))
  upF (RF g' :<-: x) = RF (upF (g' :<-: x))

Inne kawałki to trochę więcej. Aby przejść downF, musimy wejść downFdo oznaczonego komponentu, a następnie naprawić powstałe zamki błyskawiczne, aby wyświetlić tag w kontekście.

  downF (LF f) = LF (fmap (\ (f' :<-: x) -> LF f' :<-: x) (downF f))
  downF (RF g) = RF (fmap (\ (g' :<-: x) -> RF g' :<-: x) (downF g))

Aby przejść aroundF, usuwamy tag, zastanawiamy się, jak obejść nieoznakowaną rzecz, a następnie przywracamy tag we wszystkich wynikowych zamkach błyskawicznych. Element w centrum uwagi, xjest zastąpiony przez całą jego zamkiem błyskawicznym z.

  aroundF z@(LF f' :<-: (x :: x)) =
    LF (fmap (\ (f' :<-: x) -> LF f' :<-: x) . cxF $ aroundF (f' :<-: x :: ZF f x))
    :<-: z
  aroundF z@(RF g' :<-: (x :: x)) =
    RF (fmap (\ (g' :<-: x) -> RF g' :<-: x) . cxF $ aroundF (g' :<-: x :: ZF g x))
    :<-: z

Zauważ, że musiałem użyć ScopedTypeVariablesdo ujednoznacznienia rekurencyjnych wywołań do aroundF. Jako funkcja typu DFnie jest iniekcyjna, więc fakt, że f' :: D f xnie wystarcza do wymuszenia f' :<-: x :: Z f x.

Produkt zachowuje różnorodność.

data (f :*: g) x = f x :*: g x
instance (Functor f, Functor g) => Functor (f :*: g) where
  fmap h (f :*: g) = fmap h f :*: fmap h g

Aby skupić się na elemencie w parze, skup się na lewej stronie i zostaw prawą w spokoju lub na odwrót. Słynna reguła produktu Leibniza odpowiada prostej intuicji przestrzennej!

instance (Diff1 f, Diff1 g) => Diff1 (f :*: g) where
  type DF (f :*: g) = (DF f :*: g) :+: (f :*: DF g)
  upF (LF (f' :*: g) :<-: x) = upF (f' :<-: x) :*: g
  upF (RF (f :*: g') :<-: x) = f :*: upF (g' :<-: x)

Teraz downFdziała podobnie jak w przypadku sum, z wyjątkiem tego, że musimy naprawić kontekst zamka błyskawicznego nie tylko za pomocą tagu (aby pokazać, w którą stronę poszliśmy), ale także z nietkniętym innym komponentem.

  downF (f :*: g)
    =    fmap (\ (f' :<-: x) -> LF (f' :*: g) :<-: x) (downF f)
    :*:  fmap (\ (g' :<-: x) -> RF (f :*: g') :<-: x) (downF g)

Ale aroundFto ogromny worek śmiechu. Niezależnie od tego, którą stronę obecnie odwiedzamy, mamy dwie możliwości:

1. Ruszaj się aroundF na tę stronę.
2. Wyjdź upFz tej strony downFna drugą stronę.

Każdy przypadek wymaga od nas wykorzystania operacji dla podkonstrukcji, a następnie ustalenia kontekstów.

  aroundF z@(LF (f' :*: g) :<-: (x :: x)) =
    LF (fmap (\ (f' :<-: x) -> LF (f' :*: g) :<-: x)
          (cxF $ aroundF (f' :<-: x :: ZF f x))
        :*: fmap (\ (g' :<-: x) -> RF (f :*: g') :<-: x) (downF g))
    :<-: z
    where f = upF (f' :<-: x)
  aroundF z@(RF (f :*: g') :<-: (x :: x)) =
    RF (fmap (\ (f' :<-: x) -> LF (f' :*: g) :<-: x) (downF f) :*:
        fmap (\ (g' :<-: x) -> RF (f :*: g') :<-: x)
          (cxF $ aroundF (g' :<-: x :: ZF g x)))
    :<-: z
    where g = upF (g' :<-: x)

Uff! Wszystkie wielomiany są różniczkowalne, co daje nam komonady.

Hmm. To wszystko jest trochę abstrakcyjne. Dodałem więc deriving Showwszędzie, gdzie mogłem, i wrzuciłem

deriving instance (Show (DF f x), Show x) => Show (ZF f x)

co pozwoliło na następującą interakcję (uporządkowane ręcznie)

> downF (IF 1 :*: IF 2)
IF (LF (KF () :*: IF 2) :<-: 1) :*: IF (RF (IF 1 :*: KF ()) :<-: 2)

> fmap aroundF it
IF  (LF (KF () :*: IF (RF (IF 1 :*: KF ()) :<-: 2)) :<-: (LF (KF () :*: IF 2) :<-: 1))
:*:
IF  (RF (IF (LF (KF () :*: IF 2) :<-: 1) :*: KF ()) :<-: (RF (IF 1 :*: KF ()) :<-: 2))

Ćwiczenie Za pomocą reguły łańcuchowej pokaż, że skład funktorów różniczkowalnych jest różniczkowalny .

Słodkie! Czy możemy teraz iść do domu? Oczywiście nie. Nie wyróżniliśmy jeszcze żadnych struktur rekurencyjnych .

Tworzenie funktorów rekurencyjnych z bifunktorów

A Bifunctor, jak szczegółowo wyjaśnia istniejąca literatura na temat programowania generycznego typów danych (patrz praca Patrika Janssona i Johana Jeuringa lub doskonałe notatki do wykładów Jeremy'ego Gibbonsa), jest konstruktorem typu z dwoma parametrami, odpowiadającymi dwóm rodzajom podstruktury. Powinniśmy być w stanie „zmapować” oba.

class Bifunctor b where
  bimap :: (x -> x') -> (y -> y') -> b x y -> b x' y'

Możemy użyć Bifunctors, aby nadać strukturę węzłów kontenerom rekurencyjnym. Każdy węzeł ma podwęzły i elementy . Mogą to być tylko dwa rodzaje podkonstrukcji.

data Mu b y = In (b (Mu b y) y)

Widzieć? W bpierwszym argumencie „wiążemy rekurencyjny węzeł” , aw ydrugim utrzymujemy parametr . W związku z tym otrzymujemy raz na zawsze

instance Bifunctor b => Functor (Mu b) where
  fmap f (In b) = In (bimap (fmap f) f b)

Aby z tego skorzystać, będziemy potrzebować zestawu Bifunctorinstancji.

Zestaw Bifunctor

Stałe są bifunctorial.

newtype K a x y = K a

instance Bifunctor (K a) where
  bimap f g (K a) = K a

Możesz powiedzieć, że napisałem ten bit jako pierwszy, ponieważ identyfikatory są krótsze, ale to dobrze, ponieważ kod jest dłuższy.

Zmienne są bifunctorial.

Potrzebujemy bifunctorów odpowiadających jednemu lub drugiemu parametrowi, więc stworzyłem typ danych, aby je rozróżnić, a następnie zdefiniowałem odpowiedni GADT.

data Var = X | Y

data V :: Var -> * -> * -> * where
  XX :: x -> V X x y
  YY :: y -> V Y x y

To tworzy V X x ykopię xi V Y x ykopię y. Odpowiednio

instance Bifunctor (V v) where
  bimap f g (XX x) = XX (f x)
  bimap f g (YY y) = YY (g y)

Sumy i produkty bifunctorów to bifunctors

data (:++:) f g x y = L (f x y) | R (g x y) deriving Show

instance (Bifunctor b, Bifunctor c) => Bifunctor (b :++: c) where
  bimap f g (L b) = L (bimap f g b)
  bimap f g (R b) = R (bimap f g b)

data (:**:) f g x y = f x y :**: g x y deriving Show

instance (Bifunctor b, Bifunctor c) => Bifunctor (b :**: c) where
  bimap f g (b :**: c) = bimap f g b :**: bimap f g c

Jak dotąd, to szablonowe, ale teraz możemy zdefiniować takie rzeczy jak

List = Mu (K () :++: (V Y :**: V X))

Bin = Mu (V Y :**: (K () :++: (V X :**: V X)))

Jeśli chcesz używać tych typów do rzeczywistych danych i nie tracić wzroku w tradycji pointilliste Georges'a Seurata, użyj synonimów wzorców .

Ale co z zamkami błyskawicznymi? Jak mamy pokazać, że Mu bjest różniczkowalna? Musimy wykazać, że bjest różniczkowalna w obu zmiennych. Szczęk! Czas nauczyć się różnicowania częściowego.

Częściowe pochodne bifunctorów

Ponieważ mamy dwie zmienne, czasami będziemy musieli umieć o nich mówić zbiorowo, a czasami indywidualnie. Będziemy potrzebować rodziny singletonów:

data Vary :: Var -> * where
  VX :: Vary X
  VY :: Vary Y

Teraz możemy powiedzieć, co to znaczy dla Bifunctor mieć częściowe pochodne dla każdej zmiennej i podać odpowiednie pojęcie zippera.

class (Bifunctor b, Bifunctor (D b X), Bifunctor (D b Y)) => Diff2 b where
  type D b (v :: Var) :: * -> * -> *
  up      :: Vary v -> Z b v x y -> b x y
  down    :: b x y -> b (Z b X x y) (Z b Y x y)
  around  :: Vary v -> Z b v x y -> Z b v (Z b X x y) (Z b Y x y)

data Z b v x y = (:<-) {cxZ :: D b v x y, elZ :: V v x y}

Ta Doperacja musi wiedzieć, która zmienna ma być celem. Odpowiedni zamek błyskawiczny Z b vinformuje nas, która zmienna vmusi być aktywna. Kiedy „dekorujemy kontekstem”, musimy dekorować x-elementy X-contexts i y-elementy Y-contexts. Ale poza tym to ta sama historia.

Pozostały nam dwa zadania: po pierwsze, aby pokazać, że nasz zestaw bifunctor jest różniczkowalny; po drugie, aby pokazać, że Diff2 bpozwala nam to ustalić Diff1 (Mu b).

Różnicowanie zestawu Bifunctor

Obawiam się, że ten kawałek jest raczej skrzypcowy niż budujący. Możesz przejść dalej.

Stałe są jak poprzednio.

instance Diff2 (K a) where
  type D (K a) v = K Void
  up _ (K q :<- _) = absurd q
  down (K a) = K a
  around _ (K q :<- _) = absurd q

W tej sytuacji życie jest zbyt krótkie, aby rozwinąć teorię poziomu typu delta Kroneckera, więc po prostu potraktowałem zmienne oddzielnie.

instance Diff2 (V X) where
  type D (V X) X = K ()
  type D (V X) Y = K Void
  up VX (K () :<- XX x)  = XX x
  up VY (K q :<- _)      = absurd q
  down (XX x) = XX (K () :<- XX x)
  around VX z@(K () :<- XX x)  = K () :<- XX z
  around VY (K q :<- _)        = absurd q

instance Diff2 (V Y) where
  type D (V Y) X = K Void
  type D (V Y) Y = K ()
  up VX (K q :<- _)      = absurd q
  up VY (K () :<- YY y)  = YY y
  down (YY y) = YY (K () :<- YY y)
  around VX (K q :<- _)        = absurd q
  around VY z@(K () :<- YY y)  = K () :<- YY z

W przypadku przypadków strukturalnych uznałem za przydatne wprowadzenie pomocnika, który pozwala mi na jednolite traktowanie zmiennych.

vV :: Vary v -> Z b v x y -> V v (Z b X x y) (Z b Y x y)
vV VX z = XX z
vV VY z = YY z

Następnie stworzyłem gadżety, aby ułatwić zmianę tagów, której potrzebujemy do downi around. (Oczywiście podczas pracy widziałem, jakich gadżetów potrzebuję).

zimap :: (Bifunctor c) => (forall v. Vary v -> D b v x y -> D b' v x y) ->
         c (Z b X x y) (Z b Y x y) -> c (Z b' X x y) (Z b' Y x y)
zimap f = bimap
  (\ (d :<- XX x) -> f VX d :<- XX x)
  (\ (d :<- YY y) -> f VY d :<- YY y)

dzimap :: (Bifunctor (D c X), Bifunctor (D c Y)) =>
         (forall v. Vary v -> D b v x y -> D b' v x y) ->
         Vary v -> Z c v (Z b X x y) (Z b Y x y) -> D c v (Z b' X x y) (Z b' Y x y)
dzimap f VX (d :<- _) = bimap
  (\ (d :<- XX x) -> f VX d :<- XX x)
  (\ (d :<- YY y) -> f VY d :<- YY y)
  d
dzimap f VY (d :<- _) = bimap
  (\ (d :<- XX x) -> f VX d :<- XX x)
  (\ (d :<- YY y) -> f VY d :<- YY y)
  d

A mając tyle gotowych do użycia, możemy dopracować szczegóły. Sumy są łatwe.

instance (Diff2 b, Diff2 c) => Diff2 (b :++: c) where
  type D (b :++: c) v = D b v :++: D c v
  up v (L b' :<- vv) = L (up v (b' :<- vv))
  down (L b) = L (zimap (const L) (down b))
  down (R c) = R (zimap (const R) (down c))
  around v z@(L b' :<- vv :: Z (b :++: c) v x y)
    = L (dzimap (const L) v ba) :<- vV v z
    where ba = around v (b' :<- vv :: Z b v x y)
  around v z@(R c' :<- vv :: Z (b :++: c) v x y)
    = R (dzimap (const R) v ca) :<- vV v z
    where ca = around v (c' :<- vv :: Z c v x y)

Produkty to ciężka praca, dlatego jestem raczej matematykiem niż inżynierem.

instance (Diff2 b, Diff2 c) => Diff2 (b :**: c) where
  type D (b :**: c) v = (D b v :**: c) :++: (b :**: D c v)
  up v (L (b' :**: c) :<- vv) = up v (b' :<- vv) :**: c
  up v (R (b :**: c') :<- vv) = b :**: up v (c' :<- vv)
  down (b :**: c) =
    zimap (const (L . (:**: c))) (down b) :**: zimap (const (R . (b :**:))) (down c)
  around v z@(L (b' :**: c) :<- vv :: Z (b :**: c) v x y)
    = L (dzimap (const (L . (:**: c))) v ba :**:
        zimap (const (R . (b :**:))) (down c))
      :<- vV v z where
      b = up v (b' :<- vv :: Z b v x y)
      ba = around v (b' :<- vv :: Z b v x y)
  around v z@(R (b :**: c') :<- vv :: Z (b :**: c) v x y)
    = R (zimap (const (L . (:**: c))) (down b):**:
        dzimap (const (R . (b :**:))) v ca)
      :<- vV v z where
      c = up v (c' :<- vv :: Z c v x y)
      ca = around v (c' :<- vv :: Z c v x y)

Koncepcyjnie jest tak jak wcześniej, ale z większą biurokracją. Zbudowałem je przy użyciu technologii typu pre-type-hole, używającundefined jako stubu w miejscach, w których nie byłem gotowy do pracy, i wprowadzając celowy błąd typu w jednym miejscu (w danym momencie), w którym chciałem uzyskać przydatną wskazówkę od sprawdzarki typu . Ty także możesz mieć sprawdzanie typów jako doświadczenie w grach wideo, nawet w Haskell.

Zamki błyskawiczne podwęzłów dla kontenerów rekurencyjnych

Pochodna częściowa w bodniesieniu do Xmówi nam, jak znaleźć podwęzeł o jeden krok w węźle, więc otrzymujemy konwencjonalne pojęcie zippera.

data MuZpr b y = MuZpr
  {  aboveMu  :: [D b X (Mu b y) y]
  ,  hereMu   :: Mu b y
  }

Możemy przybliżyć całą drogę do korzenia poprzez wielokrotne podłączanie Xpozycji.

muUp :: Diff2 b => MuZpr b y -> Mu b y
muUp (MuZpr {aboveMu = [], hereMu = t}) = t
muUp (MuZpr {aboveMu = (dX : dXs), hereMu = t}) =
  muUp (MuZpr {aboveMu = dXs, hereMu = In (up VX (dX :<- XX t))})

Ale potrzebujemy element -zippers.

Zamki błyskawiczne do punktów mocowania rozgałęźników

Każdy element znajduje się gdzieś wewnątrz węzła. Ten węzeł znajduje się pod stosem X-pochodnych. Ale pozycja elementu w tym węźle jest określona przez Y-pochodną. Dostajemy

data MuCx b y = MuCx
  {  aboveY  :: [D b X (Mu b y) y]
  ,  belowY  :: D b Y (Mu b y) y
  }

instance Diff2 b => Functor (MuCx b) where
  fmap f (MuCx { aboveY = dXs, belowY = dY }) = MuCx
    {  aboveY  = map (bimap (fmap f) f) dXs
    ,  belowY  = bimap (fmap f) f dY
    }

Odważnie, twierdzę

instance Diff2 b => Diff1 (Mu b) where
  type DF (Mu b) = MuCx b

ale zanim opracuję operacje, będę potrzebować kilku elementów.

Mogę wymieniać dane między zamkami funktorowymi i zamkami bifunktorowymi w następujący sposób:

zAboveY :: ZF (Mu b) y -> [D b X (Mu b y) y]  -- the stack of `X`-derivatives above me
zAboveY (d :<-: y) = aboveY d

zZipY :: ZF (Mu b) y -> Z b Y (Mu b y) y      -- the `Y`-zipper where I am
zZipY (d :<-: y) = belowY d :<- YY y

Wystarczy, żebym zdefiniował:

  upF z  = muUp (MuZpr {aboveMu = zAboveY z, hereMu = In (up VY (zZipY z))})

Oznacza to, że przechodzimy w górę, najpierw składając węzeł, w którym znajduje się element, zamieniając suwak elementu w zamek błyskawiczny podwęzła, a następnie maksymalnie oddalając, jak powyżej.

Dalej, mówię

  downF  = yOnDown []

aby zejść na dół zaczynając od pustego stosu i zdefiniuj funkcję pomocniczą, która będzie się downpowtarzać spod dowolnego stosu:

yOnDown :: Diff2 b => [D b X (Mu b y) y] -> Mu b y -> Mu b (ZF (Mu b) y)
yOnDown dXs (In b) = In (contextualize dXs (down b))

Teraz down bprzenosi nas tylko do węzła. Suwaki, których potrzebujemy, muszą również przenosić kontekst węzła. To właśnie contextualiseoznacza:

contextualize :: (Bifunctor c, Diff2 b) =>
  [D b X (Mu b y) y] ->
  c (Z b X (Mu b y) y) (Z b Y (Mu b y) y) ->
  c (Mu b (ZF (Mu b) y)) (ZF (Mu b) y)
contextualize dXs = bimap
  (\ (dX :<- XX t) -> yOnDown (dX : dXs) t)
  (\ (dY :<- YY y) -> MuCx {aboveY = dXs, belowY = dY} :<-: y)

Dla każdej Ypozycji musimy podać suwak elementu, więc dobrze, że znamy cały kontekst dXsaż do korzenia, a także ten, dYktóry opisuje, jak element znajduje się w swoim węźle. Dla każdej Xpozycji jest kolejne poddrzewo do zbadania, więc powiększamy stos i kontynuujemy!

Pozostaje tylko kwestia zmiany punktu ciężkości. Możemy pozostać na miejscu, zejść z miejsca, w którym jesteśmy, albo pójść w górę, albo pójść w górę, a potem inną ścieżką. Tutaj idzie.

  aroundF z@(MuCx {aboveY = dXs, belowY = dY} :<-: _) = MuCx
    {  aboveY = yOnUp dXs (In (up VY (zZipY z)))
    ,  belowY = contextualize dXs (cxZ $ around VY (zZipY z))
    }  :<-: z

Jak zawsze, dotychczasowy element zostaje zastąpiony przez cały zamek błyskawiczny. Po belowYczęści szukamy, gdzie jeszcze możemy się udać w istniejącym węźle: znajdziemy albo alternatywne pozycje- elementów, Yalbo dalsze X-subnody do zbadania, więc contextualiseje. Po aboveYczęści, Xpo ponownym złożeniu węzła, który odwiedziliśmy , musimy wykonać kopię zapasową stosu -pochodnych.

yOnUp :: Diff2 b => [D b X (Mu b y) y] -> Mu b y ->
         [D b X (Mu b (ZF (Mu b) y)) (ZF (Mu b) y)]
yOnUp [] t = []
yOnUp (dX : dXs) (t :: Mu b y)
  =  contextualize dXs (cxZ $ around VX (dX :<- XX t))
  :  yOnUp dXs (In (up VX (dX :<- XX t)))

Na każdym kroku możemy skręcić w inne miejsce aroundlub iść dalej.

I to wszystko! Nie przedstawiłem formalnego potwierdzenia praw, ale wydaje mi się, że operacje ostrożnie zachowują prawidłowy kontekst podczas przeszukiwania struktury.

Czego się nauczyliśmy?

Różniczkowalność wywołuje pojęcia rzeczy w jej kontekście, indukując strukturę komonadyczną, w której extractdaje rzecz i duplicatebada kontekst, szukając innych rzeczy do kontekstualizacji. Jeśli mamy odpowiednią strukturę różnicową dla węzłów, możemy opracować strukturę różnicową dla całych drzew.

Aha, i traktowanie każdego indywidualnego konstruktora typu z osobna jest rażąco przerażające. Lepszym sposobem jest praca z funktorami pomiędzy indeksowanymi zbiorami

f :: (i -> *) -> (o -> *)

gdzie tworzymy oróżne rodzaje struktur przechowujących iróżne rodzaje elementów. Są one zamknięte pod konstrukcją jakobianą

J f :: (i -> *) -> ((o, i) -> *)

gdzie każda z powstałych (o, i)-struktur jest pochodną częściową, mówiącą, jak zrobić i-elementową-dziurę w o-strukturze. Ale to zależnie wpisana zabawa, na inny czas.

W Comonadprzypadku zamków błyskawicznych nie

instance (Diff t, Diff (D t)) => Comonad (Zipper t) where
    extract = here
    duplicate = fmap outOf . inTo

skąd outOfi inTopochodzić z Diffinstancji dla Zipper tsiebie. Powyższe wystąpienie narusza Comonadprawo fmap extract . duplicate == id. Zamiast tego zachowuje się jak:

fmap extract . duplicate == \z -> fmap (const (here z)) z

Diff (Zipper t)

DiffPrzykład na Zipperjest przez określenie ich jako produktów i ponowne kod produktu (poniżej).

-- Zippers are themselves products
toZipper :: (D t :*: Identity) a -> Zipper t a
toZipper (d :*: (Identity h)) = Zipper d h

fromZipper :: Zipper t a -> (D t :*: Identity) a
fromZipper (Zipper d h) = (d :*: (Identity h))

Biorąc pod uwagę izomorfizm między typami danych i izomorfizm między ich pochodnymi, możemy ponownie użyć jednego typu inToi outOfdla drugiego.

inToFor' :: (Diff r) =>
            (forall a.   r a ->   t a) ->
            (forall a.   t a ->   r a) ->
            (forall a. D r a -> D t a) ->
            (forall a. D t a -> D r a) ->
            t a -> t (Zipper t a)
inToFor' to from toD fromD = to . fmap (onDiff toD) . inTo . from

outOfFor' :: (Diff r) =>
            (forall a.   r a ->   t a) ->
            (forall a.   t a ->   r a) ->
            (forall a. D r a -> D t a) ->
            (forall a. D t a -> D r a) ->
            Zipper t a -> t a
outOfFor' to from toD fromD = to . outOf . onDiff fromD

W przypadku typów, które są tylko newTypes dla istniejącej Diffinstancji, ich pochodne są tego samego typu. Jeśli powiemy kontrolerowi typów o tej równości typów D r ~ D t, możemy to wykorzystać zamiast zapewniać izomorfizm dla pochodnych.

inToFor :: (Diff r, D r ~ D t) =>
           (forall a. r a -> t a) ->
           (forall a. t a -> r a) ->
           t a -> t (Zipper t a)
inToFor to from = inToFor' to from id id

outOfFor :: (Diff r, D r ~ D t) =>
            (forall a. r a -> t a) ->
            (forall a. t a -> r a) ->
            Zipper t a -> t a
outOfFor to from = outOfFor' to from id id

Wyposażeni w te narzędzia, możemy ponownie wykorzystać Diffinstancję do wdrożenia produktówDiff (Zipper t)

-- This requires undecidable instances, due to the need to take D (D t)
instance (Diff t, Diff (D t)) => Diff (Zipper t) where
    type D (Zipper t) = D ((D t) :*: Identity)
    -- inTo :: t        a -> t        (Zipper  t         a)
    -- inTo :: Zipper t a -> Zipper t (Zipper (Zipper t) a)
    inTo = inToFor toZipper fromZipper
    -- outOf :: Zipper  t         a -> t        a
    -- outOf :: Zipper (Zipper t) a -> Zipper t a
    outOf = outOfFor toZipper fromZipper

Płyta kotłowa

Aby faktycznie skorzystać z przedstawionego tutaj kodu, potrzebujemy pewnych rozszerzeń językowych, importu i ponownego przedstawienia proponowanego problemu.

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}

import Control.Monad.Identity
import Data.Proxy
import Control.Comonad

data Zipper t a = Zipper { diff :: D t a, here :: a }

onDiff :: (D t a -> D u a) -> Zipper t a -> Zipper u a
onDiff f (Zipper d a) = Zipper (f d) a

deriving instance Diff t => Functor (Zipper t)
deriving instance (Eq (D t a), Eq a) => Eq (Zipper t a)
deriving instance (Show (D t a), Show a) => Show (Zipper t a)

class (Functor t, Functor (D t)) => Diff t where
  type D t :: * -> *
  inTo  :: t a -> t (Zipper t a)
  outOf :: Zipper t a -> t a

Produkty, sumy i stałe

Diff (Zipper t)Instancji opiera się na wdrożeniach Diffproduktów :*:, sum :+:, stałe Identityi zera Proxy.

data (:+:) a b x = InL (a x) | InR (b x)
    deriving (Eq, Show)
data (:*:) a b x = a x :*: b x
    deriving (Eq, Show)

infixl 7 :*:
infixl 6 :+:

deriving instance (Functor a, Functor b) => Functor (a :*: b)

instance (Functor a, Functor b) => Functor (a :+: b) where
    fmap f (InL a) = InL . fmap f $ a
    fmap f (InR b) = InR . fmap f $ b


instance (Diff a, Diff b) => Diff (a :*: b) where
    type D (a :*: b) = D a :*: b :+: a :*: D b
    inTo (a :*: b) = 
        (fmap (onDiff (InL . (:*: b))) . inTo) a :*:
        (fmap (onDiff (InR . (a :*:))) . inTo) b
    outOf (Zipper (InL (a :*: b)) x) = (:*: b) . outOf . Zipper a $ x
    outOf (Zipper (InR (a :*: b)) x) = (a :*:) . outOf . Zipper b $ x

instance (Diff a, Diff b) => Diff (a :+: b) where
    type D (a :+: b) = D a :+: D b
    inTo (InL a) = InL . fmap (onDiff InL) . inTo $ a
    inTo (InR b) = InR . fmap (onDiff InR) . inTo $ b
    outOf (Zipper (InL a) x) = InL . outOf . Zipper a $ x
    outOf (Zipper (InR a) x) = InR . outOf . Zipper a $ x

instance Diff (Identity) where
    type D (Identity) = Proxy
    inTo = Identity . (Zipper Proxy) . runIdentity
    outOf = Identity . here

instance Diff (Proxy) where
    type D (Proxy) = Proxy
    inTo = const Proxy
    outOf = const Proxy

Przykład pojemnika

Podałem Binprzykład jako izomorfizm sumy iloczynów. Potrzebujemy nie tylko jego pochodnej, ale także drugiej pochodnej

newtype Bin   a = Bin   {unBin   ::      (Bin :*: Identity :*: Bin :+: Identity)  a}
    deriving (Functor, Eq, Show)
newtype DBin  a = DBin  {unDBin  ::    D (Bin :*: Identity :*: Bin :+: Identity)  a}
    deriving (Functor, Eq, Show)
newtype DDBin a = DDBin {unDDBin :: D (D (Bin :*: Identity :*: Bin :+: Identity)) a}
    deriving (Functor, Eq, Show)

instance Diff Bin where
    type D Bin = DBin
    inTo  = inToFor'  Bin unBin DBin unDBin
    outOf = outOfFor' Bin unBin DBin unDBin

instance Diff DBin where
    type D DBin = DDBin
    inTo  = inToFor'  DBin unDBin DDBin unDDBin
    outOf = outOfFor' DBin unDBin DDBin unDDBin

Przykładowe dane z poprzedniej odpowiedzi to

aTree :: Bin Int    
aTree =
    (Bin . InL) (
        (Bin . InL) (
            (Bin . InR) (Identity 2)
            :*: (Identity 1) :*:
            (Bin . InR) (Identity 3)
        )
        :*: (Identity 0) :*:
        (Bin . InR) (Identity 4)
    )

Nie instancja Comonad

Powyższy Binprzykład stanowi kontrprzykład do fmap outOf . inTobycia poprawną implementacją duplicatefor Zipper t. W szczególności stanowi kontrprzykład dla fmap extract . duplicate = idprawa:

fmap ( \z -> (fmap extract . duplicate) z == z) . inTo $ aTree

Który ocenia (zauważ, jak Falsewszędzie jest pełno, Falsewystarczyłoby, by obalić prawo)

Bin {unBin = InL ((Bin {unBin = InL ((Bin {unBin = InR (Identity False)} :*: Identity False) :*: Bin {unBin = InR (Identity False)})} :*: Identity False) :*: Bin {unBin = InR (Identity False)})}

inTo aTreejest drzewem o takiej samej strukturze jak aTree, ale wszędzie tam była wartość, zamiast niej jest suwak z wartością, a reszta drzewa z nienaruszonymi wszystkimi oryginalnymi wartościami. fmap (fmap extract . duplicate) . inTo $ aTreejest także drzewem o takiej samej strukturze jak aTree, ale zawsze, gdy była wartość, zamiast niej jest zamek błyskawiczny z wartością, a reszta drzewa ze wszystkimi wartościami zastąpionymi tą samą wartością . Innymi słowy:

fmap extract . duplicate == \z -> fmap (const (here z)) z

Kompletny test-pakiet dla wszystkich trzech Comonadustaw, extract . duplicate == id, fmap extract . duplicate == id, i duplicate . duplicate == fmap duplicate . duplicatejest w stanie

main = do
    putStrLn "fmap (\\z -> (extract . duplicate) z == z) . inTo $ aTree"
    print   . fmap ( \z -> (extract . duplicate) z == z) . inTo $ aTree    
    putStrLn ""
    putStrLn  "fmap (\\z -> (fmap extract . duplicate) z == z) . inTo $ aTree"
    print    . fmap ( \z -> (fmap extract . duplicate) z == z) . inTo $ aTree    
    putStrLn ""
    putStrLn "fmap (\\z -> (duplicate . duplicate) z) == (fmap duplicate . duplicate) z) . inTo $ aTree"
    print   . fmap ( \z -> (duplicate . duplicate) z == (fmap duplicate . duplicate) z) . inTo $ aTree

Biorąc pod uwagę nieskończenie różniczkowalną Diffklasę:

class (Functor t, Functor (D t)) => Diff t where
    type D t :: * -> *
    up :: Zipper t a -> t a
    down :: t a -> t (Zipper t a)  
    -- Require that types be infinitely differentiable
    ddiff :: p t -> Dict (Diff (D t))

aroundmożna zapisać w zakresie upi downna Zipper„s diff” s derivitive zasadniczo jako

around z@(Zipper d h) = Zipper ctx z
    where
        ctx = fmap (\z' -> Zipper (up z') (here z')) (down d)

Zipper t aSkłada się z D t ai a. Idziemy , coraz z zamkiem w każdą dziurę. Te zamki składają się z i tego, co było w otworze. Idziemy do każdego z nich, pobieramy i łączymy z tym, co było w dziurze. A i make a , dając nam a , który jest kontekstem potrzebnym do .downD t aD t (Zipper (D t) a)D (D t) aaupD t aaD t aaZipper t aD t (Zipper t a)Zipper t (Zipper t a)

ComonadWystąpienie jest po prostu

instance Diff t => Comonad (Zipper t) where
    extract   = here
    duplicate = around

Przechwycenie Diffsłownika pochodnej wymaga dodatkowej hydrauliki, którą można wykonać za pomocą Data.Constraint lub w ramach metody przedstawionej w powiązanej odpowiedzi

around :: Diff t => Zipper t a -> Zipper t (Zipper t a)
around z = Zipper (withDict d' (fmap (\z' -> Zipper (up z') (here z')) (down (diff z)))) z
    where
        d' = ddiff . p' $ z
        p' :: Zipper t x -> Proxy t
        p' = const Proxy