56

使用类型级自然值的典型定义,我定义了一个 n 维网格。

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Nat = Z | S Nat

data U (n :: Nat) x where
  Point :: x -> U Z x
  Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x

dmap :: (U n x -> U m r) -> U (S n) x -> U (S m) r
dmap f (Dimension ls mid rs) = Dimension (map f ls) (f mid) (map f rs)

instance Functor (U n) where
  fmap f (Point x) = Point (f x)
  fmap f d@Dimension{} = dmap (fmap f) d

现在我想让它成为 Comonad 的一个实例,但我无法完全理解它。

class Functor w => Comonad w where
  (=>>)    :: w a -> (w a -> b) -> w b
  coreturn :: w a -> a
  cojoin   :: w a -> w (w a)

  x =>> f = fmap f (cojoin x)
  cojoin xx = xx =>> id

instance Comonad (U n) where
  coreturn (Point x) = x
  coreturn (Dimension _ mid _) = coreturn mid

  -- cojoin :: U Z x -> U Z (U Z x)
  cojoin (Point x) = Point (Point x)
  -- cojoin ::U (S n) x -> U (S n) (U (S n) x)
  cojoin d@Dimension{} = undefined

  -- =>> :: U Z x -> (U Z x -> r) -> U Z r
  p@Point{} =>> f = Point (f p)
  -- =>> :: U (S n) x -> (U (S n) x -> r) -> U (S n) r
  d@Dimension{} =>> f = undefined

在 n 维网格上使用cojoin将产生 n 维网格的 n 维网格。我想提供一个与这个想法相同的实例,( x,y,z)处的联合网格的值应该是聚焦于(x,y,z)的原始网格。为了调整该代码,我们似乎需要进行具体化以执行“fmaps”和“rolls”。您不必那样做,但如果这有帮助,那么您就可以了。nnn

4

3 回答 3

53

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

为了说服comonadsfg组合,counits组合整齐,但你需要一个“分配律”

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 的某些序列从一个顺序转换到另一个顺序的任何两种方法都会给出相同的结果。

我们可以用它自己定义一个transposeforCursor吗?一种廉价地获得某种转置的方法是注意它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')

这就像一个广义矩阵:一对形状给出尺寸,然后在每对位置都有一个元素。当类型pp'依赖于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,这告诉我们InContexts 的张量积是共元的,因为它们本身就是InContexts。也就是说,你在每个维度上选择一个位置(这给了你在整个事物中的一个位置),而之前我们有一个外部位置和许多内部位置。随着张量积取代组合,一切都很好。

纳佩尔函子

但是有一个子类,Functor其张量积和合成重合。这些是Functors :ff () ~ (),无论如何只有一个形状,因此首先排除了构图中的参差不齐的值。对于我们可以将其视为对的某些位置集,这些Functors 都是同构的(必须提高指数才能给出)。相应地,汉考克以约翰·纳皮尔(他的鬼魂出没于汉考克居住的爱丁堡部分)之后称这些函子。(p ->)pxf xNaperian

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 ffor的版本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

因此,特别是,Focusedn 维数组确实是一个共单子。向量的组合是 n 个向量的张量积,因为向量是Naperian。但是Focusedn 维数组将是决定其维度的 n 个向量的 n 倍张量积,而不是组合。Focused为了用 zippers 来表达这个comonad,我们需要用一种可以构造张量积的形式来表达它们。我会把它留作将来的练习。

于 2012-10-27T14:03:58.870 回答
12

又一次尝试,灵感来自 pigworkers 帖子和http://hackage.haskell.org/packages/archive/representable-functors/3.0.0.1/doc/html/Data-Functor-Representable.html

如果键(或对数)是幺半群,则可表示(或 Naperian)函子本身就是共单子!然后coreturn获取 position 的值mempty。它有cojoin mappend两个可用的键。(就像 . 的comonad 实例一样(p ->)。)

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.List (genericIndex)
import Data.Monoid
import Data.Key
import Data.Functor.Representable

data Nat = Z | S Nat

data U (n :: Nat) x where
  Point :: x -> U Z x
  Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x

dmap :: (U n x -> U m r) -> U (S n) x -> U (S m) r
dmap f (Dimension ls mid rs) = Dimension (map f ls) (f mid) (map f rs)

instance Functor (U n) where
  fmap f (Point x) = Point (f x)
  fmap f d@Dimension{} = dmap (fmap f) d

class Functor w => Comonad w where
  (=>>)    :: w a -> (w a -> b) -> w b
  coreturn :: w a -> a
  cojoin   :: w a -> w (w a)

  x =>> f = fmap f (cojoin x)
  cojoin xx = xx =>> id

U如果列表无限长,则可以表示。然后只有一种形状。的键U n是一个包含 n 个整数的向量。

type instance Key (U n) = UKey n

data UKey (n :: Nat) where
  P :: UKey Z
  D :: Integer -> UKey n -> UKey (S n)

instance Lookup (U n) where lookup = lookupDefault
instance Indexable (U n) where
  index (Point x) P = x
  index (Dimension ls mid rs) (D i k) 
    | i < 0 = index (ls `genericIndex` (-i - 1)) k
    | i > 0 = index (rs `genericIndex` ( i - 1)) k
    | otherwise = index mid k

我们需要将Representable实例拆分为两种情况,一种是 for Z,一种是 for S,因为我们没有U n用于模式匹配的类型值。

instance Representable (U Z) where
  tabulate f = Point (f P)
instance Representable (U n) => Representable (U (S n)) where
  tabulate f = Dimension 
    (map (\i -> tabulate (f . D (-i))) [1..]) 
    (tabulate (f . D 0))
    (map (\i -> tabulate (f . D   i)) [1..])

instance Monoid (UKey Z) where
  mempty = P
  mappend P P = P
instance Monoid (UKey n) => Monoid (UKey (S n)) where
  mempty = D 0 mempty
  mappend (D il kl) (D ir kr) = D (il + ir) (mappend kl kr)

并且 keyU n确实是一个幺半群,所以我们可以U n变成一个comonad,使用来自representable-functor 包的默认实现。

instance (Monoid (UKey n), Representable (U n)) => Comonad (U n) where
  coreturn = extractRep
  cojoin = duplicateRep
  (=>>) = flip extendRep

这次我做了一些测试。

testVal :: U (S (S Z)) Int
testVal = Dimension 
  (repeat (Dimension (repeat (Point 1)) (Point 2) (repeat (Point 3))))
          (Dimension (repeat (Point 4)) (Point 5) (repeat (Point 6)))
  (repeat (Dimension (repeat (Point 7)) (Point 8) (repeat (Point 9))))

-- Hacky Eq instance, just for testing
instance Eq x => Eq (U n x) where
  Point a == Point b = a == b
  Dimension la a ra == Dimension lb b rb = take 3 la == take 3 lb && a == b && take 3 ra == take 3 rb

instance Show x => Show (U n x) where
  show (Point x) = "(Point " ++ show x ++ ")"
  show (Dimension l a r) = "(Dimension " ++ show (take 2 l) ++ " " ++ show a ++ " " ++ show (take 2 r) ++ ")"

test = 
  coreturn (cojoin testVal) == testVal && 
  fmap coreturn (cojoin testVal) == testVal && 
  cojoin (cojoin testVal) == fmap cojoin (cojoin testVal)
于 2012-10-27T16:44:15.040 回答
2

所以这被证明是错误的。我会把它留在这里,以防有人想尝试修复它。

这个实现是我认为@pigworker 建议的方式。它可以编译,但我还没有测试过。(我cojoin1http://blog.sigfpe.com/2006/12/evalating-cellular-automata-is.html获取了实现)

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Nat = Z | S Nat

data U (n :: Nat) x where
  Point :: x -> U Z x
  Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x

unPoint :: U Z x -> x
unPoint (Point x) = x

dmap :: (U n x -> U m r) -> U (S n) x -> U (S m) r
dmap f (Dimension ls mid rs) = Dimension (map f ls) (f mid) (map f rs)

right, left :: U (S n) x -> U (S n) x
right (Dimension a b (c:cs)) = Dimension (b:a) c cs
left  (Dimension (a:as) b c) = Dimension as a (b:c)

instance Functor (U n) where
  fmap f (Point x) = Point (f x)
  fmap f d@Dimension{} = dmap (fmap f) d

class Functor w => Comonad w where
  (=>>)    :: w a -> (w a -> b) -> w b
  coreturn :: w a -> a
  cojoin   :: w a -> w (w a)

  x =>> f = fmap f (cojoin x)
  cojoin xx = xx =>> id

instance Comonad (U n) where
  coreturn (Point x) = x
  coreturn (Dimension _ mid _) = coreturn mid
  cojoin (Point x) = Point (Point x)
  cojoin d@Dimension{} = fmap unlayer . unlayer . fmap dist . cojoin1 . fmap cojoin . layer $ d

dist :: U (S Z) (U n x) -> U n (U (S Z) x)
dist = layerUnder . unlayer

layerUnder :: U (S n) x -> U n (U (S Z) x)
layerUnder d@(Dimension _ Point{} _) = Point d
layerUnder d@(Dimension _ Dimension{} _) = dmap layerUnder d

unlayer :: U (S Z) (U n x) -> U (S n) x
unlayer = dmap unPoint

layer :: U (S n) x -> U (S Z) (U n x)
layer = dmap Point

cojoin1 :: U (S Z) x -> U (S Z) (U (S Z) x)
cojoin1 a = layer $ Dimension (tail $ iterate left a) a (tail $ iterate right a)
于 2012-10-27T12:02:28.810 回答