Comonads на молнии, как правило

Question

Comonads на молнии, как правило

Для любого типа контейнера мы можем сформировать (элементно-ориентированную) молнию и знать, что эта структура является Comonad. Это было недавно подробно изучено в другом вопросе переполнения стека для следующего типа:

data Bin a = Branch (Bin a) a (Bin a) | Leaf a deriving Functor

со следующей молнией

data Dir = L | R
data Step a = Step a Dir (Bin a)   deriving Functor
data Zip  a = Zip [Step a] (Bin a) deriving Functor
instance Comonad Zip where ...

Это тот случай, когда Zip это Comonad хотя конструкция его экземпляра немного волосатая. Это сказало, Zip может быть полностью механически получен из Tree и (я считаю), любой тип, полученный таким образом, автоматически ComonadТак что я считаю, что должно быть так, что мы можем сконструировать эти типы и их комонады в общем и автоматическом режиме.

Одним из способов достижения общности при конструировании молнии является использование следующего класса и семейства типов.

data Zipper t a = Zipper { diff :: D t a, here :: a }

deriving instance Diff t => Functor (Zipper t)

class (Functor t, Functor (D t)) => Diff t where
  data D t :: * -> *
  inTo  :: t a -> t (Zipper t a)
  outOf :: Zipper t a -> t a

который (более или менее) появился в темах Haskell Cafe и в блоге Конала Эллиотта. Этот класс может быть реализован для различных основных алгебраических типов и, таким образом, обеспечивает общую основу для разговоров о производных ADT.

Итак, в конечном итоге, мой вопрос заключается в том, можем ли мы написать

instance Diff t => Comonad (Zipper t) where ...

который можно использовать для определения конкретного экземпляра Comonad, описанного выше:

instance Diff Bin where
  data D Bin a = DBin { context :: [Step a], descend :: Maybe (Bin a, Bin a) }
  ...

К сожалению, мне не повезло написать такой экземпляр. Это inTo/outOf подписи достаточно? Есть ли что-то еще, чтобы ограничить типы? Возможен ли этот случай?

83

haskell deriving zipper comonad

Источник

user476408 28 авг '14 в 16:51

3 ответа

Решение

Comonad Экземпляр для молнии не

instance (Diff t, Diff (D t)) => Comonad (Zipper t) where
    extract = here
    duplicate = fmap outOf . inTo

где outOf а также inTo исходить из Diff экземпляр для Zipper t сам. Приведенный выше случай нарушает Comonad закон fmap extract . duplicate == id, Вместо этого он ведет себя как:

fmap extract . duplicate == \z -> fmap (const (here z)) z

Дифф (молния т)

Diff экземпляр для Zipper обеспечивается путем идентификации их как продуктов и повторного использования кода для продуктов (ниже).

-- Zippers are themselves products
toZipper :: (D t :*: Identity) a -> Zipper t a
toZipper (d :*: (Identity h)) = Zipper d h

fromZipper :: Zipper t a -> (D t :*: Identity) a
fromZipper (Zipper d h) = (d :*: (Identity h))

Учитывая изоморфизм между типами данных и изоморфизм между их производными, мы можем повторно использовать один тип inTo а также outOf для другого.

inToFor' :: (Diff r) =>
            (forall a.   r a ->   t a) ->
            (forall a.   t a ->   r a) ->
            (forall a. D r a -> D t a) ->
            (forall a. D t a -> D r a) ->
            t a -> t (Zipper t a)
inToFor' to from toD fromD = to . fmap (onDiff toD) . inTo . from

outOfFor' :: (Diff r) =>
            (forall a.   r a ->   t a) ->
            (forall a.   t a ->   r a) ->
            (forall a. D r a -> D t a) ->
            (forall a. D t a -> D r a) ->
            Zipper t a -> t a
outOfFor' to from toD fromD = to . outOf . onDiff fromD

Для типов, которые являются просто newTypes для существующего Diff Например, их производные одного типа. Если мы расскажем контролеру типов об этом равенстве типов D r ~ D tмы можем воспользоваться этим вместо обеспечения изоморфизма производных.

inToFor :: (Diff r, D r ~ D t) =>
           (forall a. r a -> t a) ->
           (forall a. t a -> r a) ->
           t a -> t (Zipper t a)
inToFor to from = inToFor' to from id id

outOfFor :: (Diff r, D r ~ D t) =>
            (forall a. r a -> t a) ->
            (forall a. t a -> r a) ->
            Zipper t a -> t a
outOfFor to from = outOfFor' to from id id

Оснащенные этими инструментами, мы можем использовать Diff экземпляр для продуктов для реализации Diff (Zipper t)

-- This requires undecidable instances, due to the need to take D (D t)
instance (Diff t, Diff (D t)) => Diff (Zipper t) where
    type D (Zipper t) = D ((D t) :*: Identity)
    -- inTo :: t        a -> t        (Zipper  t         a)
    -- inTo :: Zipper t a -> Zipper t (Zipper (Zipper t) a)
    inTo = inToFor toZipper fromZipper
    -- outOf :: Zipper  t         a -> t        a
    -- outOf :: Zipper (Zipper t) a -> Zipper t a
    outOf = outOfFor toZipper fromZipper

Boilerplate

Чтобы фактически использовать код, представленный здесь, нам нужны некоторые языковые расширения, импорт и повторение предложенной проблемы.

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}

import Control.Monad.Identity
import Data.Proxy
import Control.Comonad

data Zipper t a = Zipper { diff :: D t a, here :: a }

onDiff :: (D t a -> D u a) -> Zipper t a -> Zipper u a
onDiff f (Zipper d a) = Zipper (f d) a

deriving instance Diff t => Functor (Zipper t)
deriving instance (Eq (D t a), Eq a) => Eq (Zipper t a)
deriving instance (Show (D t a), Show a) => Show (Zipper t a)

class (Functor t, Functor (D t)) => Diff t where
  type D t :: * -> *
  inTo  :: t a -> t (Zipper t a)
  outOf :: Zipper t a -> t a

Продукты, суммы и константы

Diff (Zipper t) Экземпляр опирается на реализации Diff за продуктами :*:, суммы :+:, константы Identityи ноль Proxy,

data (:+:) a b x = InL (a x) | InR (b x)
    deriving (Eq, Show)
data (:*:) a b x = a x :*: b x
    deriving (Eq, Show)

infixl 7 :*:
infixl 6 :+:

deriving instance (Functor a, Functor b) => Functor (a :*: b)

instance (Functor a, Functor b) => Functor (a :+: b) where
    fmap f (InL a) = InL . fmap f $ a
    fmap f (InR b) = InR . fmap f $ b


instance (Diff a, Diff b) => Diff (a :*: b) where
    type D (a :*: b) = D a :*: b :+: a :*: D b
    inTo (a :*: b) = 
        (fmap (onDiff (InL . (:*: b))) . inTo) a :*:
        (fmap (onDiff (InR . (a :*:))) . inTo) b
    outOf (Zipper (InL (a :*: b)) x) = (:*: b) . outOf . Zipper a $ x
    outOf (Zipper (InR (a :*: b)) x) = (a :*:) . outOf . Zipper b $ x

instance (Diff a, Diff b) => Diff (a :+: b) where
    type D (a :+: b) = D a :+: D b
    inTo (InL a) = InL . fmap (onDiff InL) . inTo $ a
    inTo (InR b) = InR . fmap (onDiff InR) . inTo $ b
    outOf (Zipper (InL a) x) = InL . outOf . Zipper a $ x
    outOf (Zipper (InR a) x) = InR . outOf . Zipper a $ x

instance Diff (Identity) where
    type D (Identity) = Proxy
    inTo = Identity . (Zipper Proxy) . runIdentity
    outOf = Identity . here

instance Diff (Proxy) where
    type D (Proxy) = Proxy
    inTo = const Proxy
    outOf = const Proxy

Пример бина

Я задал Bin Пример в виде изоморфизма к сумме произведений. Нам нужна не только его производная, но и его вторая производная

newtype Bin   a = Bin   {unBin   ::      (Bin :*: Identity :*: Bin :+: Identity)  a}
    deriving (Functor, Eq, Show)
newtype DBin  a = DBin  {unDBin  ::    D (Bin :*: Identity :*: Bin :+: Identity)  a}
    deriving (Functor, Eq, Show)
newtype DDBin a = DDBin {unDDBin :: D (D (Bin :*: Identity :*: Bin :+: Identity)) a}
    deriving (Functor, Eq, Show)

instance Diff Bin where
    type D Bin = DBin
    inTo  = inToFor'  Bin unBin DBin unDBin
    outOf = outOfFor' Bin unBin DBin unDBin

instance Diff DBin where
    type D DBin = DDBin
    inTo  = inToFor'  DBin unDBin DDBin unDDBin
    outOf = outOfFor' DBin unDBin DDBin unDDBin

Пример данных из предыдущего ответа

aTree :: Bin Int    
aTree =
    (Bin . InL) (
        (Bin . InL) (
            (Bin . InR) (Identity 2)
            :*: (Identity 1) :*:
            (Bin . InR) (Identity 3)
        )
        :*: (Identity 0) :*:
        (Bin . InR) (Identity 4)
    )

Не Comonad экземпляр

Bin Пример выше предоставляет контрпример к fmap outOf . inTo будучи правильной реализацией duplicate за Zipper t, В частности, это является контрпримером к fmap extract . duplicate = id закон:

fmap ( \z -> (fmap extract . duplicate) z == z) . inTo $ aTree

Который оценивает (обратите внимание, как он полон Falseвезде, любой False было бы достаточно, чтобы опровергнуть закон)

Bin {unBin = InL ((Bin {unBin = InL ((Bin {unBin = InR (Identity False)} :*: Identity False) :*: Bin {unBin = InR (Identity False)})} :*: Identity False) :*: Bin {unBin = InR (Identity False)})}

inTo aTree это дерево с той же структурой, что и aTree, но везде, где было значение, вместо этого есть застежка-молния со значением, а остальная часть дерева со всеми исходными значениями не повреждена. fmap (fmap extract . duplicate) . inTo $ aTree также дерево с той же структурой, что и aTree, но где бы ни было значение, вместо него есть застежка-молния со значением, а остаток дерева со всеми значениями заменяется тем же значением. Другими словами:

fmap extract . duplicate == \z -> fmap (const (here z)) z

Полный набор тестов для всех трех Comonad законы, extract . duplicate == id, fmap extract . duplicate == id, а также duplicate . duplicate == fmap duplicate . duplicate является

main = do
    putStrLn "fmap (\\z -> (extract . duplicate) z == z) . inTo $ aTree"
    print   . fmap ( \z -> (extract . duplicate) z == z) . inTo $ aTree    
    putStrLn ""
    putStrLn  "fmap (\\z -> (fmap extract . duplicate) z == z) . inTo $ aTree"
    print    . fmap ( \z -> (fmap extract . duplicate) z == z) . inTo $ aTree    
    putStrLn ""
    putStrLn "fmap (\\z -> (duplicate . duplicate) z) == (fmap duplicate . duplicate) z) . inTo $ aTree"
    print   . fmap ( \z -> (duplicate . duplicate) z == (fmap duplicate . duplicate) z) . inTo $ aTree

12

Источник

user414413 29 авг '14 в 06:34

Учитывая бесконечно дифференцируемый Diff учебный класс:

class (Functor t, Functor (D t)) => Diff t where
    type D t :: * -> *
    up :: Zipper t a -> t a
    down :: t a -> t (Zipper t a)  
    -- Require that types be infinitely differentiable
    ddiff :: p t -> Dict (Diff (D t))

around может быть написано с точки зрения up а также down на Zipper"s diffдериват, по сути как

around z@(Zipper d h) = Zipper ctx z
    where
        ctx = fmap (\z' -> Zipper (up z') (here z')) (down d)

Zipper t a состоит из D t a и a, Мы идем down D t a, получив D t (Zipper (D t) a) с молнией в каждой лунке. Эти молнии состоит из D (D t) a и a это было в дыре. Мы идем up каждый из них, получая D t a и сравнить его с a это было в дыре. D t a и a делать Zipper t a, давая нам D t (Zipper t a), который является контекстом, необходимым для Zipper t (Zipper t a),

Comonad Экземпляр тогда просто

instance Diff t => Comonad (Zipper t) where
    extract   = here
    duplicate = around

Захват производных Diff словарь требует некоторой дополнительной сантехники, которая может быть сделана с Data.Constraint или с точки зрения метода, представленного в связанном ответе

around :: Diff t => Zipper t a -> Zipper t (Zipper t a)
around z = Zipper (withDict d' (fmap (\z' -> Zipper (up z') (here z')) (down (diff z)))) z
    where
        d' = ddiff . p' $ z
        p' :: Zipper t x -> Proxy t
        p' = const Proxy

8

Источник

user414413 01 сен '14 в 07:47

Другие вопросы по тегам haskell deriving zipper comonad

user828361 29 авг '14 в 16:12 2014-08-29 16:12 · Accepted Answer · 2014-08-29 16:12

Подобно тому, как ловец детей в "Читти-Читти-Банг-Банг" заманивает детей в плен сладостями и игрушками, рекрутеры для бакалавров физики любят дурачиться с мыльными пузырями и бумерангами, но когда дверь лязгает, это "Хорошо, дети, время учиться" о частичной дифференциации! Я тоже. Не говори, что я тебя не предупреждал.

Вот еще одно предупреждение: следующий код должен {-# 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}

У этого функтора есть производная, которая также является функтором. Производная представляет собой контекст с одним отверстием для элемента. Тип молнии 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

Полиномиальные функторы дифференцируемы

Постоянные функторы дифференцируемы.

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 или же downF от, и мы легко не можем найти ни один из способов пойти downF,

Функтор идентичности дифференцируем.

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 можно только оставаться на месте.

Сумма сохраняет дифференцируемость.

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))

Идти 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,

Продукт сохраняет дифференцируемость.

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)

Сейчас, downF работает аналогично тому, как это было для сумм, за исключением того, что мы должны исправить контекст молнии не только с помощью тега (чтобы показать, каким путем мы пошли), но также и с нетронутым другим компонентом.

  downF (f :*: g)
    =    fmap (\ (f' :<-: x) -> LF (f' :*: g) :<-: x) (downF f)
    :*:  fmap (\ (g' :<-: x) -> RF (f :*: g') :<-: x) (downF g)

Но aroundF это массивная сумка смеха. Какую бы сторону мы в настоящее время не посетили, у нас есть два варианта:

Переехать aroundF на той стороне.
Переехать 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))

Упражнение. Покажите, что композиция дифференцируемых функторов дифференцируема с использованием правила цепочки.

Милая! Можем ли мы пойти домой сейчас? Конечно, нет. Мы еще не дифференцировали никаких рекурсивных структур.

Создание рекурсивных функторов из бифункторов

Bifunctor Как объясняет существующая литература по универсальному программированию типов данных (см. работу Патрика Янссона и Йохана Йеринга или отличные конспекты лекций Джереми Гиббонс), это конструктор типов с двумя параметрами, соответствующими двум типам подструктуры. Мы должны быть в состоянии "отобразить" оба.

class Bifunctor b where
  bimap :: (x -> x') -> (y -> y') -> b x y -> b x' y'

Мы можем использовать Bifunctor s, чтобы дать структуру узла рекурсивных контейнеров. Каждый узел имеет подузлы и элементы. Это могут быть только два вида субструктуры.

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 экземпляров.

Bifunctor Kit

Константы бифункциональны.

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 а также 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)

Суммы и произведения бифункторов являются бифункторами

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 дифференцируемо в обеих переменных. Clang! Пришло время узнать о частичной дифференциации.

Частичные производные бифункторов

Поскольку у нас есть две переменные, мы должны иметь возможность говорить о них коллективно, иногда и индивидуально, в другое время. Нам понадобится семья-одиночка:

data Vary :: Var -> * where
  VX :: Vary X
  VY :: Vary Y

Теперь мы можем сказать, что для бифунктора означает иметь частные производные по каждой переменной, и дать соответствующее понятие молнии.

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}

это D Операция должна знать, на какую переменную нацеливаться. Соответствующая молния Z b v говорит нам, какая переменная v должен быть в фокусе. Когда мы "украшаем контекстом", мы должны украшать x -элементы с X -контексты и y -элементы с Y -contexts. Но в остальном это та же история.

У нас есть две оставшиеся задачи: во-первых, показать, что наш бифункторный набор дифференцируем; во-вторых, чтобы показать, что 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

В этом случае жизнь слишком коротка, чтобы развить теорию уровня типа Kronecker-delta, поэтому я просто рассматривал переменные отдельно.

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 а также 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)

Концептуально это так же, как и раньше, но с большей бюрократией. Я построил их, используя технологию pre-type-hole, используя 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))})

Но нам нужны элемент- молнии.

Элемент-молния для фиксированных точек бифункторов

Каждый элемент находится где-то внутри узла. Этот узел сидит под стопкой 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))

Сейчас, down b только забирает нас внутрь узла. Молнии, которые нам нужны, также должны нести контекст узла. Это то что contextualise делает:

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 -положение, мы должны дать элемент-молнию, так что хорошо, что мы знаем весь контекст dXs вернуться к корню, а также dY который описывает, как элемент находится в своем узле. Для каждого X -позиция, есть еще одно поддерево для исследования, поэтому мы наращиваем стек и продолжаем!

Это оставляет только бизнес смещения фокуса. Мы можем остаться на месте, или спуститься с того места, где мы находимся, или подняться, или подняться, а затем пойти по другому пути. Вот оно.

  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 различные виды элементов. Они закрыты под якобианской конструкцией

J f :: (i -> *) -> ((o, i) -> *)

где каждый из полученных (o, i) -структуры является частной производной, говорящей вам, как сделать i -элемент-отверстие в o -состав. Но это зависит от веселья, в другой раз.