为n维网格类型编写cojoin或cobind

Question

使用类型级自然的典型定义,我已经定义了一个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

使用cojoin上的n维网格将产生n维网格的n维网格.我想提供一个实例以相同的思路这一块,这就是价值的的cojoined格在(X,Y,Z)应该是原来的电网集中于(X,Y,Z).为了适应该代码,似乎我们需要n进行n修改以执行"fmaps"和n"roll".你不必这样做,但如果这有帮助,那么你去吧.

Answer 1

贾格尔/理查兹:你不能总是得到你想要的东西,但如果你有时候尝试,你可能会发现你得到了你需要的东西.

列表中的游标

让我使用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)

我们有共同点

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始终是一个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焦点已被装饰成2的光标; 在左边,我们有光标在1的列表; 在右边,是光标在3和光标在4的列表.

组合游标,移植游标？

现在,你要求成为a的结构Comonad是n倍的组合Cursor.让我们

newtype (:.:) f g x = C {unC :: f (g x)} deriving Show

为了说服comonads f和g撰写,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序列的两种方式都可以得到相同的结果.

我们可以自己定义一个transposefor Cursor吗？廉价地获得某种换位的一种方法是注意Bwd并且Fwd适用于zippily,因此也是如此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允许内部结构相对于彼此粗糙,所以不transpose,不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-structure-all-the-same-shaped"的f结构的概念.这就是不可估量的Peter Hancock所说的"张量积",我将写道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 for Tensor Products

现在,你可以在高中所学,?(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总是一个Comonad,这告诉我们InContexts的张量积是comonadic因为它们本身就是InContexts.也就是说,你在每个维度上选择一个位置(并且在整个事物中只给出一个位置),之前我们有一个外部位置和许多内部位置.随着张量产品取代组合物,一切都很甜美.

Naperian Functors

但是有一个子类,Functor张量积和组合物重合.这些是Functor小号f为其f () ~ ():即,仅存在一个形状无论如何,所以在组合物褴褛值首先被排除.这些Functors (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 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维数组确实是一个comonad.向量的组成是n个向量的张量积,因为向量是Naperian.但是Focusedn维阵列将是决定其尺寸的n个向量的n倍张量积,而不是 n 的成分Focused.为了用拉链表达这个comonad,我们需要以一种可以构造张量积的形式表达它们.我将把它作为未来的练习.

Answer 2

还有一个尝试,受到猪科工作者的启发和http://hackage.haskell.org/packages/archive/representable-functors/3.0.0.1/doc/html/Data-Functor-Representable.html.

如果键(或日志)是一个幺半群,那么一个可表示的(或Naperian)仿函数就是一个comonad本身!然后coreturn得到位置的值mempty.和cojoin mappends具有可用这两个键.(就像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在两种情况下拆分实例,一个用于Z,一个用于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)

而关键U n是确实是一个幺半群,所以我们可以U n使用来自representable-functor包的默认实现变成一个comonad.

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)