是否可以反转类型对齐的遍历？

Question

这里有很多设置.如果你以前见过类型对齐的序列,你可以浏览所有内容.

类型对齐的序列是任何看起来模糊的东西

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

给出了Atkey风格的索引函子和应用函子的类

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

和一个双索引McBride风格的仿函数类:

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).我尝试过的所有东西都撞到了一堵砖墙.对于标准Traversables,可以使用Backwards应用程序来完成.有一个IxBackwards可用,但它似乎没有帮助.对于标准Traversables,可以将容器内容转储到列表中,然后从列表中退回.但这似乎不可能在这里,因为没有明显的方法来记录出路上的类型,并确保它们在路上匹配.我错过了什么,或者这是不是？

最开始的:

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 }

但我不明白这有多大帮助.

Answer 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.

我将尝试使用Typed Holes逐步推导出来.

从这个骨架开始,我认为这很简单:

  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

所以添加更多的洞直到它编译.我的第一直觉是在前面添加另一个洞(因为类型错误是针对整个表达式的,所以必须对整个表达式做一些事情以使其成为类型检查):

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