就像《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}
它是一个具有导数的函子,导数也是一个函子。导数代表一个单洞上下文element。拉链类型ZF f x
表示单洞上下文和洞中元素的对。
的操作为Diff1
描述我们可以在拉链上进行的导航类型(没有任何“向左”和“向右”的概念,请参阅我的小丑和小丑纸)。我们可以“向上”,通过将元件插入孔中来重新组装结构。我们可以“向下”寻找访问给定结构中元素的所有方法:我们用其上下文来装饰每个元素。我们可以“绕”走,
采用现有的拉链并用其上下文装饰每个元素,因此我们找到了重新聚焦的所有方法(以及如何保持当前的焦点)。
现在,类型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
多项式函子是可微的
Constant函子是可微的。
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
or downF
从,我们很容易找到所有没有的路可走downF
.
The identity函子是可微的。
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))
To go 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
.
Product保留可微分性。
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
要关注一对元素中的一个元素,您可以关注左侧并保留右侧,反之亦然。莱布尼茨著名的乘积法则对应的是简单的空间直觉!
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)
Now, downF
其工作方式与求和的方式类似,只是我们不仅必须使用标签(以显示我们走的方向)而且还必须使用未触及的其他组件来修复拉链上下文。
downF (f :*: g)
= fmap (\ (f' :<-: x) -> LF (f' :*: g) :<-: x) (downF f)
:*: fmap (\ (g' :<-: x) -> RF (f :*: g') :<-: x) (downF g)
But aroundF
是一大堆笑声。无论我们目前访问哪一方,我们都有两个选择:
- Move
aroundF
在那一边。
- Move
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))
Exercise使用以下公式证明可微函子的组成是可微的链式法则.
甜的!我们现在可以回家了吗?当然不是。我们没有区分任何递归的结构尚未。
从双函子制作递归函子
A Bifunctor
正如关于数据类型泛型编程的现有文献(参见 Patrik Jansson 和 Johan Jeuring 的工作,或 Jeremy Gibbons 的精彩讲义)详细解释的那样,它是一个具有两个参数的类型构造函数,对应于两种子结构。我们应该能够“映射”两者。
class Bifunctor b where
bimap :: (x -> x') -> (y -> y') -> b x y -> b x' y'
我们可以用Bifunctor
s 给出递归容器的节点结构。每个节点有subnodes and elements。这些只是两种子结构。
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
实例。
双函数套件
常数是双函数的。
newtype K a x y = K a
instance Bifunctor (K a) where
bimap f g (K a) = K a
你可以看出我先写了这一点,因为标识符更短,但这很好,因为代码更长。
变量是双函数的。
我们需要与一个参数或另一个参数相对应的双函子,因此我创建了一种数据类型来区分它们,然后定义了一个合适的 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
and 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)
Sums and Products的双函子是双函子
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)))
如果您想将这些类型用于实际数据,而不是盲目遵循乔治·修拉的点画传统,请使用模式同义词.
但是拉链呢?我们该如何证明这一点Mu b
是可微分的吗?我们需要证明b
可微分于both变量。铛!是时候学习部分微分了。
双函子的偏导数
因为我们有两个变量,所以我们需要能够有时集体讨论它们,有时单独讨论它们。我们需要单身家庭:
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}
This D
操作需要知道要定位哪个变量。对应的拉链Z b v
告诉我们哪个变量v
必须是焦点。当我们“用上下文装饰”时,我们要装饰x
-元素与X
- 背景和y
-元素与Y
- 上下文。但除此之外,都是同一个故事。
我们还有两个任务:首先,证明我们的双函子套件是可微的;其次,为了表明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
这次,生命太短,无法发展类型级别克罗内克三角洲的理论,所以我只是单独处理变量。
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
and 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
作为我还没有准备好工作的地方的存根,并在我需要类型检查器提供有用提示的地方(在任何给定时间)引入故意的类型错误。即使在 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))})
但我们需要element-拉链。
双函子固定点的元素拉链
每个元素都位于节点内的某个位置。该节点位于一堆X
-衍生品。但是该节点中元素的位置由Y
-衍生物。我们得到
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))
Now, down b
只带我们进入节点。我们需要的拉链还必须携带节点的上下文。就是这样contextualise
does:
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
-position,我们必须给出一个元素拉链,所以我们知道整个上下文是件好事dXs
回到根源,以及dY
它描述了元素如何位于其节点中。对于每一个X
-position,还有一个子树需要探索,所以我们增加堆栈并继续!
剩下的就是转移焦点的事情了。我们可能会留在原地,或者从现在的位置下降,或者上升,或者上升然后沿着其他路径走下去。开始。
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
-重新组装我们正在访问的节点后的导数。
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
不同种类的元素。这些都是closed雅可比行列式构造下
J f :: (i -> *) -> ((o, i) -> *)
其中每个结果(o, i)
-structs 是一个偏导数,告诉你如何制作一个i
- 元素孔o
-结构。但这又是依赖类型的乐趣。