Using the typical definition of type-level naturals, I've defined an n-dimensional grid.
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
data Nat = Z | S Nat
data U (n :: Nat) x where
Point :: x -> U Z x
Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x
dmap :: (U n x -> U m r) -> U (S n) x -> U (S m) r
dmap f (Dimension ls mid rs) = Dimension (map f ls) (f mid) (map f rs)
instance Functor (U n) where
fmap f (Point x) = Point (f x)
fmap f d@Dimension{} = dmap (fmap f) d
Now I want to make it an instance of Comonad, but I can't quite wrap my brain around it.
class Functor w => Comonad w where
(=>>) :: w a -> (w a -> b) -> w b
coreturn :: w a -> a
cojoin :: w a -> w (w a)
x =>> f = fmap f (cojoin x)
cojoin xx = xx =>> id
instance Comonad (U n) where
coreturn (Point x) = x
coreturn (Dimension _ mid _) = coreturn mid
-- cojoin :: U Z x -> U Z (U Z x)
cojoin (Point x) = Point (Point x)
-- cojoin ::U (S n) x -> U (S n) (U (S n) x)
cojoin d@Dimension{} = undefined
-- =>> :: U Z x -> (U Z x -> r) -> U Z r
p@Point{} =>> f = Point (f p)
-- =>> :: U (S n) x -> (U (S n) x -> r) -> U (S n) r
d@Dimension{} =>> f = undefined
Using cojoin
on an n-dimensional grid will produce an n-dimensional grid of n-dimensional grids. I'd like to provide an instance with the same idea as this one, which is that the value of the cojoined grid at (x,y,z) should be the original grid focused on (x,y,z). To adapt that code, it appears that we need to reify n
in order to perform n
"fmaps" and n
"rolls". You don't have to do it that way but if that helps, then there you go.
Jagger/Richards: you can't always get what you want, but if you try sometime you just might find that you get what you need.
Cursors in Lists
Let me rebuild the components of your structure using snoc- and cons-lists to keep the spatial properties clear. I define
Let's have comonads
and let's make sure cursors are comonads
If you're turned on to this kind of stuff, you'll note that
Cursor
is a spatially pleasing variant ofInContext []
where ∂ takes the formal derivative of a functor, giving its notion of one-hole context.
InContext f
is always aComonad
, as mentioned in this answer, and what we have here is just thatComonad
induced by the differential structure, wherecounit
extracts the element at the focus andcojoin
decorates each element with its own context, effectively giving you a context full of refocused cursors and with an unmoved cursor at its focus. Let's have an example.See? The 2 in focus has been decorated to become the cursor-at-2; to the left, we have the list of the cursor-at-1; to the right, the list of the cursor-at-3 and the cursor-at-4.
Composing Cursors, Transposing Cursors?
Now, the structure you're asking to be a
Comonad
is the n-fold composition ofCursor
. Let's haveTo persuade comonads
f
andg
to compose, thecounit
s compose neatly, but you need a "distributive law"so you can make the composite
cojoin
like thisWhat laws should
transpose
satisfy? Probably something likeor whatever it takes to ensure that any two ways to shoogle some sequence of f's and g's from one order to another give the same result.
Can we define a
transpose
forCursor
with itself? One way to get some sort of transposition cheaply is to note thatBwd
andFwd
are zippily applicative, hence so isCursor
.And here you should begin to smell the rat. Shape mismatch results in truncation, and that's going to break the obviously desirable property that self-transpose is self-inverse. Any kind of raggedness will not survive. We do get a transposition operator:
sequenceA
, and for completely regular data, all is bright and beautiful.But even if I just move one of the inner cursors out of alignment (never mind making the sizes ragged), things go awry.
When you have one outer cursor position and multiple inner cursor positions, there's no transposition which is going to behave well. Self-composing
Cursor
allows the inner structures to be ragged relative to one another, so notranspose
, nocojoin
. You can, and I did, definebut it's an onus on us to make sure we keep the inner structures regular. If you're willing to accept that burden, then you can iterate, because
Applicative
andTraversable
are readily closed under composition. Here are the bits and piecesEdit: for completeness, here's what it does when all is regular,
Hancock's Tensor Product
For regularity, you need something stronger than composition. You need to be able to capture the notion of "an f-structure of g-structures-all-the-same-shape". This is what the inestimable Peter Hancock calls the "tensor product", which I'll write
f :><: g
: there's one "outer" f-shape and one "inner" g-shape common to all the inner g-structures, so transposition is readily definable and always self-inverse. Hancock's tensor is not conveniently definable in Haskell, but in a dependently typed setting, it's easy to formulate a notion of "container" which has this tensor.To give you the idea, consider a degenerate notion of container
where we say
s
is the type of "shapes" andp
the type of "positions". A value consists of the choice of a shape and the storage of anx
in each position. In the dependent case, the type of positions may depend on the choice of the shape (e.g., for lists, the shape is a number (the length), and you have that many positions). These containers have a tensor productwhich is like a generalised matrix: a pair of shapes give the dimensions, and then you have an element at each pair of positions. You can do this perfectly well when types
p
andp'
depend on values ins
ands'
, and that is exactly Hancock's definition of the tensor product of containers.InContext for Tensor Products
Now, as you may have learned in high school,
∂(s :<| p) = (s, p) :<| (p-1)
wherep-1
is some type with one fewer element thanp
. Like ∂(sx^p) = (sp)*x^(p-1). You select one position (recording it in the shape) and delete it. The snag is thatp-1
is tricky to get your hands on without dependent types. ButInContext
selects a position without deleting it.This works just as well for the dependent case, and we joyously acquire
Now we know that
InContext f
is always aComonad
, and this tells us that tensor products ofInContext
s are comonadic because they are themselvesInContext
s. That's to say, you pick one position per dimension (and that gives you exactly one position in the whole thing), where before we had one outer position and lots of inner positions. With the tensor product replacing composition, everything works sweetly.Naperian Functors
But there is a subclass of
Functor
for which the tensor product and the composition coincide. These are theFunctor
sf
for whichf () ~ ()
: i.e., there is only one shape anyway, so raggedy values in compositions are ruled out in the first place. TheseFunctor
s are all isomorphic to(p ->)
for some position setp
which we can think of as the logarithm (the exponent to whichx
must be raised to givef x
). Correspondingly, Hancock calls theseNaperian
functors after John Napier (whose ghost haunts the part of Edinburgh where Hancock lives).A
Naperian
functor has a logarithm, inducing aproject
ion function mapping positions to the elements found there.Naperian
functors are all zippilyApplicative
, withpure
and<*>
corresponding to the K and S combinators for the projections. It's also possible to construct a value where at each position is stored that very position's representation. Laws of logarithms which you might remember pop up pleasingly.Note that a fixed size array (a vector) is given by
(Id :*: Id :*: ... :*: Id :*: One)
, whereOne
is the constant unit functor, whose logarithm isVoid
. So an array isNaperian
. Now, we also havewhich means that multi-dimensional arrays are
Naperian
.To construct a version of
InContext f
forNaperian f
, just point to a position!So, in particular, a
Focused
n-dimensional array will indeed be a comonad. A composition of vectors is a tensor product of n vectors, because vectors areNaperian
. But theFocused
n-dimensional array will be the n-fold tensor product, not the composition, of the nFocused
vectors which determine its dimensions. To express this comonad in terms of zippers, we'll need to express them in a form which makes it possible to construct the tensor product. I'll leave that as an exercise for the future.