일반적으로 지퍼 코 모나드
모든 컨테이너 유형이 주어지면 (요소 중심) 지퍼를 형성 할 수 있으며이 구조가 Comonad임을 알 수 있습니다. 이것은 최근 다음 유형에 대한 또 다른 스택 오버플로 질문 에서 훌륭하게 자세히 탐구되었습니다 .
data Bin a = Branch (Bin a) a (Bin a) | Leaf a deriving Functor
뒤에 오는 지퍼로
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 ...
그것은의 경우 ZipA는 Comonad해당 인스턴스의 구성이 약간 털이 있지만. 즉, Zip완전히 기계적으로 파생 될 수 있으며 Tree이러한 방식으로 파생 된 모든 유형은 자동으로 Comonad이므로 이러한 유형과 해당 코 모나드를 일반적으로 자동으로 구성 할 수 있어야한다고 생각합니다.
지퍼 구조의 일반성을 달성하는 한 가지 방법은 다음 클래스 및 유형 제품군을 사용하는 것입니다.
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
Haskell Cafe 스레드와 Conal Elliott의 블로그에 표시되었습니다. 이 클래스는 다양한 핵심 대수 유형에 대해 인스턴스화 될 수 있으므로 ADT의 파생물에 대해 이야기하기위한 일반적인 프레임 워크를 제공합니다.
그래서 궁극적으로 제 질문은 우리가 쓸 수 있는지 여부입니다.
instance Diff t => Comonad (Zipper t) where ...
위에서 설명한 특정 Comonad 인스턴스를 포함하는 데 사용할 수 있습니다.
instance Diff Bin where
data D Bin a = DBin { context :: [Step a], descend :: Maybe (Bin a, Bin a) }
...
불행히도 나는 그러한 사례를 작성하지 못했습니다. 는 IS inTo/ outOf서명이 충분? 유형을 제한하는 데 필요한 다른 것이 있습니까? 이 경우도 가능합니까?
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엄청난 웃음 가방입니다. 현재 어느 쪽을 방문하든 두 가지 선택이 있습니다.
aroundF저쪽으로 이동하십시오 .- 이동
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)
개념적으로는 이전과 같지만 관료주의가 더 많습니다. 나는 pre-type-hole 기술을 사용 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위치로 X이동할 수 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거나 계속 올라갈 수 있습니다.
그리고 그게 다야! 나는 법에 대한 공식적인 증거를 제공하지 않았지만, 작업이 구조를 크롤링 할 때 컨텍스트를 신중하게 유지하는 것처럼 보입니다.
우리는 무엇을 배웠습니까?
미분 가능성의 유도하는 comonadic 구조를 유도하는 것 -에 - 그 컨텍스트의 개념, extract당신에게 일을 제공하고 duplicate맥락화에 다른 일을 찾고 맥락을 탐구한다. 노드에 대한 적절한 미분 구조가 있으면 전체 트리에 대한 미분 구조를 개발할 수 있습니다.
아, 유형 생성자의 각 개별 배열을 개별적으로 처리하는 것은 노골적으로 끔찍합니다. 더 좋은 방법은 인덱스 된 세트 사이에서 펑터로 작업하는 것입니다.
f :: (i -> *) -> (o -> *)
다른 종류의 요소를 o저장하는 i다른 종류의 구조를 만듭니다 . 이들은 Jacobian 구조 로 닫힙니다.
J f :: (i -> *) -> ((o, i) -> *)
각각의 결과 (o, i)구조는 편미분 i으로 o구조 에서 요소 구멍 을 만드는 방법을 알려줍니다 . 그러나 그것은 다른 시간 동안 의존적으로 입력 된 재미입니다.
Comonad지퍼에 대한 인스턴스입니다 하지
instance (Diff t, Diff (D t)) => Comonad (Zipper t) where
extract = here
duplicate = fmap outOf . inTo
인스턴스 자체 에서 어디 outOf에서 inTo왔는지 . 위의 경우는 법에 위배 됩니다. 대신 다음과 같이 작동합니다.DiffZipper tComonadfmap extract . duplicate == id
fmap extract . duplicate == \z -> fmap (const (here z)) z
Diff (지퍼 t)
에 대한 Diff인스턴스 Zipper는 제품을 제품으로 식별하고 제품 코드를 재사용하여 제공됩니다 (아래).
-- 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))
데이터 유형 간의 동형 및 파생 항목 간의 동형이 주어지면 한 유형 inTo과 outOf다른 유형을 재사용 할 수 있습니다 .
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
기존 Diff인스턴스의 newType에 불과한 유형의 경우 파생 항목은 동일한 유형입니다. 유형 검사기에 해당 유형 equality에 대해 알려 주면 D r ~ D t파생물에 동형을 제공하는 대신이를 활용할 수 있습니다.
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
이러한 도구를 갖추고 있으므로 Diff제품을 구현하기 위해 인스턴스를 재사용 할 수 있습니다.Diff (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
보일러 플레이트
여기에 제시된 코드를 실제로 사용하려면 몇 가지 언어 확장, 가져 오기 및 제안 된 문제의 수정이 필요합니다.
{-# 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
제품, 합계 및 상수
Diff (Zipper t)인스턴스의 구현에 의존하는 Diff제품 :*:, 금액 :+:, 상수 Identity, 제로 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
빈 예
I posed the Bin example as an isomorphism to a sum of products. We need not only its derivative but its second derivative as well
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
The example data from the previous answer is
aTree :: Bin Int
aTree =
(Bin . InL) (
(Bin . InL) (
(Bin . InR) (Identity 2)
:*: (Identity 1) :*:
(Bin . InR) (Identity 3)
)
:*: (Identity 0) :*:
(Bin . InR) (Identity 4)
)
Not the Comonad instance
The Bin example above provides a counter-example to fmap outOf . inTo being the correct implementation of duplicate for Zipper t. In particular, it provides a counter-example to the fmap extract . duplicate = id law:
fmap ( \z -> (fmap extract . duplicate) z == z) . inTo $ aTree
Which evaluates to (notice how it is full of Falses everywhere, any False would be enough to disprove the law)
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 aTree is a tree with the same structure as aTree, but everywhere there was a value there is instead a zipper with the value, and the remainder of the tree with all of the original values intact. fmap (fmap extract . duplicate) . inTo $ aTree is also a tree with the same structure as aTree, but everywere there was a value there is instead a zipper with the value, and the remainder of the tree with all of the values replaced with that same value. In other words:
fmap extract . duplicate == \z -> fmap (const (here z)) z
The complete test-suite for all three Comonad laws, extract . duplicate == id, fmap extract . duplicate == id, and duplicate . duplicate == fmap duplicate . duplicate is
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
Given an infinitely differentiable Diff class:
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))
around can be written in terms of up and down on the Zipper's diff's derivitive, essentially as
around z@(Zipper d h) = Zipper ctx z
where
ctx = fmap (\z' -> Zipper (up z') (here z')) (down d)
The Zipper t a consists of a D t a and an a. We go down the D t a, getting a D t (Zipper (D t) a) with a zipper in every hole. Those zippers consists of a D (D t) a and the a that was in the hole. We go up each of them, getting a D t a and paring it with the a that was in the hole. A D t a and an a make a Zipper t a, giving us a D t (Zipper t a), which is the context needed for a Zipper t (Zipper t a).
The Comonad instance is then simply
instance Diff t => Comonad (Zipper t) where
extract = here
duplicate = around
Capturing the derivative's Diff dictionary requires some additional plumbing, which can be done with Data.Constraint or in terms of the method presented in a related answer
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
참고URL : https://stackoverflow.com/questions/25554062/zipper-comonads-generically
'Programing' 카테고리의 다른 글
| open_basedir 제한이 적용됩니다. (0) | 2020.10.08 |
|---|---|
| 스레드가 처리되지 않은 예외없이 코드 0 (0x0)으로 종료되었습니다. (0) | 2020.10.08 |
| Spring MVC 애플리케이션에서 Swagger를 구현하는 '간단한'방법 (0) | 2020.10.08 |
| 속성으로 필터링 (0) | 2020.10.08 |
| 파이썬의 조건부 연산자? (0) | 2020.10.08 |