Ответ 1
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 всегда 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; справа, список курсора-at-3 и курсор-4.
Составляющие курсоры, транспонирование курсоров?
Теперь структура, которую вы просите быть Comonad, представляет собой n-кратный состав Cursor. Пусть <
newtype (:.:) f g x = C {unC :: f (g x)} deriving Show
Чтобы убедить comonads f и g составить, counit составить аккуратно, но вам нужен "дистрибутивный закон"
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
или что бы это ни потребовалось, чтобы гарантировать, что любые два способа shoogle некоторые последовательности из f и g из одного порядка в другой дают тот же результат.
Можно ли определить transpose для Cursor с собой? Один из способов получить какую-то перестановку дешево - это отметить, что Bwd и Fwd zippily applyative, следовательно, так 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)}
Хенкок-тензорный продукт
Для регулярности вам нужно нечто большее, чем состав. Вы должны уметь фиксировать понятие "f-структуры g-структур-все-одинаковой формы". Это то, что неоценимый Питер Хэнкок называет "тензорным продуктом", который я напишу f :><: g: там есть одна "внешняя" f-форма и одна "внутренняя" g-форма, общая для всех внутренних g-структур, поэтому транспозиция легко определяется и всегда самообращается. Тензор Хэнкока не удобно определить в Хаскелле, но в зависимой типизированной постановке легко сформулировать понятие "контейнера", имеющего этот тензор.
Чтобы дать вам эту идею, рассмотрим вырожденное понятие контейнера
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. Подобно ∂ (sx ^ p) = (sp) * x ^ (p-1). Вы выбираете одну позицию (записываете ее в форме) и удаляете ее. Недостатком является то, что p-1 сложно использовать без зависимых типов. Но InContext выбирает позицию, не удаляя ее.
InContext (s :<| p) ~= (s, p) :<| p
Это работает так же хорошо для зависимого случая, и мы радостно получаем
InContext (f :><: g) ~= InContext f :><: InContext g
Теперь мы знаем, что InContext f всегда a Comonad, и это говорит о том, что тензорные произведения из InContext являются comonadic, потому что они сами являются InContext s. Это означает, что вы выбираете одну позицию за измерение (и это дает вам ровно одну позицию во всем этом), где раньше у нас было одно внешнее положение и много внутренних позиций. При замене композиции тензора, все работает сладко.
Функторы Naperian
Но существует подкласс Functor, для которого тензорное произведение и композиция совпадают. Это Functor f, для которых f () ~ (): т.е. В любом случае существует только одна форма, поэтому в первую очередь исключаются значения изнасилования в композициях. Эти Functor все изоморфны (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
A Naperian имеет логарифм, индуцирующий положение функции ионной функции a 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 для 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
Итак, в частности, a Focused n-мерный массив действительно будет comonad. Композиция векторов является тензорным произведением n векторов, поскольку векторы Naperian. Но n-мерным массивом Focused будет n-кратное тензорное произведение, а не композиция векторов n Focused, определяющих его размеры. Чтобы выразить эту комонаду в терминах молнии, нам нужно выразить их в форме, которая позволяет построить тензорное произведение. Я оставлю это как упражнение на будущее.