Abstracting over Dimensionality of Types

Question

I'm building a toy where you can draw circuits on a grid and we can simulate their behaviour. I thought it would be a fun experiment to abstract over the dimensionality of the board and try to make the code work (in a type-safe way) over any board dimensions (2D, 3D, 4D, etc).

I can do most of the work with GADTs and Nats; Assuming I'm using a vector as a 2D base abstraction we can represent any dimensionality by composing it;

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

This works for the most part (unfortunately the type family requires UndecidableInstances)

With this I can express that operations over grids stay consistent in dimensionality, i.e.

alter :: Grid n a -> Grid n b

The tricky bit is that I want to also allow moving around in the grids. I've written a Representable instance for Grid which relies on the underlying Representable for Compose, basically you just pair up the representation for each functor being composed. In my case here are some example representations:

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

And so on.

Also assume that we can index into a Grid by keeping an index alongside it as a store comonad type IGrid n a = (Rep (Grid n), Grid n a)

I've written a few functions which move around in a certain dimensionality. Conceptually if a function moves the focus on the y-axis, we can still call that function on any dimensionality with at least 2 dimensions:

e.g.

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

This is doable and easy when n==2, but for higher dimensions it's probably easiest to implement by promoting a lower dimensionality index into some higher one (padding unknown dimensional coords with mempty) so that I can use seek :: Rep (Grid n) -> Grid n a -> Grid n a properly.

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

Then I can just promote a given index to any dim before using it:

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

Most of my attempts have centered around using a typeclass and implementing it over certain Nats and using lots of type assertions. I've been able to promote an index by one or two finite levels, but can't figure out the general case.

I've been trying to write this promote function for a month or two now, coming back to it from time to time and it seems possible but I just can't figure it out. Any help would be greatly appreciated. Using Nats and the singletons lib is fine if that's the way to do it :)

Thanks for taking the time to read my dilemma!

Answer 1

Measuring the size of your type expression with a Nat, and then trying to inject the index for a small grid into the index for a big one, is overkill here. All you really need to do is identify how deep into the nested Compose type you want to go before you modify the grid.

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

Under g f is shaped like a natural number - compare Under (Under Over) with S (S Z) - and it tells you how many layers of Compose you have to unpeel from f in order to find a 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

You mentioned in a comment that you're working with grids of infinite zippers. It's easier to use Under with nested Composes where the Zipper is always the left argument. My Grid2 is isomorphic to your 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

Now, given move :: Int -> Zipper a -> Zipper a, you can go Under any number of Compose constructors to move a particular dimension of your grid.

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

For example, to go up in a 2D grid, you move all the inner zippers left.

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

Now if you want to move a variety of dimensions of your grid at once you can just call moveUnder multiple times. Here I'm putting a sequence of Moves in a list. Note that I'm existentially quantifying the g in Move's constructor.

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