Databases
StackOverflow2013
Postsdbo
PO
Body
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    text
    copied!<p><strong>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.</strong></p> <h2>Cursors in Lists</h2> <p>Let me rebuild the components of your structure using snoc- and cons-lists to keep the spatial properties clear. I define</p> <pre><code>data Bwd x = B0 | Bwd x :&lt; x deriving (Functor, Foldable, Traversable, Show) data Fwd x = F0 | x :&gt; Fwd x deriving (Functor, Foldable, Traversable, Show) infixl 5 :&lt; infixr 5 :&gt; data Cursor x = Cur (Bwd x) x (Fwd x) deriving (Functor, Foldable, Traversable, Show) </code></pre> <p>Let's have comonads</p> <pre><code>class Functor f =&gt; Comonad f where counit :: f x -&gt; x cojoin :: f x -&gt; f (f x) </code></pre> <p>and let's make sure cursors are comonads</p> <pre><code>instance Comonad Cursor where counit (Cur _ x _) = x cojoin c = Cur (lefts c) c (rights c) where lefts (Cur B0 _ _) = B0 lefts (Cur (xz :&lt; x) y ys) = lefts c :&lt; c where c = Cur xz x (y :&gt; ys) rights (Cur _ _ F0) = F0 rights (Cur xz x (y :&gt; ys)) = c :&gt; rights c where c = Cur (xz :&lt; x) y ys </code></pre> <p>If you're turned on to this kind of stuff, you'll note that <code>Cursor</code> is a spatially pleasing variant of <code>InContext []</code></p> <pre><code>InContext f x = (x, ∂f x) </code></pre> <p>where ∂ takes the formal derivative of a functor, giving its notion of one-hole context. <code>InContext f</code> is always a <code>Comonad</code>, as mentioned in <a href="https://stackoverflow.com/a/12872133/828361">this answer</a>, and what we have here is just that <code>Comonad</code> induced by the differential structure, where <code>counit</code> extracts the element at the focus and <code>cojoin</code> 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.</p> <pre><code>&gt; cojoin (Cur (B0 :&lt; 1) 2 (3 :&gt; 4 :&gt; F0)) Cur (B0 :&lt; Cur B0 1 (2 :&gt; 3 :&gt; 4 :&gt; F0)) (Cur (B0 :&lt; 1) 2 (3 :&gt; 4 :&gt; F0)) ( Cur (B0 :&lt; 1 :&lt; 2) 3 (4 :&gt; F0) :&gt; Cur (B0 :&lt; 1 :&lt; 2 :&lt; 3) 4 F0 :&gt; F0) </code></pre> <p>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.</p> <h2>Composing Cursors, Transposing Cursors?</h2> <p>Now, the structure you're asking to be a <code>Comonad</code> is the n-fold composition of <code>Cursor</code>. Let's have</p> <pre><code>newtype (:.:) f g x = C {unC :: f (g x)} deriving Show </code></pre> <p>To persuade comonads <code>f</code> and <code>g</code> to compose, the <code>counit</code>s compose neatly, but you need a "distributive law"</p> <pre><code>transpose :: f (g x) -&gt; g (f x) </code></pre> <p>so you can make the composite <code>cojoin</code> like this</p> <pre><code>f (g x) -(fmap cojoin)-&gt; f (g (g x)) -cojoin-&gt; f (f (g (g x))) -(fmap transpose)-&gt; f (g (f (g x))) </code></pre> <p>What laws should <code>transpose</code> satisfy? Probably something like</p> <pre><code>counit . transpose = fmap counit cojoin . transpose = fmap transpose . transpose . fmap cojoin </code></pre> <p>or 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.</p> <p>Can we define a <code>transpose</code> for <code>Cursor</code> with itself? One way to get some sort of transposition cheaply is to note that <code>Bwd</code> and <code>Fwd</code> are <em>zippily</em> applicative, hence so is <code>Cursor</code>.</p> <pre><code>instance Applicative Bwd where pure x = pure x :&lt; x (fz :&lt; f) &lt;*&gt; (sz :&lt; s) = (fz &lt;*&gt; sz) :&lt; f s _ &lt;*&gt; _ = B0 instance Applicative Fwd where pure x = x :&gt; pure x (f :&gt; fs) &lt;*&gt; (s :&gt; ss) = f s :&gt; (fs &lt;*&gt; ss) _ &lt;*&gt; _ = F0 instance Applicative Cursor where pure x = Cur (pure x) x (pure x) Cur fz f fs &lt;*&gt; Cur sz s ss = Cur (fz &lt;*&gt; sz) (f s) (fs &lt;*&gt; ss) </code></pre> <p>And here you should begin to smell the rat. Shape mismatch results in <em>truncation</em>, 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: <code>sequenceA</code>, and for completely regular data, all is bright and beautiful.</p> <pre><code>&gt; regularMatrixCursor Cur (B0 :&lt; Cur (B0 :&lt; 1) 2 (3 :&gt; F0)) (Cur (B0 :&lt; 4) 5 (6 :&gt; F0)) (Cur (B0 :&lt; 7) 8 (9 :&gt; F0) :&gt; F0) &gt; sequenceA regularMatrixCursor Cur (B0 :&lt; Cur (B0 :&lt; 1) 4 (7 :&gt; F0)) (Cur (B0 :&lt; 2) 5 (8 :&gt; F0)) (Cur (B0 :&lt; 3) 6 (9 :&gt; F0) :&gt; F0) </code></pre> <p>But even if I just move one of the inner cursors out of alignment (never mind making the sizes ragged), things go awry.</p> <pre><code>&gt; raggedyMatrixCursor Cur (B0 :&lt; Cur ((B0 :&lt; 1) :&lt; 2) 3 F0) (Cur (B0 :&lt; 4) 5 (6 :&gt; F0)) (Cur (B0 :&lt; 7) 8 (9 :&gt; F0) :&gt; F0) &gt; sequenceA raggedyMatrixCursor Cur (B0 :&lt; Cur (B0 :&lt; 2) 4 (7 :&gt; F0)) (Cur (B0 :&lt; 3) 5 (8 :&gt; F0)) F0 </code></pre> <p>When you have one outer cursor position and multiple inner cursor positions, there's no transposition which is going to behave well. Self-composing <code>Cursor</code> allows the inner structures to be ragged relative to one another, so no <code>transpose</code>, no <code>cojoin</code>. You can, and I did, define</p> <pre><code>instance (Comonad f, Traversable f, Comonad g, Applicative g) =&gt; Comonad (f :.: g) where counit = counit . counit . unC cojoin = C . fmap (fmap C . sequenceA) . cojoin . fmap cojoin . unC </code></pre> <p>but 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 <code>Applicative</code> and <code>Traversable</code> are readily closed under composition. Here are the bits and pieces</p> <pre><code>instance (Functor f, Functor g) =&gt; Functor (f :.: g) where fmap h (C fgx) = C (fmap (fmap h) fgx) instance (Applicative f, Applicative g) =&gt; Applicative (f :.: g) where pure = C . pure . pure C f &lt;*&gt; C s = C (pure (&lt;*&gt;) &lt;*&gt; f &lt;*&gt; s) instance (Functor f, Foldable f, Foldable g) =&gt; Foldable (f :.: g) where fold = fold . fmap fold . unC instance (Traversable f, Traversable g) =&gt; Traversable (f :.: g) where traverse h (C fgx) = C &lt;$&gt; traverse (traverse h) fgx </code></pre> <p><strong>Edit:</strong> for completeness, here's what it does when all is regular,</p> <pre><code>&gt; cojoin (C regularMatrixCursor) C {unC = Cur (B0 :&lt; Cur (B0 :&lt; C {unC = Cur B0 (Cur B0 1 (2 :&gt; (3 :&gt; F0))) (Cur B0 4 (5 :&gt; (6 :&gt; F0)) :&gt; (Cur B0 7 (8 :&gt; (9 :&gt; F0)) :&gt; F0))}) (C {unC = Cur B0 (Cur (B0 :&lt; 1) 2 (3 :&gt; F0)) (Cur (B0 :&lt; 4) 5 (6 :&gt; F0) :&gt; (Cur (B0 :&lt; 7) 8 (9 :&gt; F0) :&gt; F0))}) (C {unC = Cur B0 (Cur ((B0 :&lt; 1) :&lt; 2) 3 F0) (Cur ((B0 :&lt; 4) :&lt; 5) 6 F0 :&gt; (Cur ((B0 :&lt; 7) :&lt; 8) 9 F0 :&gt; F0))} :&gt; F0)) (Cur (B0 :&lt; C {unC = Cur (B0 :&lt; Cur B0 1 (2 :&gt; (3 :&gt; F0))) (Cur B0 4 (5 :&gt; (6 :&gt; F0))) (Cur B0 7 (8 :&gt; (9 :&gt; F0)) :&gt; F0)}) (C {unC = Cur (B0 :&lt; Cur (B0 :&lt; 1) 2 (3 :&gt; F0)) (Cur (B0 :&lt; 4) 5 (6 :&gt; F0)) (Cur (B0 :&lt; 7) 8 (9 :&gt; F0) :&gt; F0)}) (C {unC = Cur (B0 :&lt; Cur ((B0 :&lt; 1) :&lt; 2) 3 F0) (Cur ((B0 :&lt; 4) :&lt; 5) 6 F0) (Cur ((B0 :&lt; 7) :&lt; 8) 9 F0 :&gt; F0)} :&gt; F0)) (Cur (B0 :&lt; C {unC = Cur ((B0 :&lt; Cur B0 1 (2 :&gt; (3 :&gt; F0))) :&lt; Cur B0 4 (5 :&gt; (6 :&gt; F0))) (Cur B0 7 (8 :&gt; (9 :&gt; F0))) F0}) (C {unC = Cur ((B0 :&lt; Cur (B0 :&lt; 1) 2 (3 :&gt; F0)) :&lt; Cur (B0 :&lt; 4) 5 (6 :&gt; F0)) (Cur (B0 :&lt; 7) 8 (9 :&gt; F0)) F0}) (C {unC = Cur ((B0 :&lt; Cur ((B0 :&lt; 1) :&lt; 2) 3 F0) :&lt; Cur ((B0 :&lt; 4) :&lt; 5) 6 F0) (Cur ((B0 :&lt; 7) :&lt; 8) 9 F0) F0} :&gt; F0) :&gt; F0)} </code></pre> <h2>Hancock's Tensor Product</h2> <p>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 <code>f :&gt;&lt;: g</code>: 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.</p> <p>To give you the idea, consider a degenerate notion of container</p> <pre><code>data (:&lt;|) s p x = s :&lt;| (p -&gt; x) </code></pre> <p>where we say <code>s</code> is the type of "shapes" and <code>p</code> the type of "positions". A value consists of the choice of a shape and the storage of an <code>x</code> 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 product</p> <pre><code>(s :&lt;| p) :&gt;&lt;: (s' :&lt;| p') = (s, s') :&lt;| (p, p') </code></pre> <p>which 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 <code>p</code> and <code>p'</code> depend on values in <code>s</code> and <code>s'</code>, and that is exactly Hancock's definition of the tensor product of containers.</p> <h2>InContext for Tensor Products</h2> <p>Now, as you may have learned in high school, <code>∂(s :&lt;| p) = (s, p) :&lt;| (p-1)</code> where <code>p-1</code> is some type with one fewer element than <code>p</code>. Like ∂(s<em>x^p) = (s</em>p)*x^(p-1). You select one position (recording it in the shape) and delete it. The snag is that <code>p-1</code> is tricky to get your hands on without dependent types. But <code>InContext</code> selects a position <em>without deleting it</em>.</p> <pre><code>InContext (s :&lt;| p) ~= (s, p) :&lt;| p </code></pre> <p>This works just as well for the dependent case, and we joyously acquire</p> <pre><code>InContext (f :&gt;&lt;: g) ~= InContext f :&gt;&lt;: InContext g </code></pre> <p>Now we know that <code>InContext f</code> is always a <code>Comonad</code>, and this tells us that tensor products of <code>InContext</code>s are comonadic because they are themselves <code>InContext</code>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.</p> <h2>Naperian Functors</h2> <p>But there is a subclass of <code>Functor</code> for which the tensor product and the composition coincide. These are the <code>Functor</code>s <code>f</code> for which <code>f () ~ ()</code>: i.e., there is only one shape anyway, so raggedy values in compositions are ruled out in the first place. These <code>Functor</code>s are all isomorphic to <code>(p -&gt;)</code> for some position set <code>p</code> which we can think of as the <em>logarithm</em> (the exponent to which <code>x</code> must be raised to give <code>f x</code>). Correspondingly, Hancock calls these <code>Naperian</code> functors after John Napier (whose ghost haunts the part of Edinburgh where Hancock lives).</p> <pre><code>class Applicative f =&gt; Naperian f where type Log f project :: f x -&gt; Log f -&gt; x positions :: f (Log f) --- project positions = id </code></pre> <p>A <code>Naperian</code> functor has a logarithm, inducing a <code>project</code>ion function mapping positions to the elements found there. <code>Naperian</code> functors are all zippily <code>Applicative</code>, with <code>pure</code> and <code>&lt;*&gt;</code> 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.</p> <pre><code>newtype Id x = Id {unId :: x} deriving Show instance Naperian Id where type Log Id = () project (Id x) () = x positions = Id () newtype (:*:) f g x = Pr (f x, g x) deriving Show instance (Naperian f, Naperian g) =&gt; Naperian (f :*: g) where type Log (f :*: g) = Either (Log f) (Log g) project (Pr (fx, gx)) (Left p) = project fx p project (Pr (fx, gx)) (Right p) = project gx p positions = Pr (fmap Left positions, fmap Right positions) </code></pre> <p>Note that a fixed size array (a <em>vector</em>) is given by <code>(Id :*: Id :*: ... :*: Id :*: One)</code>, where <code>One</code> is the constant unit functor, whose logarithm is <code>Void</code>. So an array is <code>Naperian</code>. Now, we also have</p> <pre><code>instance (Naperian f, Naperian g) =&gt; Naperian (f :.: g) where type Log (f :.: g) = (Log f, Log g) project (C fgx) (p, q) = project (project fgx p) q positions = C $ fmap (\ p -&gt; fmap (p ,) positions) positions </code></pre> <p>which means that multi-dimensional arrays are <code>Naperian</code>.</p> <p>To construct a version of <code>InContext f</code> for <code>Naperian f</code>, just point to a position!</p> <pre><code>data Focused f x = f x :@ Log f instance Functor f =&gt; Functor (Focused f) where fmap h (fx :@ p) = fmap h fx :@ p instance Naperian f =&gt; Comonad (Focused f) where counit (fx :@ p) = project fx p cojoin (fx :@ p) = fmap (fx :@) positions :@ p </code></pre> <p>So, in particular, a <code>Focused</code> n-dimensional array will indeed be a comonad. A composition of vectors is a tensor product of n vectors, because vectors are <code>Naperian</code>. But the <code>Focused</code> n-dimensional array will be the n-fold tensor product, <em>not the composition</em>, of the n <code>Focused</code> 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.</p>
 

Querying!

 
Guidance
An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload