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
fmap upF (downF xs) = fmap (const xs) xs
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:
- Ruszaj się
aroundF na tę stronę.
- 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]
zAboveY (d :<-: y) = aboveY d
zZipY :: ZF (Mu b) y -> Z b Y (Mu b y) y
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.