Возможно ли отменить выровненные по типу обходы?

Здесь много настроек. Если вы когда-либо видели последовательность, выровненную по типу, вы можете просмотреть все до строки.

Выровненная по типу последовательность - это все, что выглядит нечетко как

data ConsList c x y where
  CNil :: ConsList c x x     
  Cons :: c x y -> ConsList c y z -> ConsList c x z

Учитывая класс для индексированных функторов с индексом Akey и аппликативных функторов

class IxFunctor f where
  ixmap :: (a -> b) -> f x y a -> f x y b
class IxFunctor f => IxApply f where
  ixap :: f i j (a -> b) -> f j k a -> f i k b
class IxApply f => IxApplicative f where
  ixpure :: a -> f i i a

и двухзначный класс функторов в стиле Макбрайда:

type (f :: q -> r -> *) ~~> (g :: q -> r -> *) =
  forall (i :: q) (j :: r) . f i j -> g i j

class TFunctor t where
  tmap :: (c ~~> d) -> (t c ~~> t d)

можно описать карты, складки и обходы, которые будут работать для последовательностей, выровненных по строкам:

class TFoldable t where
  tfoldMap :: Category d => (c ~~> d) -> t c ~~> d
  tfoldMap f = tfoldr (\cij djk -> f cij >>> djk) id

class (TFunctor t, TFoldable t) => TTraversable t where
  ttraverse :: IxApplicative f
            => (forall x y . c x y -> f x y (d x y))
            -> (t c p q -> f p q (t d p q))

Теперь выясняется, что можно определить версию Data.Functor.Reverse для последовательностей с выравниванием по типу. Конкретно

newtype Reverse t c x y = Reverse {unReverse :: t (Dual c) y x}

где

newtype Dual c x y = Dual {getDual :: c y x}

Когда тип t является фактически последовательностью, выровненной по типу, просто дать Reverse t полный набор операций последовательности с выравниванием по типу.

Фактический вопрос

Что мне не ясно, является ли t IxTraversable достаточным для реализации IxTraversable (Reverse t). Все, что я пробовал, поражает кирпичную стену. Для стандартных Traversable s это можно сделать, используя аппликацию Backwards. Доступен IxBackwards, но он, похоже, не помогает. Для стандартного Traversable s можно сбросить содержимое контейнера в список, а затем вернуться из списка. Но это не представляется возможным здесь, потому что нет очевидного способа записи типов на выходе и обеспечения того, что они будут совпадать по пути. Я что-то пропустил или это не-go?

Самый простой старт:

instance IxTraversable t => IxTraversable (Reverse t) where
  ttraverse f (Reverse xs) = Reverse `ixmap` _ xs

Это дает мне отверстие типа

t (Dual c) q p -> f p q (t (Dual d) q p)

Очевидная задача состоит в том, что мы имеем t _ q p, но f p q _. Поэтому, если есть способ сделать это, нам, по-видимому, нужно как-то придумать f, который будет переворачивать вещи. Как я уже говорил, там IxBackwards

newtype IxBackwards f y x a = IxBackwards { ixforwards :: f x y a }

но я не вижу, как это помогает.

Ответы

Ответ 1

Ваша установка звучит, и IxBackwards полезен (на самом деле, критический) - проблема, с которой вы столкнулись, заключается в том, что обе Dual и Reverse заменяют позиции переменных типа, тогда как первый аргумент ttraverse требует, чтобы позиции квантифицированных переменных типа (x,y) в некотором смысле "соглашались". Вы должны одновременно "перевернуть" эти переменные в рекурсивном вызове на ttraverse, используя как Dual, так и IxBackwards:

instance TTraversable t => TTraversable (Reverse t) where

  ttraverse f = 
    ixmap Reverse . ixforwards . 
    ttraverse (IxBackwards . ixmap Dual . f . getDual) . 
    unReverse

Запись экземпляров для TFunctor и TFoldable может дать нам подсказку о том, как найти эту реализацию:

dualNat2 :: (c ~~> d) -> Dual c ~~> Dual d 
dualNat2 k (Dual x) = Dual $ k x 

instance TFunctor f => TFunctor (Reverse f) where 
  tmap f (Reverse q) = Reverse $ tmap (dualNat2 f) q 

instance TFoldable f => TFoldable (Reverse f) where 
  tfoldMap k (Reverse z) = getDual $ tfoldMap (dualNat2 k) z

Вы по существу делаете то же самое в случае TTraversable, за исключением того, что теперь есть два индекса для перевода:

f                                      :: forall x y . c x y -> f x y (d x y)   
ixmap Dual . f . getDual               :: forall x y . Dual c y x -> f x y (Dual d y x)
IxBackwards . f                        :: forall x y . c x y -> IxBackwards f y x (d x y)
IxBackwards . ixmap Dual . f . getDual :: forall x y . Dual c y x -> IxBackwards f y x (Dual d y x)

и обратите внимание, что если вы только переверните один из индексов, тип функции даже не соответствует типу аргумента ttraverse.

Я попытаюсь дать пошаговый вывод с помощью Типированных отверстий.

Начните с этого скелета, который я считаю тривиальным для вывода:

  ttraverse f = 
    ixmap Reverse .  
    ttraverse _trfun . 
    unReverse

Это дает ошибку типа:

Couldn't match type `q' with `p'
...
Expected type: Reverse t c p q -> f p q (Reverse t d p q)
Actual type: Reverse t c q p -> f p q (Reverse t d q p)
* In the expression: ixmap Reverse . ttraverse _trfun . unReverse

Итак, добавьте больше отверстий, пока они не скомпилируются. Мой первый инстинкт - добавить еще одну дыру в фронт (так как ошибка типа для всего выражения, что-то нужно сделать для всего выражения, чтобы сделать его typecheck):

  ttraverse f = 
    _out . ixmap Reverse .  
    ttraverse _trfun . 
    unReverse

Теперь мы не получаем ошибок типа (игнорируя ошибки "неоднозначного типа" формы C x, где C - класс, - ошибочны), а тип, о котором сообщается,

 _out :: f0 q p (Reverse t c0 p q) -> f p q (Reverse t d p q)

где f0, c0 (в настоящее время) свободные переменные типа, которые мы используем в наших интересах! Если мы дадим c0 ~ d и f0 ~ IxBackwards f, то это как раз тип ixforwards - так что попробуйте:

  ttraverse f = 
    ixforwards . ixmap Reverse .  
    ttraverse _trfun . 
    unReverse

и теперь мы получаем хороший мономорфный предполагаемый тип:

 _trfun :: Dual c x y -> IxBackwards f x y (Dual d x y)
 * Relevant bindings include
     f :: forall (x :: r) (y :: r). c x y -> f x y (d x y)

Теперь я также предполагаю, что очевидно, что _trfun должно каким-то образом использовать f, поэтому попробуйте это. Мы замечаем, что как область, так и область f не являются точно такими, как _trfun, поэтому мы размещаем отверстие с обеих сторон:

  ttraverse f = 
    ixforwards . ixmap Reverse .  
    ttraverse (_out . f . _in) . 
    unReverse

и получим:

_out :: f x0 y0 (d x0 y0) -> IxBackwards f x y (Dual d x y)
_in :: Dual c x y -> c x0 y0

где x0, y0 - свободные переменные. Вероятно, наиболее очевидно, что с x0 ~ y, y0 ~ x мы имеем _in = getDual, поэтому мы пытаемся это сделать и получаем новый вывод:

_out :: f y x (d y x) -> IxBackwards f x y (Dual d x y)

и теперь очевидно, что переменные типа "перевернуты" в двух разных местах; один раз IxBackwards и один раз Dual. Способ перевернуть первую пару индексов наиболее очевидно (возможно):

  ttraverse f = 
    ixforwards . ixmap Reverse .  
    ttraverse (_out . IxBackwards . f . getDual) . 
    unReverse

и получим:

_out :: IxBackwards f x y (d y x) -> IxBackwards f x y (Dual d x y)

Теперь у нас есть что-то вроде q A -> q B с IxFunctor q, поэтому, устанавливая _out = ixmap _out, получаем

_out :: d y x -> Dual d x y

и существует тривиальная функция этого типа - а именно Dual - которая завершает определение:

  ttraverse f = 
    ixforwards . ixmap Reverse .  
    ttraverse (ixmap Dual . IxBackwards . f . getDual) . 
    unReverse

Обратите внимание, что некоторые композиции функций перевернуты по сравнению с исходной версией - я притворялся, что не знаю ответа априори и вывел его "самым очевидным" способом, заполнив самые простые вещи. Два определения эквивалентны (поистине эквивалентны, так как Dual и IxBackwards являются как раз newtype s).