# Relative references for Löb spreadsheets

This post is literate Haskell; you can copy and paste the contents to a module or just download the source file directly, load it in GHCi, and play with it on your own machine. As usual, we need to start with some pragmas and imports.

```
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
module LoebSheets where
import Data.Monoid
import Control.Applicative
```

Some years ago I read a blog post by Dan Piponi which includes the following statement:

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

and one possible definition for such a function is this:

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. 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. 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`

. (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:

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:

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.

## 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:

```
$> prune 5 $ eval test5
$> fmap mediant $ prune 5 $ eval test5
$> inord $ fmap mediant $ prune 5 $ eval test5
```

This “spreadsheet” constructs the Stern-Brocot 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.

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.