SOLOMON'S BLOG

functional programming, permaculture, math

After reading Chris Penner's blog post on Conway's Game
Of Life Using Representable and Comonads, I decided to implement a
similar solution for the 1 dimensional automata Rule 110. Being such a
simple algorithm I thought the implementation would be trivial. However,
it turns out that working with arbitarily bounded spaces in the
`Store Comonad`

requires a clever use of dependent types to
apply memoizaition as described in Chris' blog.

This blog post walks through my experience attempting to use
`Store`

, `Representable`

in Haskell to implement
Rule 110, difficulty finding a suitable `Representable`

instance, and then a pivot to Idris where I was able to solve the
problem using the finite set type `Fin n`

.

The Rule 110 algorithm takes a vector of boolean values and applies a simple set of rules for transforming each index based upon its neighbors. You can think of it as a 1 dimensional variant of Conway's Game of Life, but with the twist that the first and last element of the vector are considered neighbors. In other words, the automata in Rule 110 exists on a circle rather then a line segment.

Here is the rubric for generating the new state for a given element:

Current Pattern | 111 | 110 | 101 | 100 | 011 | 010 | 001 | 000 |

New State | 0 | 1 | 1 | 0 | 1 | 1 | 1 | 0 |

This post assumes no prior knowledge of Comonads, Representable
Functors, `Fin n`

. The first few sections are intended to
introduce these concepts by focusing on the actual implementations of
their APIs.

The `Store`

type can be thought of as a way to query some
indexable state along with a cursor that queries into the store at some
index.

`data Store s a = Store (s -> a) s`

State is held implicitly in your query function and, as we shall see later, can be transformed through composition.

As an example, we can construct a `Store`

whose implicit
state is an infinite list of Booleans which we index into with an
Integer:

```
initialStore :: Store Int Bool
= Store query 0
initialStore where
query :: Int -> Bool
= (cycle [True, False]) !! abs i query i
```

The `Store`

API then allows us to do things like query
arbitrary indices, shift around our cursor, and through its
`Functor`

and `Comonad`

instances to perform
transformations on the implicit state held inside the query
function.

Lets walk through the implementation of this API to gain a better intuition.

First we need a getter to lookup the current index:

```
pos :: Store s a -> s
Store query s) = s pos (
```

Next, we want a way to query the `Store`

:

```
peek :: s -> Store s a -> a
Store query _) = query s
peek s (
peeks :: (s -> s) -> Store s a -> a
Store query s) = query (f s) peeks f (
```

`peek`

disregards the current cursor and instead applies a
new cursor to the store's query function. `peeks`

uses a
function ```
s ->
s
```

to modify the current cursor and then query the store with
the new cursor.

We would also like a way to set and shift our cursor index:

```
seek :: s -> Store s a -> Store s a
Store query _) = Store query s
seek s (
seeks :: (s -> s) -> Store s a -> Store s a
Store query s) = Store query (f s) seeks f (
```

This covers are basic getters and setters, but what if we wanted a way to query multiple indices into our store?

We might write this function:

```
peekMany :: [s] -> Store s a -> [a]
= fmap (flip peek store) xs peekMany xs store
```

This function looks pretty good, but notice we are using
`fmap`

. We can take advantage of polymorphism here allow use
use of any `Functor`

:

```
peekFunctor :: Functor f => f s -> Store s a -> f a
= fmap (flip peek store) fs peekFunctor fs store
```

Now we can use any `Functor`

we want, but notice how we
aren't using our cursor at all. This is a clue that we might be able to
generalize this function further.

It would be great if we could modify `peekFunctor`

to use
our cursor value without losing the current behavior of the
function.

If we replace the `f s`

parameter with a function
`s -> f s`

then we could apply the current cursor to our
function and generate an ```
f
s
```

to generate our `f a`

output. Then if we want the
precise behavior of `peekFunctor`

we can simply apply
`const (x :: f s)`

and ignore the current cursor!

```
experiment :: Functor f => (s -> f s) -> Store s a -> f a
= fmap (flip peek store) (f (pos store)) experiment f store
```

To recap our `Store`

API we have:

```
pos :: Store s a -> a
peek :: s -> Store s a -> a
peeks :: (s -> s) Store s a -> a
seek :: s -> Store s a -> a
seeks :: (s -> s) Store s a -> a
experiment :: Functor f => (s -> f s) -> Store s a -> f a
```

The state of the system is stored implicitely inside the
`s -> a`

query function rather then in some data
structure. Because of this, the only way to modify the state would be to
modify the query function itself.

We can do this by first querying the current store to get an
`a`

value and then apply some `a -> b`

function
to the value to produce a modified version of the state at that
index.

We can do this by pattern matching on our `Store`

then
composing an `a -> b`

function with our query
function:

```
updateStoreState :: (a -> b) -> Store s a -> Store s b
Store query s) = Store (f . query) s updateStoreState f (
```

`updateStoreState`

allows you to modify the query result
for all possible values inside the Store's implicit state. This
signature shoud look familiar as it is `fmap`

and
`Store`

is in fact a `Functor`

.

```
instance Functor (Store s) where
fmap :: (a -> b) -> Store s a -> Store s b
fmap f (Store query s) = Store (f . query) s
```

Now we can model successive transformations of the state through
applications of `fmap`

. For example, using the
`Store Int Bool`

example from earlier, we might want to apply
`not :: Bool -> Bool`

to invert the state of our
system:

```
initialStore :: Store Int Bool
= Store query 0
initialStore where
= (cycle [True, False]) !! i
query i
newState :: Store Int Bool
= fmap not initialStore newState
```

Using equational reasoning we can translate that into:

```
= fmap not initialStore
newState = fmap not (Store query s)
= Store (not . query) s
```

Using this technique to model 3 manipulations of a system shows how each modification to the implicit state builds up a larger composed query function:

```
newState :: (a -> b) -> (b -> c) -> (c -> d) -> Store s a -> Store s b
= fmap f (fmap g (fmap h store))
newState h g f store = fmap f (fmap g (fmap h (Store query s)))
= fmap f (fmap g (Store (h . query) s))
= fmap f (Store (g . h . query) s)
= Store (f . g . h . query) s
```

While elegant, modeling state transformations as function composition
means that every time we query an index in a `Store`

, we must
recalculate every single previous transformation going back to the
original `Store`

query. Without caching these intermediate
computations this will get very expensive.

Luckily, Chris Penner showed us a fantastic solution for this using
Representable Functors. We will look at `Representable`

shortly, but for now lets ignore the performance issue and focus on the
tools we need to naively implement Rule 110.

Not only is `Store`

a `Functor`

, it is also a
`Comonad`

.

`Comonads`

are the dual of `Monads`

. Where
`Monads`

introduce some effect to an argument via the form
`a -> m b`

, `Comonads`

introduce a notion of
querying a structure for data (co-effects):

```
-- Monadic
-> m a
a repeat :: a -> [a]
-- Comonadic
-> a
w a length :: [a] -> Int
```

The `Comonad`

Typeclass has three functions:

```
class Functor w => Comonad w where
extract :: w a -> a
duplicate :: w a -> w (w a)
extend :: (w a -> b) -> w a -> w b
```

Notice the inverse relation to `return`

,
`join`

, and `(=<<)`

from
`Monad`

:

```
extract :: w a -> a
return :: a -> m a
duplicate :: w a -> w (w a)
join :: m (m a) -> m a
extend :: (w a -> b) -> w a -> w b
(=<<) :: (a -> m b) -> m a -> m b
```

If a defining characteristic of `Comonads`

in Haskell is
to provide a mechanism for querying some structure for data, then we can
almost definitionally say that `Store`

is a
`Comonad`

. `Store`

is literally a mechnanism for
querying a structure to produce data!

```
instance Comonad (Store s) where
extract :: Store s a -> a
Store query s) = query s
extract (
extend :: (Store s a -> b) -> Store s a -> Store s b
Store query s) = Store (\s' -> f (Store query s')) s extend f (
```

`extract`

applies the current cursor to the query function
and `extend`

chains state transforming queries.

`extract`

is fairly trivial in this case, but
`extend`

is a little trickier. It helps to think about in
relation to our `fmap`

implementation.

Like `fmap`

, it uses a function to modify our implicit
state, but where `fmap`

composed a pure
`a -> b`

function with our query, `extend`

creates a new query function by applying your entire store to a
comonadic action. This allows us to bring into scope the entire current
store when modifying particular points in the store.

`extend`

is extremely powerful and allows us to do really
interesting things like create windowing functions and perform kernel
convolution. It allows us to modify every single individual points in
"parallel" using the entire state as context.

One interesting example of extend is to perform a moving average on some time series data.

First we need a `Store`

modeling time sequenced data. We
will use `Int`

for our Index and it will represent a single
unit of time in a data stream. We want some fairly dynamic data source
so I chose the Fibbonaci sequence. At each point in time (each index) we
get the next Fibbonaci number.

```
fibStore :: Store Int Int
= store query 0
fibStore where
query :: Int -> Int
0 = 0
query 1 = 1
query = query (n - 1) + query (n - 2) query n
```

Now, if we want to calculate a window starting from a given cursor
want some way to query for the subsequent points in time.
`experiement`

will work perfectly here:

```
window :: Store Int a -> [a]
= experiment (\s -> [s..s+10]) store window store
```

I chose to fix the window at 10 units of time arbitrarily.

Now notice the shape of `window`

is
`Store Int a -> [a]`

. That looks a lot like the comonadic
action for `extend`

: ```
Store s a ->
b
```

. We can use `extend`

to apply `window`

over the enter store:

```
windowedStore :: Store Int [Int]
= extend window fibStore windowedStore
```

Now if we `peek`

at any index in the store we see a window
of the subsequent Fibonacci numbers!

```
> peek 4 $ extend window fibStore
λ3,5,8,13,21,34,55,89,144,233,377] [
```

With the tools now available to us, we can make a first attempt at our Rule 110 algorithm.

The first step is to load our initial state into the
`Store`

:

```
type Index = Int
initializeStore :: [Bool] -> Store Index Bool
= Store query 0
initializeStore xs where
query :: Index -> Bool
= xs !! i query i
```

We are modeling our initial state as a list and using an unsafe list lookup function for our query. This isn't ideal, but we are just trying to put together a rough draft.

Next we need a way to query an index and its neighbors. Just like our
windowing function, we can use `experiment`

here.

```
neighbors :: Store Index Bool -> [Bool]
= experiment _lookupIndices neighbors
```

`_lookupIndices`

is a type hole we need to fill. By
starting from `neighborValues`

we let GHC tell us what shape
we need for `lookupIndices`

:

`Found hole: _lookupIndices :: Index -> [Index] • `

We wan't something like this:

```
lookupIndices :: Int -> [Int]
= [s-1, s, s+1] lookupIndices s
```

But which accounts for the fact that our automata lives on a circle not a line. We need to be able to identify the first and last index and use that information to select the correct neighbors.

The first, simplest solution is to pass in the length of the list as a value:

```
type Index = Int
type Size = Int
lookupIndices :: Size -> Index -> [Index]
lookupIndices size i| i == 0 = [size - 1, 0, 1]
| i == size -1 = [i - 1, i, 0]
| otherwise = [i - 1, i, i + 1]
neighbors :: Size -> Store Int Bool -> [Bool]
= experiment (lookupIndices size) neighbors size
```

With a mechanism to lookup the state for our index and its neighbors,
we next need to use that information to calculate the next state of at
our index. We can do this by casing on the output of
`neighborValues`

:

Now we need to case on the state of the neighbors and apply our rubric to determine the new state at our index:

```
newState :: Size -> Store Index Bool -> Bool
=
newState size store case neighbors size store of
False, False, False] -> False
[True, False, False] -> False
[True, True, True] -> False
[-> True _
```

Lastly, we need a way to apply this transformation to the entire
store to create the next generation of the automata. `extend`

to the rescue!

```
nextGen :: Size -> Store Index Bool -> Store Index Bool
= extend (newState size) nextGen size
```

Lets use equational reasoning to take a closer look at what happens
when you call `nextGen`

:

```
= extend (newState size) store
nextGen size store = extend (newState size) (Store query s)
= Store (\s' -> (newState size) (Store query s')) s
```

And calling `nextGen`

twice:

```
= extend (newState size) (extend (newState size) store)
nextGen size (nextGen size store) = extend (newState size) (extend (newState size) (Store query s))
= extend (newState size) (Store (\s' -> (newState size) (Store query s')) s)
= Store (\s'' -> (newState size) (Store (\s' -> (newState size) (Store query s')) s'')) s
```

Its a little hard to grok, but if you squint your eyes a bit you can
see that we are building up our `query`

function by chaining
calls of `newState`

on the store. So whenever you query an
index, the composed query function will apply `newState`

a
bunch of times to your store.

The last step to a working implementation is a function to view a store as a list. This isn't really a part of the algorithm per se, but we do want a way to view our results!

```
viewStore :: Size -> Store Index Bool -> [Bool]
= experiment (const [0..size]) store viewStore size store
```

To run the simulation we can use a recursive function in
`IO`

to repeatedely print the result of
`viewStore`

and then call `nextGen`

to update the
state:

```
runSimulation :: Size -> Store Index Bool -> IO ()
= do
runSimulation size store print $ viewStore size store
$ nextGen size store runSimulation size
```

This implementation does work, but if you try running it you will see
that it has major performance issue. Extending a new generation means
growing a chain of calls to `newState`

.

This ever growing query function has to be calculated in full every
time you peek into an index. We do that for every index at every
generation when we call `runSimulation`

.

Its actually worse then that though! To calculate the new state at each index we also have to peek at its neighbors. So that means for every index we are repeating the same huge query 3 times!

What we need is a way to memoize all these calculations.

A `Functor`

`f`

is representable if it has a
corresponding type `Rep f`

that indexes `f`

completely. There must be a valid index into `f`

for every
value of `Rep f`

and at the same time we must be able to
construct a container where each element in the container is produced
from its `Rep f`

index.

Another more formal way of stating this is that there must exist an
isomorphism between `f a`

and `Rep f -> a`

.
This isomorphism is witnessed by the `tabulate`

and
`index`

functions from the `Representable`

typeclass:

```
class Functor f => Representable f where
type Rep f :: *
tabulate :: (Rep f -> a) -> f a
index :: f a -> (Rep f -> a)
```

It's hard to see exactly how this would be useful to us, but there is
a clever trick we can play with `Representable`

to get
memoization 'for free.'

`tabulate`

will takes some function that produces
`a`

values from `Rep f`

values and then
constructors a `Representable f`

containing an `a`

value for every possible `Rep f`

value.

`index`

lets you use a `Rep f`

to query a
`Representable f`

for `a`

values. One nice
property of `Representable`

is that if you have a lawful
instance then `index`

must be a safe function without the
need for `Maybe`

!

Lets try to come up with a valid instance of
`Representable`

.

The most obvious first choice for `Functor`

is
`[]`

, but what would we use for `Rep f`

?
`Int`

doesn't work because you can't have a negative index
into `[]`

. `Nat`

almost works, but then what
happes if the list is empty? Unfortunately there is no
`Representable`

instance for `[]`

.

`NonEmpty`

solves those problems, but it is still possible
to have a `NonEmpty`

without an element for every
`Nat`

.

What if our `Functor`

was an infinite stream?

```
newtype Stream a = Cons a (Strema a)
data Nat = Z | S Nat
instance Functor Stream where
fmap :: (a -> b) -> Stream a -> Stream b
fmap f (Stream a as) = Cons (f a) (fmap f as)
instance Representable Stream where
type Rep f = Nat
tabulate :: (Nat -> a) -> Stream a
= Cons (f Z) (tabulate (f . S))
tabulate f
index :: Stream a -> Nat -> a
index (Cons a as) Z = a
index (Cons _ as) (S n) = index as n
```

Yup! Our First `Representable`

. Here is another somewhat
trivial instance:

```
data Identity a = Identity a
instance Functor Identity where
fmap f (Identity a) = Identity (f a)
instance Representable Identity where
type Rep f = ()
tabulate :: (() -> a) -> Identity a
= Identity $ f ()
tabulate f
index :: Identity a -> () -> a
index (Identity a) () = a
```

Since `Identity`

can only hold a single `a`

and
`()`

is inhabited by a single value, this instance lawful and
total. :)

If our `Store`

had a single element `Identity`

would be perfect to represent queries into it and likewise, if it had an
infinite amount of elements `Stream`

might be perfect.
However, we are looking for something in between.

What we need is some sort of bounded data structure, but in order to
make it `Representable`

we also need a corresponding bounded
indexing type `Rep f`

. `Identity`

and
`()`

is a great example of a such a bounded
`Representable`

, but its bound at a fixed size of 1 element.
We would like some `Functor f`

and `Rep f`

where
we can fix the bound at whatever size we wish.

Another way of saying this is that we want is a family of
`Representable`

functors and a family of corresponding
`Rep f`

types, one pairing for each possible size
boundary.

We can do this using `Vect n a`

and `Fin n a`

.
`Vect`

is a fixed length vector whose length is encoded with
a type level `Nat`

. `Fin`

is a finite natural
whose maximum value is encoded with a type level `Nat`

.

```
data Vect (n :: Nat) a where
VNil :: Vect Z a
VCons :: a -> Vect n a -> Vect (S n) a
data Fin (n :: Nat) where
FZ :: Fin (S n)
FS :: Fin n -> Fin (S n)
```

And like that, we have entered the world of dependent types. A world very messy and confusing in Haskell. It is now time to switch over to Idris, but don't worry all the implementations up to this point are identical modulo a few small syntax changes.

Here is our `Representable`

interface (Typeclass) in Idris
and our instance for `Vect~/~Fin`

:

```
interface Functor f => Representable (f : Type -> Type) (rep : Type) | f where
tabulate : (rep -> a) -> f a
index : f a -> rep -> a
Representable (Vect n) (Fin n) where
= Z} = []
tabulate f {n = (S k)} = f FZ :: tabulate (f . FS)
tabulate f {n :: _) FZ {n = (S k)} = x
index (x _ :: xs) (FS x) {n = (S k)} = index xs x index (
```

In Idris there is no distinction between the "type level" and "term level." Types are first class values that can be passed around and worked with like any other values.

Correspondingly, type parameters (such as the `n`

in
```
Vect n (Fin
n)
```

are the same as term level parameters and can be passed
into functions and pattern matched on. You can see this in the
definition of `tabulate`

above where the `n`

from
`Vect n`

is wrapped in curly braces and treated like a
function parameter.

The curly braces indicate that it is an implict parameter. This means that the typechecker is able to infer the value of the parameter and the caller never has to explicitely pass a value in. This might seem like magic, but its very similar to the type inference you are used to with Haskell.

With this instance of `Representable`

, the indexing type
`Fin n`

cannot ever produce a value greater then
`n - 1`

and the `Functor`

must be of size
`n`

. This is guaranteed at compile time.

This means that by choosing a different value for `n`

, we
can have a `Representable`

instance for an arbitrary fixed
length vector.

Now that we have switched over to Idris we need to rewrite our
`Store`

type. We also need to make it to work with
`Representable`

:

```
data Store : (Type -> Type) -> Type -> Type -> Type where
MkStore : rep -> f a -> Store f rep a
```

This version of `Store`

contains our current index (now
called `rep`

) and our `Representable`

type
`f a`

. We no longer have a query function. Instead we are
going to store our state as data in the
`Representable Functor`

and then use the `index`

function to query it.

We then need to rewrite our API using `index`

and
`tabulate`

. `peek`

and `peeks`

, and
`extract`

are all used for querying data so they will defined
using `index`

. `extend`

is used for modifying our
query so we know we will need to use `tabulate`

.

Here is the full `Store`

API in Idris:

```
pos : Store f rep a -> rep
MkStore rep' fa) = rep'
pos (
peek : Representable f rep => rep -> Store f rep a -> a
MkStore _ fa) = index fa rep'
peek rep' (
peeks : Representable f rep => (rep -> rep) -> Store f rep a -> a
MkStore rep' fa) = index fa (f rep')
peeks f (
seek : Representable f rep => rep -> Store f rep a -> Store f rep a
MkStore _ fa) = MkStore rep' fa
seek rep' (
seeks : Representable f rep => (rep -> rep) -> Store f rep a -> Store f rep a
MkStore rep' fa) = MkStore (func rep') fa
seeks func (
experiment : (Representable f rep, Functor g) => (rep -> g rep) -> Store f rep a -> g a
= map (`peek` s) (f (pos s))
experiment f s
Representable f rep => Comonad (Store f rep) where
MkStore rep fa) = index fa rep
extract (MkStore rep' fa) = MkStore rep' (tabulate (\rep'' => func (MkStore rep'' fa))) extend func (
```

Again we use `index`

to do our actual lookup inside the
`f a`

. The real magic is in `extend`

. In our
previous `Store`

, extend created a new query function using a
lambda which applied the initial `Store`

to
`f : Store s a -> b`

:

`Store' g s) = Store (\s' -> f (Store g s')) s extend f (`

In our new version, we do the exact same thing but then we pass the
new query function into
```
tabulate :: (Fin n -> Bool) -> Vect (Fin
N) Bool
```

, which uses that query function to generate the
complete new state in a `Vect (Fin n)`

.

Lets use equational reasoning to walk through a small example of
`extend`

where we pass in a function to extract the element
at the current index and apply `not`

to it. We can use that
to create a small example where we walk through all the
subsitutions.

```
initialStore : Store (Vect (Fin 3) (Fin 3) Bool)
= MkStore FZ [True, False, True]
initialStore
= extend (not . extract) initialStore
= extend (not . extract) (MkStore FZ [True,False,True])
= extend (not . extract) (MkStore FZ (tabulate (\rep' => extract (MkStore rep' fa))))
= extend (not . extract) (MkStore FZ
\rep' => (not . extract) (MkStore rep' fa)) FZ
( (:: ((\rep' => (not . extract) (MkStore rep' fa)) . FS) FZ
:: ((\rep' => (not . extract) (MkStore rep' fa)) . FS . FS) FZ
:: [])
)= extend extract (MkStore FZ
\FZ => (not . extract) (MkStore rep' [True,False,True]))
( (:: (\(FS FZ) => (not . extract) (MkStore rep' [True,False,True]))
:: (\(FS (FS FZ)) => (not . extract) (MkStore rep' [True,False,True]))
:: [])
)= extend extract (MkStore FZ
. extract) (MkStore FZ [True,False,True])
( (not :: (not . extract) (MkStore (FS FZ) [True,False,True])
:: (not . extract) (MkStore (FS (FS FZ)) [True,False,True])
:: [])
)= extend extract (MkStore FZ
MkStore FZ [True,False,True]))
( not (extract (:: not (extract (MkStore (FS FZ) [True,False,True]))
:: not (extract (MkStore (FS (FS FZ)) [True,False,True]))
:: [])
)= extend extract (MkStore FZ
True,False,True] FZ)
( not (index [:: not (index [True,False,True] (FS FZ))
:: not (index [True,False,True] (FS (FS FZ)))
:: [])
)= extend extract (MkStore FZ
True
( not :: not False
:: not True
:: [])
)= extend extract (MkStore FZ
False
( :: True
:: False
:: [])
)= extend extract (MkStore FZ [False, True, False])
```

That example got a little big, but it demonstrates that the entire
store transformation is done once and only once when you call
`extend`

. This is a huge improvement over having to recompute
every prior generation every time you extend into a new generation.

The last thing to do is reimplement our algorith using our new
version of `Store`

. Other then switching languages, at this
point we actually don't need to modify our code a whole bunch!

The biggest changes are updating type signatures and writing some
clever helper functions to work with `Fin n`

.

First we intialize the store:

```
initialStore : Vect (3 + k) Bool -> Store (Vect (3 + k)) (Fin (3 + k)) Bool
= MkStore FZ xs initialStore xs
```

Lets take a closer look at this type signature:

- Notice the dependent type signature
`Vect (3 + k) Bool`

. This tells

the compiler that the `Vect`

's size must be 3 greater then
any `Nat`

. The smallest possible `Nat`

is 0 so
this means that the `Vect`

must be at a minimum length 3.

Notice how in the

`Store`

our`Representable`

is`Vect (3 + k)`

and our`Rep f`

is`Fin (3 + k)`

. By sharing the same type variable`k`

this tells the compiler that the`Fin`

must be 3 greater then the exact same`Nat`

as the`Vect`

.Lastly, notice how we no longer need to pass around our

`Size`

as a term. All the information we need is now encoded in the types. :)

The next function we will need to rewrite is `indices`

.
This will require some clever tricks with `Fin`

:

```
up : Fin (S k) -> Fin (S k)
= either (const FZ) FS . strengthen
up
down : Fin (S k ) -> Fin (S k)
FZ = last
down FS k) = weaken k
down (
indices : Fin (3 + k) -> Vect 3 (Fin (3 + k))
= [down x, x, up x] indices x
```

When applying `FS`

to produce the succesor to some
`Fin n`

we produce a `Fin (S n)`

. Likewise,
pattern matching and removing a `FS`

from some
`Fin (S k)`

produces a `Fin k`

.

This is a problem for us. We need to maintain the size of the finite
set as an invariant thorughout our program. We have to use some tricks
to shift our `Fin`

values while maintaining the same size of
set.

If `Fin (S k)`

represents the finite set of naturals
smaller then `k`

, then we know morally that unwrapping
`FS`

constructors from our `Fin`

does produce
numbers that fit within `Fin (S k)`

. We just need a way to
demonstrate that to the type system.

Idris provides us with `weaken`

and
`strengthen`

to do just this:

```
weaken : Fin n -> Fin (S n)
strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
```

`weaken`

says that any `Fin n`

is also a valid
`Fin (S n)`

. It's like saying any number `x`

is
smaller then `x + 1`

. This allows us to unwrap one
`FS`

from our `Fin (S k)`

to produce a number one
digit smaller that is type `Fin k`

and then convert it back
to a `Fin (S k)`

.

`last`

is another helper function from Idris that gives
you the largest valid value for `Fin n`

. In `down`

we use pattern matching and `weaken`

to produce a smaller
`Fin n`

in the successor case and `last`

in the
zero case to wrap around the modulus point.

In order to increase the value of a `x : Fin (S n)`

, we
need to show whether or not `x`

is also a valid
`Fin n`

. eg., if `x`

were 4, then it would be a
member of the set of numbers 0 to 5 and the set 0 to 4 but not the set 0
to 3.

`strengthen`

says if `x : Fin (S n)`

is too big
to be a valid ```
Fin
n
```

then return it as `Fin (S n)`

, otherwise return it
as ```
Fin
n
```

. `up`

is saying that if `x : Fin (S n)`

is too big to be `Fin n`

it must be the modulus point and we
loop around to zero. Otherwise, we convert it to `Fin n`

and
apply `FS`

to it to increment its value and keep the type as
`Fin (S n)`

.

The rest of the algorithm is as you would expect. The only changes were in the type signatures and removing the explicit threading of the size:

```
neighbors : Store (Vect (3 + k)) (Fin (3 + k)) Bool -> Vect 3 Bool
= experiment indices
neighbors
isAlive : Store (Vect (3 + k)) (Fin (3 + k)) Bool -> Bool
=
isAlive s case neighbors s of
False, False, False] => False
[True, False, False] => False
[True, True, True] => False
[_ => True
nextGen : Store (Vect (3 + k)) (Fin (3 + k)) Bool -> Store (Vect (3 + k)) (Fin (3 + k)) Bool
= extend isAlive nextGen
```

The last thing we need is an updated `runSimulation`

written in Idris:

```
universe : Vect k (Fin k)
= Z} = []
universe {k = (S k)} = FZ :: map FS (universe {k=k})
universe {k
boolToString : Bool -> String
False = "0"
boolToString True = "1"
boolToString
printState : (Vect (3 + k)) Bool -> IO ()
= do
printState xs . boolToString) $ toList xs
traverse_ (putStr ""
putStrLn
runSimulation : Store (Vect (3 + k)) (Fin (3 + k)) Bool -> IO ()
=
runSimulation s {k} if all id curr || all not curr
then printState curr
else printState curr >>= \_ => runAutomata (nextGen s)
where
curr : Vect (3 + k) Bool
= experiment (const universe) s
curr
main : IO ()
= runSimulation init
main where
start : Vect 14 Bool
= map (\i => if i == 0 then False else True) [0,0,0,1,0,0,1,1,0,1,1,1,1,1]
start init : Store (Vect 14) (Fin 14) Bool
= initialStore start init
```

And there it is! A type safe, performant implementation of Rule 110 using Comonads!