我正在制作一个玩具,您可以在其中在网格上绘制电路,我们可以模拟它们的行为。我认为抽象电路板的维度并尝试使代码在任何电路板维度(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 和单例库就可以了:)
感谢您花时间阅读我的困境!
最佳答案
使用 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)]
关于haskell - 对类型维度的抽象,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/46133182/