对类型的维度进行抽象

Question

我正在制作一个玩具，您可以在其中在网格上绘制电路，我们可以模拟它们的行为。我认为抽象板的维度并尝试使代码在任何板尺寸（2D、3D、4D 等）上工作（以类型安全的方式）将是一个有趣的实验。

我可以使用 GADT 和 Nats 完成大部分工作；假设我使用向量作为 2D 基础抽象，我们可以通过组合它来表示任何维度；

type family Count t where
  Count (Compose _ g) = 1 + (Count g)
  Count _ = 0

data Grid (n::Nat) a where
  Grid :: f a -> Grid (Count f) a

这在大多数情况下都有效（不幸的是，类型族需要 UndecidableInstances）

这样我可以表达网格上的操作在维度上保持一致，即

alter :: Grid n a -> Grid n b

棘手的一点是我还想允许在网格中移动。 我已经为 Grid 编写了一个 Representable 实例，它依赖于 Compose 的底层 Representable，基本上你只需为每个组成的仿函数配对表示。就我而言，这里有一些示例表示：

Rep (Grid 2) ~ (Sum Int, Sum Int)
Rep (Grid 3) ~ (Sum Int, (Sum Int, Sum Int))
Rep (Grid 3) ~ (Sum Int, (Sum Int, (Sum Int, Sum Int)))

等等。

还假设我们可以通过在网格旁边保留一个索引作为存储comonad type IGrid n a = (Rep (Grid n), Grid n a)来索引到一个网格中

我编写了一些在特定维度上移动的函数。从概念上讲，如果一个函数将焦点移到 y 轴上，我们仍然可以在至少有 2 个维度的任何维度上调用该函数：

例如

moveUp :: (n >= 2) => IGrid n a -> IGrid n a

这在 n==2 时是可行且容易的，但对于更高维度，通过将较低维度索引提升为更高维度索引（用 mempty 填充未知维度坐标）可能最容易实现，这样我就可以正确使用 seek :: Rep (Grid n) -> Grid n a -> Grid n a .

promote :: (m <= n) => Rep (Grid m) -> Rep (Grid n)

然后我可以在使用之前将给定的索引提升为任何暗淡：

moveBy :: Rep (Grid n) -> IGrid n a -> IGrid n a
moveBy m (rep, grid) = (rep <> m, grid)

moveAround :: IGrid n a -> IGrid n a
moveAround grid = grid
                & moveBy (promote (Sum 3, Sum 2)) 
                & moveBy (promote (Sum 1))

我的大部分尝试都集中在使用类型类并在某些 Nat 上实现它并使用大量类型断言。我有 能够将索引提升一到两个有限级别，但无法弄清楚一般情况。

我已经尝试编写这个promote 函数一两个月了，时不时回到它，这似乎是可能的，但我就是想不通。任何帮助将不胜感激。如果这样做的话，使用 Nats 和单例库就可以了 :)

感谢您花时间阅读我的困境！

Answer 1

使用Nat 测量类型表达式的大小，然后尝试将小网格的索引注入到大网格的索引中，这在此处是多余的。您真正需要做的就是在修改网格之前确定您想要深入嵌套的Compose 类型。

data Under g f where
    Over :: Under f f
    Under :: Functor h => Under g f -> Under g (Compose h f)

Under g f 的形状像一个自然数 - 将 Under (Under Over) 与 S (S Z) 进行比较 - 它会告诉您必须从 f 剥离多少层 Compose 才能找到 g。

under :: Under g f -> (g a -> g a) -> f a -> f a
under Over f = f
under (Under u) f = Compose . fmap (under u f) . getCompose

您在评论中提到您正在使用无限拉链网格。将Under 与嵌套的Composes 一起使用更容易，其中Zipper 始终是左侧参数。我的Grid2 与您的Compose Zipper Zipper 同构。

type Zipped = Compose Zipper
type Grid1 = Zipped Identity
type Grid2 = Zipped Grid1

zipped :: (Zipper (f a) -> Zipper (g b)) -> Zipped f a -> Zipped g b
zipped f = Compose . f . getCompose

现在，给定move :: Int -> Zipper a -> Zipper a，您可以将Under 任意数量的Compose 构造函数转换为move 网格的特定维度。

moveUnder :: Under (Zipped g) f -> Int -> f a -> f a
moveUnder u n = under u (zipped $ move n)

例如，要在 2D 网格中移动 up，请将所有内部拉链向左移动。

-- up :: Grid2 a -> Grid2 a
up :: Functor f => Compose f (Zipped g) a -> Compose f (Zipped g) a
up = moveUnder (Under Over) (-1)

现在，如果您想一次移动网格的多个维度，只需多次调用 moveUnder。在这里，我将一系列Moves 放入列表中。请注意，我在Move 的构造函数中量化了g。

data Move f where
    Move :: Under (Zipped g) f -> Int -> Move f

movesZipped :: [Move f] -> f a -> f a
movesZipped ms z = foldr (\(Move u n) -> moveUnder u n) z ms

rightTwoUpOne = movesZipped [Move Over 2, Move (Under Over) (-1)]