So here's a way to write code: pick a theorem, find the corresponding type, and find a function of that type.Dan then takes a result known as [Löb's Theorem](https://en.wikipedia.org/wiki/L%C3%B6b's_theorem) in modal logic and shows how one "implementation" of this theorem acts like a spreadsheet evaluator. (!) At the time I remember thinking this was pretty neat, but the depth of this strategy for finding useful abstractions went over my head. More recently I was reading that post again and it occurred to me that with some tweaking, Dan's ``loeb`` function could probably form the basis of a practical functional spreadsheet program. To recap, Löb's theorem is the following modal logic statement: $$\square(\square P \rightarrow P) \rightarrow \square P.$$ One way to interpret that statement as a type is like this: ```haskell loeb :: (Functor f) => f (f x -> x) -> f x ``` and one possible definition for such a function is this: ```haskell loeb x = fmap (\a -> a (loeb x)) x ``` For example, ``loeb`` will take a list of functions that each take a list of integers and return an integer and then return a list of integers. This allows us to define lists that refer back to parts of themselves and evaluate them in a meaningful way -- like a spreadsheet. One thing ``loeb`` *can't* do is handle relative references. For example, we can have a cell that says "add 1 to the number at cell index 2", but not one that says "add 1 to the number at the cell with index 5 less than mine". Of course relative references are an important feature of real spreadsheets, so this is a problem. Kenny Foner addressed this by replacing the ``Functor`` constraint on ``f`` with ``ComonadApply``, and wrapped this in a library called [ComonadSheet](https://github.com/kwf/ComonadSheet). The result is an infinite, lazy, $n$-dimensional spreadsheet. Have a look -- that library and its documentation have some interesting things to say. Today I'm interested in a different approach to relative references. The fundamental barrier to using relative references with ``loeb`` is that each cell needs to know something about it's "address" within the spreadsheet. For example, in a list, each entry has a position of type ``Int``; in a matrix, each entry has a position of type ``(Int, Int)``, and so on. The important thing about this position is that (1) every entry has one and (2) they are all distinct. Normally I'd refer to a position like this as an *index*, but unfortunately the term "Indexed Functor" already means something. And wouldn't you know it, the concept of a functor with index information already lives in the Lens library, where it goes by the name [FunctorWithIndex](http://hackage.haskell.org/package/lens-4.15.1/docs/Control-Lens-Indexed.html#t:FunctorWithIndex). To avoid pulling in too many dependencies I'll roll my own simplified version of this class, called an *Addressable*. For convenience, I'll make it depend on ``Applicative``. > -- t is the "container type" > -- n is the "address type" > class (Applicative t) => Addressable t n | t -> n where > > -- extract the entry at a given address > -- (not necessarily a total function) > at :: t a -> n -> a > > -- replace each entry by its address > addresses :: t a -> t n And we need an address-aware version of ``fmap``. > -- address-aware mapping > amap :: (Applicative t, Addressable t n) > => (n -> a -> b) -> t a -> t b > amap f xs = f <$> (addresses xs) <*> xs For example, here's an implementation for [``ZipLists``](https://hackage.haskell.org/package/base-4.9.1.0/docs/Control-Applicative.html#t:ZipList). (We need to use ``ZipList``s to get the right ``Applicative`` implementation.) Note that I prefer to think of lists as 1 indexed. :) > instance Addressable ZipList Int where > (ZipList as) `at` n = as !! (n-1) > > addresses as = const <$> (ZipList [1..]) <*> as And finally, the ``loeb`` function with appropriate changes. I've renamed it to ``eval``, because (1) that name is suggestive of what the function does and (2) the type isn't Löb's Theorem anymore! The ``eval'`` version is tweaked from Piponi's ``loeb``, and ``eval`` is cribbed from Foner's fixpoint-based version of ``loeb``. > -- slow > eval' :: (Addressable t n) => t (n -> t x -> x) -> t x > eval' x = amap (\i a -> a i (eval' x)) x > > -- fast > eval :: (Addressable t n) => t (n -> t x -> x) -> t x > eval x = fix $ \y -> amap (\i a -> a i y) x > > fix :: (a -> a) -> a > fix f = let x = f x in x The type of ``eval`` looks like the statement $$\square(Q \rightarrow (\square P \rightarrow P)) \rightarrow \square P,$$ and I have no idea if that means anything in the context of modal logic (I doubt it!). Now to use ``eval``, our "spreadsheet" will consist of functions that take both an address and a spreadsheet. This ``Num`` instance for functions will be handy: > instance Show (x -> a) where show = undefined > instance Eq (x -> a) where (==) = undefined > > instance (Num a, Eq a) => Num (x -> a) where > fromInteger = const . fromInteger > f + g = \x -> f x + g x > f * g = \x -> f x * g x > negate = (negate .) > abs = (abs .) > signum = (signum .) And a type synonym for convenience: > -- t is the "container" type > -- n is the "address" type > -- x is the "value" type > type Sheet t n x = t (n -> t x -> x) Now we can define boring spreadsheet-like lists like so: > test1 :: Sheet ZipList Int Int > test1 = ZipList [ 1, 3, 6 + 5 ] Try evaluating this with ``eval test1``. Woo! Note that the literal integers ``1``, ``3``, et cetera are not of type ``Int``, but type ``Int -> [Int] -> Int``, and that ``+`` operates not on ``Int``s but on functions. Useful spreadsheets include cell references, both absolute (get the value in cell 2) and relative (get the value in the cell 3 slots to the right). We'll introduce some helper functions to make this simpler. > refAbs, refRel :: (Addressable t n, Monoid n) > => n -> n -> t x -> x > > refAbs k _ xs = xs `at` k > refRel k i xs = xs `at` (mappend i k) Making the "address" type an instance of monoid makes this code more polymorphic. An instance for ``Int`` will be handy: > instance Monoid Int where > mappend = (+) > mempty = 0 Now we can write cells that refer to each other, both absolutely and relatively, like so. (Try these out with ``eval`` too.) > test2 :: Sheet ZipList Int Int > test2 = ZipList > [ 1 > , refAbs 1 > , refRel 1 + refRel (-2) > , 5 > , const (length . getZipList) > ] Here's another: this "spreadsheet" constructs the [Fibonacci sequence](https://en.wikipedia.org/wiki/Fibonacci_number). > test3 :: Sheet ZipList Int Integer > test3 = ZipList $ [0,1] ++ > repeat (refRel (-1) + refRel (-2)) Again, with Trees ----------------- Of course the whole point of polymorphism is that the same code can apply to different data. So let's try again, this time with a binary tree shaped spreadsheet. First we roll a quick type: > data Tree x > = E -- empty > | B x (Tree x) (Tree x) -- branch > deriving (Eq, Show) > > instance Functor Tree where > fmap _ E = E > fmap f (B x l r) = B (f x) (fmap f l) (fmap f r) > > instance Applicative Tree where > pure x = B x E E > > (B f l1 r1) <*> (B x l2 r2) = > B (f x) (l1 <*> l2) (r1 <*> r2) And a couple of utilities for working with trees: > -- "take" for trees > prune :: Int -> Tree x -> Tree x > prune k t > | k <= 0 = E > | otherwise = case t of > E -> E > B x a b -> B x (prune (k-1) a) (prune (k-1) b) > > -- list elements using inorder traversal > inord :: Tree x -> [x] > inord E = [] > inord (B x a b) = (inord a) ++ [x] ++ (inord b) Now how can we "address" the nodes in a binary tree? With lists a single integer sufficed, and making the integer signed allowed both absolute and relative references. There's probably a clever way to encode the position of a tree node as an integer, but I'm feeling lazy -- I'll just say that from any node we can travel to the left branch, to the right branch, or up to the parent. > -- L -> go left, R -> go right, U -> go up > data Dir = L | R | U deriving (Eq, Show) > > > instance Addressable Tree [Dir] where > at t ps = let qs = norm ps in at' t qs > where > at' (B x _ _) [] = x > at' (B _ l _) (L:es) = at' l es > at' (B _ _ r) (R:es) = at' r es > at' _ _ = undefined > > -- normalize a list of Dirs > norm :: [Dir] -> [Dir] > norm [] = [] > norm (U:x) = norm x > norm (L:U:x) = norm x > norm (R:U:x) = norm x > norm (d:x) = d : norm x > > addresses x = f x [] > where > f E _ = E > > f (B _ l r) ds > = B (reverse ds) (f l (L:ds)) (f r (R:ds)) Now ``[Dir]`` is a monoid for free, and we can do things like this: > test4 :: Sheet Tree [Dir] Int > test4 = > B 10 > (B 2 > (B (1 + refAbs []) E E) > (B (refRel [U,L] + refRel [U,U]) E E)) > (B 7 > (B 4 E E) > (B 5 E E)) Working with tree shaped "spreadsheets" is a little less natural than lists or matrices, but I suspect that is because they are less familiar. Here's another example: > mediant :: (Num a) => ((a,a),(a,a)) -> (a,a) > mediant ((x1,y1),(x2,y2)) = (x1+x2, y1+y2) > > test5 :: Sheet Tree [Dir] ((Int, Int), (Int, Int)) > test5 = B (\_ _ -> ((0,1),(1,0))) tL tR > where > tL = B (fL $ refRel[U]) tL tR > tR = B (fR $ refRel[U]) tL tR > > fL = \f h k -> let (x,y) = f h k in (x, mediant (x,y)) > fR = \f h k -> let (x,y) = f h k in (mediant (x,y), y) This one is awkward -- there are likely to be several helper functions we could factor out here. But what does it do? Try this: ```haskell $> prune 5 $ eval test5 $> fmap mediant $ prune 5 $ eval test5 $> inord $ fmap mediant $ prune 5 $ eval test5 ``` This "spreadsheet" constructs the [Stern-Brocot tree](https://en.wikipedia.org/wiki/Stern%E2%80%93Brocot_tree) of positive rational numbers. Woo! One Step Further ---------------- If we have an applicative functor and it makes sense to assign the contents "addresses", we have a kind of spreadsheet, and can use both absolute and relative references. Just out of curiosity, we can also have references that depend on a computed value like so. > crefAbs, crefRel :: (Addressable t n, Monoid n) > => (n -> t n -> n) -> n -> t n -> n > > crefAbs f i xs = xs `at` (f i xs) > crefRel f i xs = xs `at` (mappend i (f i xs)) Note that ``crefAbs`` and ``crefRel`` look a lot like ``refAbs`` and ``refRel``, except that they apply a context function. These act like the ``Indirect`` or ``Index`` functions in Excel -- they let us compute a cell reference (absolute or relative) on the fly. > test6 :: Sheet ZipList Int Int > test6 = ZipList > [ 1 > , 1 + crefAbs (2 + refRel (-1)) > , 5 > ] I don't quite have the motivation to turn this into an actual GUI-driven spreadsheet, so I'll leave that part as an exercise. :) But I am curious -- are there any other interesting applicative functors with addresses? Can oddly "shaped" spreadsheets do interesting things that array shaped ones can't? I'll end with a trivial ``main`` so this module can be typechecked as a test. > main :: IO () > main = putStrLn "ok"