haskell - 对类型维度的抽象

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

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

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

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

Answer 1

使用 Nat 测量类型表达式的大小，然后尝试将小网格的索引注入(inject)大网格的索引，在这里是过度的。您真正需要做的就是在修改网格之前确定您想要进入嵌套 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

您在评论中提到您正在使用无限 zipper 网格。将 Under 与嵌套 Compose 一起使用会更容易，其中 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 构造函数移动网格的特定维度。

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

例如，要在 2D 网格中向上，您需要向左移动所有内部 zipper 。

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

现在，如果您想一次移动网格的多个维度，只需多次调用 moveUnder 即可。在这里，我将一系列 Move 放入列表中。请注意，我正在对 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)]