[haskell] 일반적으로 지퍼 코 모나드

Chitty-Chitty-Bang-Bang의 유인원처럼 아이들을 과자와 장난감으로 포로로 유인하고, 물리학을 학부 모집하는 사람은 비누 방울과 부메랑으로 속이는 것을 좋아하지만 문이 닫히면 “맞아요, 아이들, 배울 시간입니다. 부분 미분에 대해! “. 나도. 내가 경고하지 않았다고 말하지 마십시오.

여기에 또 다른 경고가 있습니다. 다음 코드 {-# LANGUAGE KitchenSink #-}에는, 또는

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

특별한 순서없이.

차별화 가능한 펑터로 코모 나딕 지퍼 제공

어쨌든 차별화 가능한 펑 터는 무엇입니까?

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}

그것은 펑터이기도 한 파생물이있는 펑터입니다. 파생물은 요소에 대한 원홀 컨텍스트를 나타냅니다 . 지퍼 유형 ZF f x은 한 쌍의 구멍 컨텍스트와 구멍의 요소를 나타냅니다.

에 대한 작업은 Diff1지퍼에 대해 수행 할 수있는 탐색의 종류 를 설명합니다 ( “왼쪽”및 “오른쪽”이라는 개념이 없습니다. 이에 대해서는 Clowns and Jokers 문서 참조). 우리는 “위로”가서 그 구멍에 요소를 꽂아 구조를 재 조립할 수 있습니다. 우리는 “아래로”가서 주어진 구조에서 요소를 방문하는 모든 방법을 찾을 수 있습니다. 우리는 모든 요소를 ​​컨텍스트로 장식합니다. 우리는 “둘러서”, 기존 지퍼를 가져 와서 컨텍스트에 따라 각 요소를 장식 할 수 있으므로 초점을 다시 맞추는 모든 방법 (및 현재 초점을 유지하는 방법)을 찾습니다.

자,이 유형 aroundF은 여러분에게

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

그리고 당신은 상기시키는 것이 옳습니다! 우리는 홉과 스킵으로

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

그리고 우리는 그것을 주장합니다

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

우리는 또한 필요합니다

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

다항식 펑 터는 미분 가능

상수 펑 터는 구별 할 수 있습니다.

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

요소를 넣을 곳이 없으므로 컨텍스트를 형성하는 것이 불가능합니다. 이 갈 곳이 없습니다 것 upF또는 downF에서, 우리는 쉽게 갈 수있는 모든 방법 아무도 찾을 수 없습니다 downF.

신원 펑 터는 미분이다.

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

사소한 맥락에서 하나의 요소가 있고, downF그것을 찾고, upF재 포장하고, aroundF단지 그대로있을 수 있습니다.

Sum 은 차별성을 유지합니다.

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))

다른 비트와 조각은 조금 더 적습니다. 이동하려면 태그가 지정된 구성 요소 내부 downF로 이동 downF한 다음 결과 지퍼를 수정하여 컨텍스트에 태그를 표시해야합니다.

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

이동하려면 aroundF태그를 제거하고 태그가 지정되지 않은 물건을 돌아 다니는 방법을 파악한 다음 모든 결과 지퍼에서 태그를 복원합니다. 초점이 맞춰진 요소 x는 전체 지퍼로 대체됩니다 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

에 ScopedTypeVariables대한 재귀 호출을 명확하게하기 위해을 사용해야 했습니다 aroundF. 유형 함수로서 DF주입 적이 지 않으므로 f' :: D f x강제로 f' :<-: x :: Z f x.

제품 은 차별성을 유지합니다.

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

한 쌍의 요소에 초점을 맞추려면 왼쪽에 초점을 맞추고 오른쪽은 그대로 두거나 그 반대의 경우도 마찬가지입니다. Leibniz의 유명한 제품 규칙은 단순한 공간 직관에 해당합니다!

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)

이제는 downF태그 (어느 방향으로 갔는지 표시하기 위해)뿐만 아니라 손대지 않은 다른 구성 요소를 사용하여 지퍼 컨텍스트를 수정해야한다는 점을 제외하면 합계에 대해 수행 한 방식과 유사하게 작동합니다.

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

그러나 aroundF엄청난 웃음 가방입니다. 현재 어느 쪽을 방문하든 두 가지 선택이 있습니다.

1. aroundF저쪽으로 이동하십시오 .
2. 이동 upF이 측면의 밖으로 downF다른 측면으로.

각각의 경우에 우리는 하부 구조에 대한 작업을 사용하고 컨텍스트를 수정해야합니다.

  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)

휴! 다항식은 모두 미분 가능하므로 코 모나드를 제공합니다.

흠. 모두 약간 추상적입니다. 그래서 가능한 deriving Show모든 곳에 추가 하고

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

다음과 같은 상호 작용을 허용했습니다 (손으로 묶음).

> 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))

운동 보기는 미분 펑터의 구성은 사용 미분이다 체인 규칙을 .

단! 이제 집에 갈 수 있을까요? 당연히 아니지. 우리는 아직 어떤 재귀 구조도 구별하지 않았습니다.

bifunctor에서 재귀 펑터 만들기

Bifunctor길이가 하부의 두 종류에 해당하는 두 개의 매개 변수와 타입 생성자이다에서, 데이터 타입 일반적인 프로그래밍에 대한 기존의 문헌으로 (패트릭 얀손과 요한 Jeuring, 또는 제레미 기븐스에 의한 우수한 강의 노트에 의해 참조 작업)을 설명합니다. 둘 다 “매핑”할 수 있어야합니다.

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

Bifunctors를 사용하여 재귀 컨테이너의 노드 구조를 제공 할 수 있습니다 . 각 노드에는 하위 노드 와 요소가 있습니다. 이것들은 단지 두 종류의 하부 구조 일 수 있습니다.

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

보다? 우리는 b의 첫 번째 인수 에서 “재귀 매듭을 묶고” 매개 변수 y를 두 번째 인수에 유지합니다 . 따라서 우리는 모두를 위해 한 번 얻습니다

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

이를 사용하려면 Bifunctor인스턴스 키트가 필요 합니다.

Bifunctor 키트

상수 는 이중 기능입니다.

newtype K a x y = K a

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

식별자가 더 짧기 때문에이 비트를 먼저 썼다고 말할 수 있지만 코드가 더 길기 때문에 좋습니다.

변수 는 이중 기능입니다.

하나 또는 다른 매개 변수에 해당하는 bifunctor가 필요하므로이를 구별하기 위해 데이터 유형을 만든 다음 적절한 GADT를 정의했습니다.

data Var = X | Y

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

즉 수 V X x y의 사본 x과 V Y x y사본을 y. 따라서

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

덧셈 과 제품 bifunctors의는 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

지금까지는 상용구이지만 이제 다음과 같은 것을 정의 할 수 있습니다.

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

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

이러한 유형을 실제 데이터에 사용하고 Georges Seurat의 점진적 전통에서 눈을 멀게하지 않으려면 패턴 동의어를 사용하십시오 .

하지만 지퍼는 어떻습니까? 그것이 Mu b차별화 될 수 있음을 어떻게 보여줄 까요? 우리는 그것이 두 변수 b에서 구별 될 수 있음을 보여줄 필요가 있습니다. 그 소리! 부분 미분에 대해 배울 때입니다.

bifunctor의 부분 도함수

우리는 두 가지 변수를 가지고 있기 때문에 때때로 집단적으로 그리고 다른 시간에는 개별적으로 이야기 할 수 있어야합니다. 싱글 톤 패밀리가 필요합니다.

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

이제 Bifunctor가 각 변수에서 편도 함수를 갖는 것이 무엇을 의미하는지 말할 수 있고 이에 상응하는 지퍼 개념을 제공 할 수 있습니다.

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}

이 D작업은 타겟팅 할 변수를 알아야합니다. 해당 지퍼 Z b v는 어떤 변수 v에 초점 이 맞춰져야 하는지 알려줍니다 . 우리는 “컨텍스트 장식은”우리는 장식이있는 경우 x와 -elements X-contexts과 y와 -elements Y-contexts을. 그러나 그렇지 않으면 같은 이야기입니다.

나머지 두 가지 작업이 있습니다. 첫째, bifunctor 키트가 차별화 될 수 있음을 보여줍니다. 둘째,이를 Diff2 b통해 Diff1 (Mu b).

Bifunctor 키트 차별화

나는이 부분이 교화보다는 어리석은 일이 아닐까 두렵다. 건너 뛰어도됩니다.

상수는 이전과 같습니다.

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

이 경우, Kronecker-delta 유형 수준의 이론을 개발하기에는 인생이 너무 짧아서 변수를 별도로 처리했습니다.

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

구조적인 경우에는 변수를 균일하게 다룰 수있는 도우미를 도입하는 것이 유용하다는 것을 알았습니다.

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

그런 다음 down및에 필요한 “태그 재 지정”을 용이하게하는 가젯을 만들었습니다 around. (물론 작업 할 때 필요한 가젯이 무엇인지 확인했습니다.)

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

그리고 그 많은 준비가 완료되면 세부 사항을 다듬을 수 있습니다. 합계는 쉽습니다.

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)

제품은 열심히 일하기 때문에 엔지니어가 아닌 수학자입니다.

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)

개념적으로는 이전과 같지만 관료주의가 더 많습니다. 저는 프리 타입 홀 기술을 사용하여 이것을 만들었습니다.undefined 하고, 내가 일할 준비가되지 않은 곳에서 스텁으로 하고, typechecker로부터 유용한 힌트를 원했던 한곳 (언제든지)에 의도적 인 유형 오류를 도입했습니다. . Haskell에서도 비디오 게임 경험으로 타입 체킹을 할 수 있습니다.

재귀 컨테이너 용 서브 노드 지퍼

에 대한 편미분 은 노드 내에서 한 단계 하위 노드를 찾는 방법 b을 X알려주므로 기존의 지퍼 개념을 얻습니다.

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

X위치 를 반복해서 연결하여 루트까지 확대 할 수 있습니다 .

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))})

그러나 우리는 요소 지퍼 가 필요합니다 .

바이 펑터 고정 점용 요소 지퍼

각 요소는 노드 내부에 있습니다. 해당 노드는 X파생 상품 스택 아래에 있습니다. 그러나 해당 노드에서 요소의 위치는 Y-derivative 로 제공됩니다 . 우리는

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
    }

대담하게 나는 주장한다

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

그러나 작업을 개발하기 전에 약간의 조각이 필요합니다.

다음과 같이 functor-zippers와 bifunctor-zippers간에 데이터를 교환 할 수 있습니다.

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

이것으로 정의 할 수 있습니다.

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

즉, 먼저 요소가있는 노드를 재 조립하고 요소-지퍼를 하위 노드-지퍼로 전환 한 다음 위와 같이 완전히 축소하여 위로 이동합니다.

다음으로

  downF  = yOnDown []

빈 스택에서 시작하여 아래로 내려 가서 스택 down아래에서 반복적으로 이동하는 도우미 함수를 정의합니다 .

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))

이제 down b노드 내부로만 이동합니다. 필요한 지퍼는 노드의 컨텍스트를 전달해야합니다. 그게 뭐죠 contextualise:

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)

모든 Y위치에 대해 요소-지퍼를 제공해야하므로 dXs루트로 돌아가는 전체 컨텍스트 dY와 요소가 노드에 배치되는 방식을 설명하는 을 아는 것이 좋습니다 . 모든 X위치에 대해 탐색 할 추가 하위 트리가 있으므로 스택을 늘리고 계속 진행합니다!

그것은 초점을 바꾸는 사업만을 남깁니다. 우리는 가만히 있거나 우리가있는 곳에서 내려가거나, 올라가거나, 다른 길로 올라 갔다가 내려갈 수 있습니다. 여기 있습니다.

  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

여느 때와 마찬가지로 기존 요소는 전체 지퍼로 대체됩니다. 를 들어 belowY우리가 다른 요소 중 하나를 찾을 수 있습니다 : 우리는 기존 노드에 갈 수있는 다른 부분, 우리는 볼 Y-positions 또는 추가 X탐구하는 -subnodes을 우리, contextualise그들. 를 들어 aboveY부분, 우리는 스택까지 우리의 방식으로 다시 일해야 X우리가 방문했던 노드를 재 조립 한 후 -derivatives합니다.

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)))

각 단계에서 우리는 around 거나 계속 올라갈 수 있습니다.

그리고 그게 다야! 나는 법에 대한 공식적인 증거를 제공하지 않았지만, 작업이 구조를 크롤링 할 때 컨텍스트를 신중하게 유지하는 것처럼 보입니다.

우리는 무엇을 배웠습니까?

차별화 가능성은 상황에 맞는 사물의 개념을 유도하여 사물을 extract제공 하는 코모 나딕 구조를 유도합니다.duplicate 맥락화에 다른 일을 찾고 맥락을 탐구한다. 노드에 대한 적절한 미분 구조가 있으면 전체 트리에 대한 미분 구조를 개발할 수 있습니다.

오, 유형 생성자의 각 개별 배열을 개별적으로 처리하는 것은 노골적으로 끔찍합니다. 더 좋은 방법은 인덱스 된 세트 사이에서 펑터로 작업하는 것입니다.

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

여기서 우리는 o다른 i종류의 요소를 저장하는 다른 종류의 구조를 만듭니다 . 이들은 Jacobian 구조 로 닫힙니다.

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

각각의 결과 (o, i)구조는 편미분 i으로 o구조 에서 요소 구멍 을 만드는 방법을 알려줍니다 . 그러나 그것은 다른 시간 동안 의존적으로 입력 된 재미입니다.