Jagger/Richards:你不能总是得到你想要的,但如果你尝试一下,你可能会发现你得到了你需要的。
列表中的光标
让我使用 snoc- 和 cons-lists 重建结构的组件,以保持空间属性清晰。我定义
data Bwd x = B0 | Bwd x :< x deriving (Functor, Foldable, Traversable, Show)
data Fwd x = F0 | x :> Fwd x deriving (Functor, Foldable, Traversable, Show)
infixl 5 :<
infixr 5 :>
data Cursor x = Cur (Bwd x) x (Fwd x) deriving (Functor, Foldable, Traversable, Show)
让我们有comonads
class Functor f => Comonad f where
counit :: f x -> x
cojoin :: f x -> f (f x)
让我们确保游标是comonads
instance Comonad Cursor where
counit (Cur _ x _) = x
cojoin c = Cur (lefts c) c (rights c) where
lefts (Cur B0 _ _) = B0
lefts (Cur (xz :< x) y ys) = lefts c :< c where c = Cur xz x (y :> ys)
rights (Cur _ _ F0) = F0
rights (Cur xz x (y :> ys)) = c :> rights c where c = Cur (xz :< x) y ys
如果您开始使用这种东西,您会注意到这Cursor
是一种令人愉悦的空间变体InContext []
InContext f x = (x, ∂f x)
其中∂取函子的形式导数,给出单孔上下文的概念。InContext f
总是 a Comonad
,正如这个答案中提到的那样,我们在这里所拥有的只是Comonad
由微分结构引起的,其中counit
提取焦点处的cojoin
元素并用自己的上下文装饰每个元素,有效地为您提供一个充满重新聚焦光标的上下文和在其焦点处有一个未移动的光标。让我们举个例子。
> cojoin (Cur (B0 :< 1) 2 (3 :> 4 :> F0))
Cur (B0 :< Cur B0 1 (2 :> 3 :> 4 :> F0))
(Cur (B0 :< 1) 2 (3 :> 4 :> F0))
( Cur (B0 :< 1 :< 2) 3 (4 :> F0)
:> Cur (B0 :< 1 :< 2 :< 3) 4 F0
:> F0)
看?焦点中的 2 已被修饰为 cursor-at-2;在左边,我们有 cursor-at-1 的列表;右侧是 cursor-at-3 和 cursor-at-4 的列表。
组合游标,转置游标?
现在,您要求成为 a 的结构Comonad
是 的 n 倍组合Cursor
。让我们
newtype (:.:) f g x = C {unC :: f (g x)} deriving Show
为了说服comonadsf
和g
组合,counit
s组合整齐,但你需要一个“分配律”
transpose :: f (g x) -> g (f x)
cojoin
所以你可以像这样制作复合材料
f (g x)
-(fmap cojoin)->
f (g (g x))
-cojoin->
f (f (g (g x)))
-(fmap transpose)->
f (g (f (g x)))
transpose
应该满足哪些法律?大概是这样的
counit . transpose = fmap counit
cojoin . transpose = fmap transpose . transpose . fmap cojoin
或者采取任何措施来确保将 f 和 g 的某些序列从一个顺序转换到另一个顺序的任何两种方法都会给出相同的结果。
我们可以用它自己定义一个transpose
forCursor
吗?一种廉价地获得某种转置的方法是注意它Bwd
并且Fwd
是快速适用的,因此也是如此Cursor
。
instance Applicative Bwd where
pure x = pure x :< x
(fz :< f) <*> (sz :< s) = (fz <*> sz) :< f s
_ <*> _ = B0
instance Applicative Fwd where
pure x = x :> pure x
(f :> fs) <*> (s :> ss) = f s :> (fs <*> ss)
_ <*> _ = F0
instance Applicative Cursor where
pure x = Cur (pure x) x (pure x)
Cur fz f fs <*> Cur sz s ss = Cur (fz <*> sz) (f s) (fs <*> ss)
在这里你应该开始闻到老鼠的味道。形状不匹配会导致截断,这将破坏自转置是自反转的明显理想属性。任何形式的衣衫褴褛都无法生存。我们确实得到了一个转置算子:sequenceA
,对于完全正则的数据,一切都是美好的。
> regularMatrixCursor
Cur (B0 :< Cur (B0 :< 1) 2 (3 :> F0))
(Cur (B0 :< 4) 5 (6 :> F0))
(Cur (B0 :< 7) 8 (9 :> F0) :> F0)
> sequenceA regularMatrixCursor
Cur (B0 :< Cur (B0 :< 1) 4 (7 :> F0))
(Cur (B0 :< 2) 5 (8 :> F0))
(Cur (B0 :< 3) 6 (9 :> F0) :> F0)
但是,即使我只是将其中一个内部光标移出对齐(别介意使尺寸参差不齐),事情也会出错。
> raggedyMatrixCursor
Cur (B0 :< Cur ((B0 :< 1) :< 2) 3 F0)
(Cur (B0 :< 4) 5 (6 :> F0))
(Cur (B0 :< 7) 8 (9 :> F0) :> F0)
> sequenceA raggedyMatrixCursor
Cur (B0 :< Cur (B0 :< 2) 4 (7 :> F0))
(Cur (B0 :< 3) 5 (8 :> F0))
F0
当您有一个外部光标位置和多个内部光标位置时,没有表现良好的换位。自组合Cursor
允许内部结构相对于彼此参差不齐,所以 no transpose
, no cojoin
。你可以,我也确实,定义
instance (Comonad f, Traversable f, Comonad g, Applicative g) =>
Comonad (f :.: g) where
counit = counit . counit . unC
cojoin = C . fmap (fmap C . sequenceA) . cojoin . fmap cojoin . unC
但我们有责任确保我们保持内部结构正常。如果你愿意接受这个负担,那么你可以迭代,因为Applicative
并且Traversable
很容易在组合下关闭。这里是点点滴滴
instance (Functor f, Functor g) => Functor (f :.: g) where
fmap h (C fgx) = C (fmap (fmap h) fgx)
instance (Applicative f, Applicative g) => Applicative (f :.: g) where
pure = C . pure . pure
C f <*> C s = C (pure (<*>) <*> f <*> s)
instance (Functor f, Foldable f, Foldable g) => Foldable (f :.: g) where
fold = fold . fmap fold . unC
instance (Traversable f, Traversable g) => Traversable (f :.: g) where
traverse h (C fgx) = C <$> traverse (traverse h) fgx
编辑:为了完整起见,这就是一切正常时的作用,
> cojoin (C regularMatrixCursor)
C {unC = Cur (B0 :< Cur (B0 :<
C {unC = Cur B0 (Cur B0 1 (2 :> (3 :> F0))) (Cur B0 4 (5 :> (6 :> F0)) :> (Cur B0 7 (8 :> (9 :> F0)) :> F0))})
(C {unC = Cur B0 (Cur (B0 :< 1) 2 (3 :> F0)) (Cur (B0 :< 4) 5 (6 :> F0) :> (Cur (B0 :< 7) 8 (9 :> F0) :> F0))})
(C {unC = Cur B0 (Cur ((B0 :< 1) :< 2) 3 F0) (Cur ((B0 :< 4) :< 5) 6 F0 :> (Cur ((B0 :< 7) :< 8) 9 F0 :> F0))} :> F0))
(Cur (B0 :<
C {unC = Cur (B0 :< Cur B0 1 (2 :> (3 :> F0))) (Cur B0 4 (5 :> (6 :> F0))) (Cur B0 7 (8 :> (9 :> F0)) :> F0)})
(C {unC = Cur (B0 :< Cur (B0 :< 1) 2 (3 :> F0)) (Cur (B0 :< 4) 5 (6 :> F0)) (Cur (B0 :< 7) 8 (9 :> F0) :> F0)})
(C {unC = Cur (B0 :< Cur ((B0 :< 1) :< 2) 3 F0) (Cur ((B0 :< 4) :< 5) 6 F0) (Cur ((B0 :< 7) :< 8) 9 F0 :> F0)} :> F0))
(Cur (B0 :<
C {unC = Cur ((B0 :< Cur B0 1 (2 :> (3 :> F0))) :< Cur B0 4 (5 :> (6 :> F0))) (Cur B0 7 (8 :> (9 :> F0))) F0})
(C {unC = Cur ((B0 :< Cur (B0 :< 1) 2 (3 :> F0)) :< Cur (B0 :< 4) 5 (6 :> F0)) (Cur (B0 :< 7) 8 (9 :> F0)) F0})
(C {unC = Cur ((B0 :< Cur ((B0 :< 1) :< 2) 3 F0) :< Cur ((B0 :< 4) :< 5) 6 F0) (Cur ((B0 :< 7) :< 8) 9 F0) F0} :> F0)
:> F0)}
汉考克的张量积
对于规律性,你需要比组合更强大的东西。您需要能够捕捉到“g-structures-all-the-same-shape 的 f 结构”的概念。这就是不可估量的彼得汉考克所说的“张量积”,我会写f :><: g
:所有内部 g 结构都有一个“外部”f 形和一个“内部”g 形,因此转置很容易定义并且总是自逆。Hancock 的张量在 Haskell 中不能方便地定义,但在依赖类型的设置中,很容易制定一个具有该张量的“容器”概念。
为了给你这个想法,考虑一个退化的容器概念
data (:<|) s p x = s :<| (p -> x)
我们说s
的是“形状”p
的类型和“位置”的类型。一个值由形状的选择和x
每个位置的存储组成。在从属情况下,位置的类型可能取决于形状的选择(例如,对于列表,形状是一个数字(长度),并且您有那么多位置)。这些容器有一个张量积
(s :<| p) :><: (s' :<| p') = (s, s') :<| (p, p')
这就像一个广义矩阵:一对形状给出尺寸,然后在每对位置都有一个元素。当类型p
和p'
依赖于s
和中的值时,您可以完美地做到这一点s'
,这正是汉考克对容器张量积的定义。
张量积的 InContext
现在,正如您在高中时可能已经了解到的那样,∂(s :<| p) = (s, p) :<| (p-1)
哪里p-1
有比 . 少一个元素的类型p
。就像∂(s x^p) = (s p)*x^(p-1)。您选择一个位置(将其记录在形状中)并将其删除。问题是p-1
在没有依赖类型的情况下很难掌握。但是InContext
选择一个位置而不删除它。
InContext (s :<| p) ~= (s, p) :<| p
这同样适用于从属情况,我们很高兴地获得
InContext (f :><: g) ~= InContext f :><: InContext g
现在我们知道它InContext f
总是 a Comonad
,这告诉我们InContext
s 的张量积是共元的,因为它们本身就是InContext
s。也就是说,你在每个维度上选择一个位置(这给了你在整个事物中的一个位置),而之前我们有一个外部位置和许多内部位置。随着张量积取代组合,一切都很好。
纳佩尔函子
但是有一个子类,Functor
其张量积和合成重合。这些是Functor
s :f
即f () ~ ()
,无论如何只有一个形状,因此首先排除了构图中的参差不齐的值。对于我们可以将其视为对数的某些位置集,这些Functor
s 都是同构的(必须提高指数才能给出)。相应地,汉考克以约翰·纳皮尔(他的鬼魂出没于汉考克居住的爱丁堡部分)之后称这些函子。(p ->)
p
x
f x
Naperian
class Applicative f => Naperian f where
type Log f
project :: f x -> Log f -> x
positions :: f (Log f)
--- project positions = id
Naperian
函子有一个对数,将离子project
函数映射到那里找到的元素的位置。Naperian
函子都是 zippily Applicative
,具有pure
并<*>
对应于投影的 K 和 S 组合子。也可以构造一个值,在每个位置存储该位置的表示。您可能记得的对数定律令人愉快地弹出。
newtype Id x = Id {unId :: x} deriving Show
instance Naperian Id where
type Log Id = ()
project (Id x) () = x
positions = Id ()
newtype (:*:) f g x = Pr (f x, g x) deriving Show
instance (Naperian f, Naperian g) => Naperian (f :*: g) where
type Log (f :*: g) = Either (Log f) (Log g)
project (Pr (fx, gx)) (Left p) = project fx p
project (Pr (fx, gx)) (Right p) = project gx p
positions = Pr (fmap Left positions, fmap Right positions)
请注意,固定大小的数组(向量)由 给出(Id :*: Id :*: ... :*: Id :*: One)
,其中One
是常数单位函子,其对数为Void
。所以一个数组是Naperian
. 现在,我们也有
instance (Naperian f, Naperian g) => Naperian (f :.: g) where
type Log (f :.: g) = (Log f, Log g)
project (C fgx) (p, q) = project (project fgx p) q
positions = C $ fmap (\ p -> fmap (p ,) positions) positions
这意味着多维数组是Naperian
.
要构造InContext f
for的版本Naperian f
,只需指向一个位置!
data Focused f x = f x :@ Log f
instance Functor f => Functor (Focused f) where
fmap h (fx :@ p) = fmap h fx :@ p
instance Naperian f => Comonad (Focused f) where
counit (fx :@ p) = project fx p
cojoin (fx :@ p) = fmap (fx :@) positions :@ p
因此,特别是,Focused
n 维数组确实是一个共单子。向量的组合是 n 个向量的张量积,因为向量是Naperian
。但是Focused
n 维数组将是决定其维度的 n 个向量的 n 倍张量积,而不是组合。Focused
为了用 zippers 来表达这个comonad,我们需要用一种可以构造张量积的形式来表达它们。我会把它留作将来的练习。