Haskell eXchange
If you’re located near London, you might be interested in the fact that I will give a talk about the contents of this blogpost at the Haskell eXchange 2018 that is happening Thursday 11th - Friday 12th of October.
After that conference, a video should be available as well which I will link here.
Introduction
This post makes a bit of a departure from the “practical Haskell” I usually try to write about, although – believe it or not – this blogpost actually originated from a very practical origin .
This blogpost is a literate Haskell file, which means you can just download it here and load it into GHCi to play around with it. In this case, you can also verify the properties we will be talking about (yes, GHC as a proof checker). Since we are dipping our toes into dependent types territory here, we will need to enable some extensions that are definitely a bit more on the advanced side.
Since the goal of this blogpost is mainly educational, we will only use a few standard modules and generally define things ourselves. This also helps us to show that there is no magic going on behind the scenes: all term-level functions in this file are total and compile fine with -Wall.
I assume most readers will be at least somewhat familiar with the standard length-indexed list:
These vectors carry their length in their types. In GHCi:
*Main> :t VCons "Hello" (VCons "World" VNull)
Vec ('Succ ('Succ 'Zero)) [Char]
This blogpost defines a similar way to deal with binomial heaps. Binomial heaps are one of my favorite data structures because of their simple elegance and the fascinating way their structure corresponds to binary numbers.
We will combine the idea of Peano number-indexed lists with the idea that binomial heaps correspond to binary numbers to lift binary numbers to the type level. This is great because we get O(log(n)) size and time in places where we would see O(n) for the Peano numbers defined above (in addition to being insanely cool). In GHCi:
*Main> :t pushHeap 'a' $ pushHeap 'b' $ pushHeap 'c' $
pushHeap 'd' $ pushHeap 'e' emptyHeap
Heap ('B1 ('B0 ('B1 'BEnd))) Char
Where 101 is, of course, the binary representation of the number 5.
Conveniently, 101 also represents the basics of a subject. So the title of this blogpost works on two levels, and we present an introductory-level explanation of a non-trivial (and again, insanely cool) example of dependent Haskell programming.
Table of contents
- Introduction
- Singletons and type equality
- Binomial heaps: let’s build it up
- Binomial trees
- Type level binary numbers
- Binomial forests
- The binomial heap
- Binomial heaps: let’s break it down
- Taking apart a single tree
- More Vec utilities
- Popcount and width
- Lumberjack
- Lumberjack: final form
- popHeap: gluing the pieces together
- Acknowledgements
- Appendices
- Appendix 1: runtime cost of this approach
- Appendix 2: “pretty”-printing of heaps
- Appendix 3: left-to-right increment
Singletons and type equality
If I perform an appropriate amount of hand-waving and squinting, I feel like there are two ways to work with these stronger-than-usual types in Haskell. We can either make sure things are correct by construction, or we can come up with a proof that they are in fact correct.
The former is the simpler approach we saw in the Vec snippet: by using the constructors provided by the GADT, our constraints are always satisfied. The latter builds on the singletons approach introduced by Richard Eisenberg and Stephanie Weirich.
We need both approaches for this blogpost. We assume that the reader is somewhat familiar with the first one and in this section we will give a brief introduction to the second one. It is in no way intended to be a full tutorial, we just want to give enough context to understand the code in the blogpost.
If we consider a closed type family for addition of natural numbers (we are using an N prefix since we will later use B for addition of binary numbers):
We can trivially define the following function:
NAdd 'Zero x is easily reduced to x by GHC since it is simply a clause of the type family, so it accepts the definition id. However, if we try to write
We run into trouble, and GHC will tell us:
Couldn't match type ‘x’ with ‘NAdd x 'Zero’
We will need to prove to GHC that these two types are equal – commutativity doesn’t come for free! This can be done by providing evidence for the equality by way of a GADT constructor .
Take a minute to think about the implications this GADT has – if we can construct a QED value, we are actually providing evidence that the two types are equal. We assume that the two types (a and b) have the same kind k .
The QED constructor lives on the term-level though, not on the type-level. We must synthesize this constructor using a term-level computation. This means we need a term-level representation of our natural numbers as well. This is the idea behind singletons and again, a much better explanation is available in said paper and some talks, but I wanted to at least provide some intuition here.
The singleton for Nat is called SNat and it’s easy to see that each Nat has a unique SNat and the other way around:
We can use such a SNat to define a proof for what we are trying to accomplish. Since this proof can be passed any n in the form of an SNat, it must be correct for all n.
GHC can figure out the base case on its own by reducing NAdd 'Zero 'Zero to 'Zero:
And we can use induction to complete the proof. The important trick here is that in the body of the pattern match on EqualityProof a b, GHC knows that a is equal to b.
This can be used to write cast02:
cast02 takes an extra parameter and there are several ways to synthesize this value. The common one is a typeclass that can give us an SNat x from a Proxy x. In this blogpost however, we keep things simple and make sure we always have the right singletons on hand by passing them around in a few places. In other words: don’t worry about this for now.
Binomial heaps: let’s build it up
Binomial trees
A binomial heap consists of zero or more binomial trees. I will quote the text from the Wikipedia article here since I think it is quite striking how straightforward the definition translates to GADTs that enforce the structure:
- A binomial tree of order 0 is a single node
- A binomial tree of order k has a root node whose children are roots of binomial trees of orders k−1, k−2, …, 2, 1, 0 (in this order).
Some illustrations to make this a bit more clear:
<figure>
<figcaption>Illustration of trees of different sizes, with the children array marked in green</figcaption>
</figure>
This is definitely a very good example of the correctness by construction approach I talked about earlier: it is simply impossible to create a tree that does not have the right shape.
Empty trees do not exist according to this definition. A singleton tree is easy to create:
We only need to define one operation on trees, namely merging two trees.
A tree of order k has 2ᵏ elements, so it makes sense that merging two trees of order k creates a tree of order k+1. We can see this in the type signature as well:
Concretely, we construct the new tree by taking either the left or the right tree and attaching it as new child to the other tree. Since we are building a heap to use as a priority queue, we want to keep the smallest element in the root of the new tree.
<figure>
<figcaption>Merging two trees. Since ‘a’ is smaller than ‘b’ we attach the ‘b’ tree as a new child to the ‘a’ tree.</figcaption>
</figure>
Type level binary numbers
With these trees defined, we can move on to binomial heaps.
While binomial trees are interesting on their own, they can really only represent collections that have a number of elements that are exactly a power of two.
Binomial heaps solve this in a surprisingly simple way. A binomial heap is a collection of binomial trees where we may only have at most one tree for every order.
This is where the correspondence with binary numbers originates. If we have a binomial heap with 5 elements, the only way to do this is to have binomial trees of orders 2 and 0 (2² + 2⁰ = 5).
We start out by defining a simple datatype that will be lifted to the kind-level, just as we did with Nat:
It’s important to note that we will represent binary numbers in a right-to-left order since this turns out to match up more naturally with the way we will be defining heaps.
For example, the type:
'B0 ('B1 ('B1 'BEnd))
represents the number 6 (conventionally written 110).
I think it is fairly common in Haskell for a developer to play around with different ways of representing a certain thing until you converge on an elegant representation. This is many, many times more important when we are dealing with dependently-typed Haskell.
Inelegant and awkward data representations can make term-level programming clunky. Inelegant and awkward type representations can make type-level programming downright infeasible due to the sheer amount of lemmas that need to be proven.
Consider the relative elegance of defining a type family for incrementing a binary number that is read from the right to the left:
Appendix 3 contains an (unused) implementation of incrementing left-to-right binary numbers. Getting things like this to work is not too much of a stretch these days (even though GHC’s error messages can be very cryptic). However, due to the large amount of type families involved, proving things about it presumably requires ritually sacrificing an inappropriate amount of Agda programmers while chanting Richard Eisenberg’s writings.
To that end, it is almost always worth spending time finding alternate representations that work out more elegantly. This can lead to some arbitrary looking choices – we will see this in full effect when trying to define CutTree further below.
Addition is not too hard to define:
Let’s quickly define a number of examples
This allows us to play around with it in GHCi:
*Main> :set -XDataKinds
*Main> :kind! BAdd BFour BFive
BAdd BFour BFive :: Binary
= 'B1 ('B0 ('B0 ('B1 'BEnd)))
Finally, we define a corresponding singleton to use later on:
Binomial forests
Our heap will be a relatively simple wrapper around a recursive type called Forest. This datastructure follows the definition of the binary numbers fairly closely, which makes the code in this section surprisingly easy and we end up requiring no lemmas or proofs whatsoever.
A Forest k b refers to a number of trees starting with (possibly) a tree of order k. The b is the binary number that indicates the shape of the forest – i.e., whether we have a tree of a given order or not.
Using a handwavy but convenient notation, this means that Forest 3 101 refers to binomial trees of order 3 and 5 (and no tree of order 4).
Note that we list the trees in increasing order here, which contrasts to Children, where we listed them in decreasing order. You can see this in the way we are removing layers of 'Succ as we add more constructors. This is the opposite of what happens in Children.
The empty forest is easily defined:
insertTree inserts a new tree into the forest. This might require merging two trees together – roughly corresponding to carrying in the binary increment operation.
Similarly, merging two forests together corresponds to adding two binary numbers together:
It’s worth seeing how the different branches in insertTree and mergeForests match up almost 1:1 with the different clauses in the definition of the type families BInc and BAdd. If we overlay them visually:
<figure>
<figcaption>Overlaying mergeForests and BAdd brings out the similarity</figcaption>
</figure>
That is the intuitive explanation as to why no additional proofs or type-level trickery are required here.
Here is an informal illustration of what happens when we don’t need to merge any trees. The singleton Forest on the left is simply put in the empty F0 spot on the right.
<figure>
<figcaption>Simple merge; 1 + 100 = 101</figcaption>
</figure>
When there is already a tree there, we merge the trees using mergeTree and carry that, in a very similar way to how carrying works in the addition of binary numbers:
<figure>
<figcaption>Merge with carry, 1 + 101 = 110</figcaption>
</figure>
The binomial heap
The Forest structure is the main workhorse and Heap is just a simple wrapper on top of that, where we start out with a tree of order 0:
The operations on Heap are also simple wrappers around the previously defined functions:
We are now ready to show this off in GHCi again:
*Main> :t pushHeap 'a' $ pushHeap 'b' $ pushHeap 'c' $
pushHeap 'd' $ pushHeap 'e' emptyHeap
Heap ('B1 ('B0 ('B1 'BEnd))) Char
We can also take a look at the internals of the datastructure using a custom show instance provided in the appendix 2:
*Main> pushHeap 'a' $ pushHeap 'b' $ pushHeap 'c' $
pushHeap 'd' $ pushHeap 'e' emptyHeap
(tree of order 0)
'a'
(no tree of order 1)
(tree of order 2)
'b'
'd'
'e'
'c'
Neat!
Binomial heaps: let’s break it down
I think it’s interesting that we have implemented an append-only heap without even requiring any lemmas so far. It is perhaps a good illustration of how append-only datastructures are conceptually much simpler.
<figure>
<figcaption>Yes, this is a long blogpost. We’ve arrived at the halfway point, so it’s a good time to get a coffee and take a break. You deserve it for sticking with me so far.</figcaption>
</figure>
Things get significantly more complicated when we try to implement popping the smallest element from the queue. For reference, I implemented the current heap in a couple of hours, whereas I worked on the rest of the code on and off for about a week.
Let’s look at a quick illustration of how popping works.
We first select the tree with the smallest root and remove it from the heap:
We break up the tree we selected into its root (which will be the element that is “popped”) and its children, which we turn into a new heap.
We merge the remainder heap from step 1 together with the new heap we made out of the children of the removed tree:
The above merge requires carrying twice.
Taking apart a single tree
We will start by implementing step 2 of the algorithm above since it is a bit easier. In this step, we are taking all children from a tree and turning that into a new heap.
We need to keep all our invariants intact, and in this case this means tracking them in the type system. A tree of k has 2ᵏ elements. If we remove the root, we have k children trees with 2ᵏ - 1 elements in total. Every child becomes a tree in the new heap. This means that the heap contains k full trees, and its shape will be written as k “1”s. This matches our math: if you write k “1”s, you get the binary notation of 2ᵏ - 1.
Visually:
<figure>
<figcaption>A tree of order 3 results in a heap with an “11” shape</figcaption>
</figure>
We introduce a type family for computing n “1”s:
We will use a helper function childrenToForest_go to maintain some invariants. The wrapper childrenToForest is trivially defined but its type tells us a whole deal:
We use childrenSingleton to obtain a singleton for n.
The tricky bit is that the list of trees in Children has them in descending order, and we want them in ascending order in Forest. This means we will have to reverse the list.
We can reverse a list easily using an accumulator in Haskell. In order to maintain the type invariants at every step, we will increase the size of the accumulator as we decrease the size of the children. This can be captured by requiring that their sum remains equal (m ~ NAdd x n).
I will not always go into detail on how the lemmas apply but let’s do it here nonetheless.
For the base case, we simply want to return our accumulator. However, our accumulator has the type Forest n (Ones x) and we expect something of the type Forest n (Ones m). Furthermore, we know that:
n ~ 'Zero, m ~ NAdd x n
⊢ m ~ NAdd x 'Zero
We need to prove that x ~ m in order to do the cast from Forest n (Ones x) to Forest n (Ones m).
We can do so by applying lemma1 to x (the latter represented here by xnat). This gives us lemma1 xnat :: NAdd x 'Zero :~: n. Combining this with what we already knew:
m ~ NAdd x 'Zero, NAdd x 'Zero ~ n
⊢ m ~ x
…which is what we needed to know.
The inductive case is a bit harder and requires us to prove that:
m ~ NAdd x n, m ~ NAdd x n, n ~ 'Succ k
⊢ Ones m ~ 'B1 (Ones (NAdd x k))
GHC does a great job and ends up with something like:
Ones (NAdd x (Succ k)) ~ 'B1 (Ones (NAdd x k))
Which only requires us to prove commutativity on NAdd. You can see that proof in lemma2 a bit further below. This case also illustrates well how we carry around the singletons as inputs for our lemmas and call on them when required.
Proving lemma2 is trivial… once you figure out what you need to prove and how all of this works.
It took me a good amount of time to put the different pieces together in my head. It is not only a matter of proving the lemma: restructuring the code in childrenToForest_go leads to different lemmas you can attempt to prove, and figuring out which ones are feasible is a big part of writing code like this.
More Vec utilities
These are some minor auxiliary functions we need to implement on Vec. We mention them here because we’ll also need two type classes dealing with non-zeroness.
First, we need some sort of map, and we can do this by implementing the Functor typeclass.
Secondly, we need a very simple function to convert a Vec to a list. Note that this erases the information we have about the size of the list.
Using vecToList, we can build a function to convert a non-empty Vec to a NonEmpty list. This uses an additional NNonZero typeclass.
Non-zeroness can be defined on binary numbers as well:
You might be asking why we cannot use a simpler type, such as:
It we use this, we run into trouble when trying to prove that a Vec is not empty later on. We would have to construct a singleton for n, and we only have something that looks a bit like ∃n. 'Succ n. Trying to get the n out of that requires some form of non-zeroness constraint… which would be exactly what we are trying to avoid by using the simpler type.
Popcount and width
The minimal element will always be the root of one of our trees. That means we have as many choices for our minimal element as there are trees in our heap. We need some way to write down this number as a type.
Since we have a tree for every 1 in our binary number, we can define the number of trees as the popcount of the binary number.
In a weird twist of fate, you can also pretend this stands for “the count of trees which we can pop”, which is exactly what we will be using it for.
Popcount can be used to relate the non-zeroness of a natural number, and the non-zeroness of a binary number.
In addition to caring about the popcount of a binary number, we are sometimes interested in its width (number of bits). This is also easily captured in a type family:
That is a fair amount of type families so far. To make things a bit more clear, here is an informal visual overview of all the type families we have defined, including BDec (binary decrement, defined further below).
<figure>
<figcaption>Rectangles represent (lifted) kinds, arrows are type families</figcaption>
</figure>
Lumberjack
Now, popping the smallest element from the heap first involves cutting a single tree from the forest inside the heap. We take the root of that tree and merge the children of the tree back together with the original heap.
<figure>
<figcaption>Selecting a single tree</figcaption>
</figure>
However, just selecting (and removing) a single tree turns out to be quite an endeavour on its own. We define an auxiliary GADT which holds the tree, the remainder of the heap, and most importantly, a lot of invariants.
Feel free to scroll down to the datatype from here if you are willing to assume the specific constraint and types are there for a reason.
The two first fields are simply evidence singletons that we carry about. k stands for the same concept as in Forest; it means we are starting with an order of k. x stands for the index of the tree that was selected.
This means the tree that was selected has an order of NAdd k x, as we can see in the third field. If the remainder of the heap is Forest k b a, its shape is denoted by b and we can reason about the shape of the original heap.
The children of tree (Tree (NAdd k x) a) that was selected will convert to a heap of shape Ones x. We work backwards from that to try and write down the type for the original heap. The tree (Tree (NAdd k x) a) would form a singleton heap of shape BInc (Ones x). The remainder (i.e., the forest with this tree removed) had shape b, so we can deduce that the original shape of the forest must have been BAdd b (BInc (Ones x)).
Finally, we restructure the type in that result to BInc (BAdd b (Ones x)). The restructuring is trivially allowed by GHC since it just requires applying the necessary type families. The restructured type turns out to be more easily usable in the places where we case-analyse CutTree further down in this blogpost.
We also carry a constraint here that seems very arbitrary and relates the widths of two binary numbers. It is easier to understand from an intuitive point of view: the new (merged) heap has the same width as the original heap. Why is it here?
Well, it turns out we will need this fact further down in a function definition. If we can conclude it here by construction in the GADT, we avoid having to prove it further down.
Of course, I know that I will need this further down because I already have the code compiling. When writing this, there is often a very, very painful dialogue in between different functions and datatypes, where you try to mediate by making the requested and expected types match by bringing them closer together step by step. In the end, you get a monstrosity like:
Fortunately, this type is internal only and doesn’t need to be exported.
lumberjack_go is the worker function that takes all possible trees out of a heap. For every 1 in the shape of the heap, we have a tree: therefore it should not be a surprise that the length of the resulting vector is Popcount b.
The definition is recursive and a good example of how recursion corresponds with inductive proofs (we’re using lemma1 and lemma2 here). We don’t go into much detail with our explanation here – this code is often hard to write, but surprisingly easy to read.
Now that we can select Popcount b trees, it’s time to convert this to something more convenient to work with. We will use a NonEmpty to represent our list of candidates to select from.
First, we select the Popcount b trees:
Then we convert it to a NonEmpty. This requires us to call lemma3 (the proof that relates non-zeroness of a binary number with non-zeroness of a natural number through popcount). We need an appropriate SBin to call lemma3 and the auxiliary function forestSingleton defined just below does that for us.
This function is similar to childrenSingleton – it constructs an appropriate singleton we can use in proofs.
popHeap: gluing the pieces together
We can now find all trees in the heap that may be cut. They are returned in a CutTree datatype. If we assume that we are taking a specific CutTree, we can take the root from the tree inside this datatype, and we can construct a new heap from its children using childrenToForest. Then, we merge it back together with the original heap.
The new heap has one less element – hence we use BDec (binary decrement, defined just a bit below).
We deconstruct the CutTree to get the root (x) of the selected tree, the children of the selected trees (children), and the remaining trees in the heap (forest).
We construct a new forest from the children.
We merge it with the remainder of the heap:
The illustration from above applies here:
<figure>
<figcaption>Merging back together</figcaption>
</figure>
Now, we cast it to the result using a new lemma4 with a singleton that we construct from the trees:
This is the type family for binary decrement. It is partial, as expected – you cannot decrement zero. This is a bit unfortunate but necessary. Having the BNonZero type family and using it as a constraint will solve that though.
The weirdly specific lemma4 helps us prove that we can take a number, increment it and then decrement it, and then get the same number back provided incrementing doesn’t change its width. This ends up matching perfectly with the width constraint generated by the CutTree, where the number that we increment is a number of “1”s smaller than the shape of the total heap (intuitively).
Using another constraint in CutTree with another proof here should also be possible. I found it hard to reason about why this constraint is necessary, but once I understood that it wasn’t too abnormal. The proof is easy though.
We don’t need to define a clause for SBEnd since Width SBEnd ~ Width (BInc SBEnd) does not hold.
Tying all of this together makes for a relatively easy readable popHeap:
Out of the different candidates, select the one with the minimal root (minimumBy is total on NonEmpty):
Pop that tree using popForest:
Helper to compare candidates by root:
In GHCi:
*Main> let heap = pushHeap 'a' $ pushHeap 'b' $ pushHeap 'c' $
pushHeap 'd' $ pushHeap 'e' emptyHeap
*Main> :t heap
heap :: Heap ('B1 ('B0 ('B1 'BEnd))) Char
*Main> :t popHeap heap
popHeap heap :: (Char, Heap ('B0 ('B0 ('B1 'BEnd))) Char)
*Main> fst $ popHeap heap
'a'
*Main> snd $ popHeap heap
(no tree of order 0)
(no tree of order 1)
(tree of order 2)
'b'
'd'
'e'
'c'
Beautiful! Our final interface to deal with the heap looks like this:
Acknowledgements
I would like to thank Alex Lang for many discussions about this and for proofreading, Akio Takano and Fumiaki Kinoshita for some whiteboarding, and Titouan Vervack and Becki Lee for many additional corrections.
I am by no means an expert in dependent types so while GHC can guarantee that my logic is sound, I cannot guarantee that my code is the most elegant or that my explanations are waterproof. In particular, I am a bit worried about the fact that binary numbers do not have unique representations – even though it does seem to make the code a bit simpler. If you have any ideas for improvements, however, feel free to reach out!
Update: Lars Brünjes contacted me and showed me a similar implementation he did for leftist heaps. You can see it in this repository. He uses a similar but unique representation of binary numbers, along the lines of:
I think is actually more elegant than the representation I used. The only disadvantage is that is a bit less concise (which is somewhat relevant for a blogpost), requiring two functions and two datatypes for most cases (e.g. a Forest k Binary and a PForest k Positive, with mergeForests and mergePForests, and so on). But if you wanted to use this idea in a real implementation, I encourage you to check that out.
Appendices
Appendix 1: runtime cost of this approach
Since we represent the proofs at runtime, we incur an overhead in two ways:
- Carrying around and allocating the singletons;
- Evaluating the lemmas to the
QED constructor.
It should be possible to remove these at runtime once the code has been typechecked, possibly using some sort of GHC core or source plugin (or CPP in a darker universe).
Another existing issue is that the tree of the spine is never “cleaned up”. We never remove trailing F0 constructors. This means that if you fill a heap of eight elements and remove all of them again, you will end up with a heap with zero elements that has the shape 'B0 ('B0 ('B0 ('B0 'BEnd))) rather than B0 'BEnd. However, this sufficed for my use case. It should be possible to add and prove a clean-up step, but it’s a bit outside the scope of this blogpost.
Appendix 2: “pretty”-printing of heaps
Appendix 3: left-to-right increment
Increment gets tricky mainly because we need some way to communicate the carry back in a right-to-left direction. We can do this with a type-level Either and some utility functions. It’s not too far from what we would write on a term-level, but again, a bit more clunky. We avoid this kind of clunkiness since having significantly more code obviously requires significantly more proving.
<section class="footnotes">
For work, I recently put together an interpreter for a lambda calculus that was way faster than I expected it to be – around 30 times as fast. I suspected this meant that something was broken, so in order to convince myself of its correctness, I wrote a well-typed version of it in the style of Francesco’s well-typed suspension calculus blogpost. It used a standard length-indexed list which had the unfortunate side effect of pushing me into O(n) territory for random access. I started looking for an asymptotically faster way to do this, which is how I ended up looking at heaps. In this blogpost, I am using the binomial heap as a priority queue rather than a bastardized random access skip list since that is what readers are presumably more familiar with.
For reasons that will become clear later on, the binary numbers that pop up on the type level should be read right-to-left. A palindrome was chosen as example here to avoid having to explain that at this point.
This type and related utilities are found in Data.Type.Equality, but redefined here for educational purposes.
The datatype in Data.Type.Equality allows equality between heterogeneous kinds as well, but we don’t need that here. This saves us from having to toggle on the “scary” {-# LANGUAGE TypeInType #-}.
I’m not sure if it is actually impossible to use this simpler type, but I did not succeed in finding a proof that uses this simpler type.
</section>
<figcaption>Girls learning computer science using Scratch (
<figcaption>The first computer, only 70 years ago</figcaption></figure>
<figcaption>Scratch, a language designed for early computer science</figcaption></figure>
</figure>
</figure>
<figcaption>The wrong way to start strength training.</figcaption></figure>
<figcaption>Middle school students learning Haskell with CodeWorld</figcaption></figure>
</figure>
and 
on lists, and list homomorphisms with an associative binary operator. For simplicity, I’m only going to be discussing finite lists.![\displaystyle \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{foldr} :: (\alpha \rightarrow \beta \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow \beta} \\ \mathit{foldr}\;(\oplus)\;e\;[\,] & = e \\ \mathit{foldr}\;(\oplus)\;e\;(a:x) & = a \oplus \mathit{foldr}\;(\oplus)\;e\;x \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dll%7D+%5Cmulticolumn%7B2%7D%7B%40%7B%7Dl%7D%7B%5Cmathit%7Bfoldr%7D+%3A%3A+%28%5Calpha+%5Crightarrow+%5Cbeta+%5Crightarrow+%5Cbeta%29+%5Crightarrow+%5Cbeta+%5Crightarrow+%5B%5Calpha%5D+%5Crightarrow+%5Cbeta%7D+%5C%5C+%5Cmathit%7Bfoldr%7D%5C%3B%28%5Coplus%29%5C%3Be%5C%3B%5B%5C%2C%5D+%26+%3D+e+%5C%5C+%5Cmathit%7Bfoldr%7D%5C%3B%28%5Coplus%29%5C%3Be%5C%3B%28a%3Ax%29+%26+%3D+a+%5Coplus+%5Cmathit%7Bfoldr%7D%5C%3B%28%5Coplus%29%5C%3Be%5C%3Bx+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{foldr} :: (\alpha \rightarrow \beta \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow \beta} \\ \mathit{foldr}\;(\oplus)\;e\;[\,] & = e \\ \mathit{foldr}\;(\oplus)\;e\;(a:x) & = a \oplus \mathit{foldr}\;(\oplus)\;e\;x \end{array}")
to be expressible as a ![\displaystyle \begin{array}{@{}l} h = \mathit{foldr}\;(\oplus)\;e \quad\Longleftrightarrow\quad h\;[\,] = e \;\land\; h\;(a:x) = a \oplus (h\;x) \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+h+%3D+%5Cmathit%7Bfoldr%7D%5C%3B%28%5Coplus%29%5C%3Be+%5Cquad%5CLongleftrightarrow%5Cquad+h%5C%3B%5B%5C%2C%5D+%3D+e+%5C%3B%5Cland%5C%3B+h%5C%3B%28a%3Ax%29+%3D+a+%5Coplus+%28h%5C%3Bx%29+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} h = \mathit{foldr}\;(\oplus)\;e \quad\Longleftrightarrow\quad h\;[\,] = e \;\land\; h\;(a:x) = a \oplus (h\;x) \end{array}")
into a 
is surjective. If 
of the form 
for some 
, not for all 
” is a concise if opaque way of writing the binary operator pointfree: 
.![\displaystyle \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{foldl} :: (\beta \rightarrow \alpha \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow \beta} \\ \mathit{foldl}\;(\oplus)\;e\;[\,] & = e \\ \mathit{foldl}\;(\oplus)\;e\;(a:x) & = \mathit{foldl}\;(\oplus)\;(e \oplus a)\;x \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dll%7D+%5Cmulticolumn%7B2%7D%7B%40%7B%7Dl%7D%7B%5Cmathit%7Bfoldl%7D+%3A%3A+%28%5Cbeta+%5Crightarrow+%5Calpha+%5Crightarrow+%5Cbeta%29+%5Crightarrow+%5Cbeta+%5Crightarrow+%5B%5Calpha%5D+%5Crightarrow+%5Cbeta%7D+%5C%5C+%5Cmathit%7Bfoldl%7D%5C%3B%28%5Coplus%29%5C%3Be%5C%3B%5B%5C%2C%5D+%26+%3D+e+%5C%5C+%5Cmathit%7Bfoldl%7D%5C%3B%28%5Coplus%29%5C%3Be%5C%3B%28a%3Ax%29+%26+%3D+%5Cmathit%7Bfoldl%7D%5C%3B%28%5Coplus%29%5C%3B%28e+%5Coplus+a%29%5C%3Bx+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{foldl} :: (\beta \rightarrow \alpha \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow \beta} \\ \mathit{foldl}\;(\oplus)\;e\;[\,] & = e \\ \mathit{foldl}\;(\oplus)\;e\;(a:x) & = \mathit{foldl}\;(\oplus)\;(e \oplus a)\;x \end{array}")
, the universal property entails abstracting that argument on the left in favour of a universal quantification on the right: ![\displaystyle \begin{array}{@{}l} h = \mathit{foldl}\;(\oplus) \quad\Longleftrightarrow\quad \forall b \;.\; h\;b\;[\,] = b \;\land\; h\;b\;(a:x) = h\;(b \oplus a)\;x \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+h+%3D+%5Cmathit%7Bfoldl%7D%5C%3B%28%5Coplus%29+%5Cquad%5CLongleftrightarrow%5Cquad+%5Cforall+b+%5C%3B.%5C%3B+h%5C%3Bb%5C%3B%5B%5C%2C%5D+%3D+b+%5C%3B%5Cland%5C%3B+h%5C%3Bb%5C%3B%28a%3Ax%29+%3D+h%5C%3B%28b+%5Coplus+a%29%5C%3Bx+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} h = \mathit{foldl}\;(\oplus) \quad\Longleftrightarrow\quad \forall b \;.\; h\;b\;[\,] = b \;\land\; h\;b\;(a:x) = h\;(b \oplus a)\;x \end{array}")
. There is also a fusion theorem: 
is associative with neutral element 
(that is, 
) and 
(for all 
, but fixed 
(but curiously, also a slight strengthening: apparently all we require is that 
, not that both equal 
; for example, we still have 
, even though 
is not the neutral element for 
).
—so: 
![{e = h\;[\,]}](https://s0.wp.com/latex.php?latex=%7Be+%3D+h%5C%3B%5B%5C%2C%5D%7D&bg=ffffff&fg=000000&s=0 "{e = h\;[\,]}")
, we have 
is a fold, but not the least bit injective. Is there a simple condition that is both sufficient and necessary for a function to be a fold? There is! The condition is that lists equivalent under 
of a function 
such that 
; this condition is equivalent to 
for every 
and 
for some 
(and it doesn’t matter what value 
, as long as indeed 
that also satisfies 
entails the same outcome 
for 
. Intuitively, it is not necessary to completely invert 
(for which indeed 
implies 
), we could pick ![{g\;b = [b]}](https://s0.wp.com/latex.php?latex=%7Bg%5C%3Bb+%3D+%5Bb%5D%7D&bg=ffffff&fg=000000&s=0 "{g\;b = [b]}")
. In particular, 
is obviously in the range of 
is chosen to be some 
, and so by construction 
—in other words, 
![\displaystyle \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{hom} :: (\beta\rightarrow\beta\rightarrow\beta) \rightarrow (\alpha\rightarrow\beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow \beta} \\ \mathit{hom}\;(\odot)\;f\;e\;[\,] & = e \\ \mathit{hom}\;(\odot)\;f\;e\;[a] & = f\;a \\ \mathit{hom}\;(\odot)\;f\;e\;(x \mathbin{{+}\!\!\!{+}} y) & = \mathit{hom}\;(\odot)\;f\;e\;x \;\odot\; \mathit{hom}\;(\odot)\;f\;e\;y \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dll%7D+%5Cmulticolumn%7B2%7D%7B%40%7B%7Dl%7D%7B%5Cmathit%7Bhom%7D+%3A%3A+%28%5Cbeta%5Crightarrow%5Cbeta%5Crightarrow%5Cbeta%29+%5Crightarrow+%28%5Calpha%5Crightarrow%5Cbeta%29+%5Crightarrow+%5Cbeta+%5Crightarrow+%5B%5Calpha%5D+%5Crightarrow+%5Cbeta%7D+%5C%5C+%5Cmathit%7Bhom%7D%5C%3B%28%5Codot%29%5C%3Bf%5C%3Be%5C%3B%5B%5C%2C%5D+%26+%3D+e+%5C%5C+%5Cmathit%7Bhom%7D%5C%3B%28%5Codot%29%5C%3Bf%5C%3Be%5C%3B%5Ba%5D+%26+%3D+f%5C%3Ba+%5C%5C+%5Cmathit%7Bhom%7D%5C%3B%28%5Codot%29%5C%3Bf%5C%3Be%5C%3B%28x+%5Cmathbin%7B%7B%2B%7D%5C%21%5C%21%5C%21%7B%2B%7D%7D+y%29+%26+%3D+%5Cmathit%7Bhom%7D%5C%3B%28%5Codot%29%5C%3Bf%5C%3Be%5C%3Bx+%5C%3B%5Codot%5C%3B+%5Cmathit%7Bhom%7D%5C%3B%28%5Codot%29%5C%3Bf%5C%3Be%5C%3By+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{hom} :: (\beta\rightarrow\beta\rightarrow\beta) \rightarrow (\alpha\rightarrow\beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow \beta} \\ \mathit{hom}\;(\odot)\;f\;e\;[\,] & = e \\ \mathit{hom}\;(\odot)\;f\;e\;[a] & = f\;a \\ \mathit{hom}\;(\odot)\;f\;e\;(x \mathbin{{+}\!\!\!{+}} y) & = \mathit{hom}\;(\odot)\;f\;e\;x \;\odot\; \mathit{hom}\;(\odot)\;f\;e\;y \end{array}")
and 
.) The Haskell library 
defines an analogous method, whose list instance is ![\displaystyle \mathit{foldMap} :: \mathit{Monoid}\;\beta \Rightarrow (\alpha \rightarrow \beta) \rightarrow [\alpha] \rightarrow \beta](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cmathit%7BfoldMap%7D+%3A%3A+%5Cmathit%7BMonoid%7D%5C%3B%5Cbeta+%5CRightarrow+%28%5Calpha+%5Crightarrow+%5Cbeta%29+%5Crightarrow+%5B%5Calpha%5D+%5Crightarrow+%5Cbeta+&bg=ffffff&fg=000000&s=0 "\displaystyle \mathit{foldMap} :: \mathit{Monoid}\;\beta \Rightarrow (\alpha \rightarrow \beta) \rightarrow [\alpha] \rightarrow \beta")
instance rather than being passed explicitly.
): 
such that 
and associative 
![\displaystyle h\;x = h\;x' \Longrightarrow h\;(x \mathbin{{+}\!\!\!{+}} [a]) = h\;(x' \mathbin{{+}\!\!\!{+}} [a])](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++h%5C%3Bx+%3D+h%5C%3Bx%27+%5CLongrightarrow+h%5C%3B%28x+%5Cmathbin%7B%7B%2B%7D%5C%21%5C%21%5C%21%7B%2B%7D%7D+%5Ba%5D%29+%3D+h%5C%3B%28x%27+%5Cmathbin%7B%7B%2B%7D%5C%21%5C%21%5C%21%7B%2B%7D%7D+%5Ba%5D%29+&bg=ffffff&fg=000000&s=0 "\displaystyle h\;x = h\;x' \Longrightarrow h\;(x \mathbin{{+}\!\!\!{+}} [a]) = h\;(x' \mathbin{{+}\!\!\!{+}} [a])")
. It also gives a specification of 
—in this case, 
suffices, because 
is right-associating, loose-binding function application). To be more precise: 
can be represented as a finite state machine over states 
, with a state transition function of type 
, and such a function is clearly not associative. But by mapping this function over the sequence of symbols, we get a sequence of 
functions, which should be subject to composition. Composition is of course associative, so can be computed in parallel, in 
steps on 
processors. Better yet, each such 
s will always kill an incoming carry, and a 
; 
and 
are both left zeroes of composition, and 
is neutral). Better still, we can compute the carry-in at all positions using a 
, which for an associative binary operator can also be performed in parallel in 
, with 
a set, and 
an associative binary operator with neutral element 
, there is another monoid 
on the carrier 
of endomorphisms of the form 
; the mappings 
and 
are both monoid homomorphisms, and are each other’s inverse. (Cayley’s Theorem is what happens to the 
takes a list element 
. The change of representation from 
is the same as in The Trick, and is also what underlies Hughes’s 
ing some arbitrary element of the final interval, we pick explicitly the lower bound of the interval (by 
, when it is represented as a pair). We suppose a function 
. We have operations on intervals: 
![\displaystyle \begin{array}{@{}l} \mathit{encode}_1 :: [\mathit{Symbol}] \rightarrow \mathit{Rational} \\ \mathit{encode}_1 = \mathit{fst} \cdot \mathit{foldl}\;\mathit{estep}_1\;\mathit{unit} \qquad \mathbf{where} \\ \qquad \begin{array}[t]{@{}l} \mathit{estep}_1 :: \mathit{Interval} \rightarrow \mathit{Symbol} \rightarrow \mathit{Interval} \\ \mathit{estep}_1\;i\;s = \mathit{narrow}\;i\;(\mathit{encodeSym}\;s) \medskip \end{array} \\ \mathit{decode}_1 :: \mathit{Rational} \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_1 = \mathit{unfoldr}\;\mathit{dstep}_1 \qquad \mathbf{where} \\ \qquad \begin{array}[t]{@{}l} \mathit{dstep}_1 :: \mathit{Rational} \rightarrow \mathsf{Maybe}\;(\mathit{Symbol}, \mathit{Rational}) \\ \mathit{dstep}_1\;x = \mathbf{let}\;s = \mathit{decodeSym}\;x\;\mathbf{in}\; \mathit{Just}\;(s, \mathit{scale}\;(\mathit{encodeSym}\;s)\;x) \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bencode%7D_1+%3A%3A+%5B%5Cmathit%7BSymbol%7D%5D+%5Crightarrow+%5Cmathit%7BRational%7D+%5C%5C+%5Cmathit%7Bencode%7D_1+%3D+%5Cmathit%7Bfst%7D+%5Ccdot+%5Cmathit%7Bfoldl%7D%5C%3B%5Cmathit%7Bestep%7D_1%5C%3B%5Cmathit%7Bunit%7D+%5Cqquad+%5Cmathbf%7Bwhere%7D+%5C%5C+%5Cqquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dl%7D+%5Cmathit%7Bestep%7D_1+%3A%3A+%5Cmathit%7BInterval%7D+%5Crightarrow+%5Cmathit%7BSymbol%7D+%5Crightarrow+%5Cmathit%7BInterval%7D+%5C%5C+%5Cmathit%7Bestep%7D_1%5C%3Bi%5C%3Bs+%3D+%5Cmathit%7Bnarrow%7D%5C%3Bi%5C%3B%28%5Cmathit%7BencodeSym%7D%5C%3Bs%29+%5Cmedskip+%5Cend%7Barray%7D+%5C%5C+%5Cmathit%7Bdecode%7D_1+%3A%3A+%5Cmathit%7BRational%7D+%5Crightarrow+%5B%5Cmathit%7BSymbol%7D%5D+%5C%5C+%5Cmathit%7Bdecode%7D_1+%3D+%5Cmathit%7Bunfoldr%7D%5C%3B%5Cmathit%7Bdstep%7D_1+%5Cqquad+%5Cmathbf%7Bwhere%7D+%5C%5C+%5Cqquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dl%7D+%5Cmathit%7Bdstep%7D_1+%3A%3A+%5Cmathit%7BRational%7D+%5Crightarrow+%5Cmathsf%7BMaybe%7D%5C%3B%28%5Cmathit%7BSymbol%7D%2C+%5Cmathit%7BRational%7D%29+%5C%5C+%5Cmathit%7Bdstep%7D_1%5C%3Bx+%3D+%5Cmathbf%7Blet%7D%5C%3Bs+%3D+%5Cmathit%7BdecodeSym%7D%5C%3Bx%5C%3B%5Cmathbf%7Bin%7D%5C%3B+%5Cmathit%7BJust%7D%5C%3B%28s%2C+%5Cmathit%7Bscale%7D%5C%3B%28%5Cmathit%7BencodeSym%7D%5C%3Bs%29%5C%3Bx%29+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{encode}_1 :: [\mathit{Symbol}] \rightarrow \mathit{Rational} \\ \mathit{encode}_1 = \mathit{fst} \cdot \mathit{foldl}\;\mathit{estep}_1\;\mathit{unit} \qquad \mathbf{where} \\ \qquad \begin{array}[t]{@{}l} \mathit{estep}_1 :: \mathit{Interval} \rightarrow \mathit{Symbol} \rightarrow \mathit{Interval} \\ \mathit{estep}_1\;i\;s = \mathit{narrow}\;i\;(\mathit{encodeSym}\;s) \medskip \end{array} \\ \mathit{decode}_1 :: \mathit{Rational} \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_1 = \mathit{unfoldr}\;\mathit{dstep}_1 \qquad \mathbf{where} \\ \qquad \begin{array}[t]{@{}l} \mathit{dstep}_1 :: \mathit{Rational} \rightarrow \mathsf{Maybe}\;(\mathit{Symbol}, \mathit{Rational}) \\ \mathit{dstep}_1\;x = \mathbf{let}\;s = \mathit{decodeSym}\;x\;\mathbf{in}\; \mathit{Just}\;(s, \mathit{scale}\;(\mathit{encodeSym}\;s)\;x) \end{array} \end{array}")
from which we select the lower bound 
of the final interval. (This version doesn’t stream well, because of the decision to pick the lower bound of the final interval as the result. But it will suffice for our purposes.)
, using map fusion for 
is associative (and 
its neutral element), so we can replace the 
back into the 
, where ![\displaystyle \begin{array}{@{}l} \mathit{encode}_2 :: [\mathit{Symbol}] \rightarrow \mathit{Rational} \\ \mathit{encode}_2 = \mathit{foldr}\;\mathit{estep}_2\;0 \qquad\mathbf{where} \\ \qquad \begin{array}[t]{@{}l} \mathit{estep}_2 :: \mathit{Symbol} \rightarrow \mathit{Rational} \rightarrow \mathit{Rational} \\ \mathit{estep}_2\;s\;x = \mathit{weight}\;(\mathit{encodeSym}\;s)\;x \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bencode%7D_2+%3A%3A+%5B%5Cmathit%7BSymbol%7D%5D+%5Crightarrow+%5Cmathit%7BRational%7D+%5C%5C+%5Cmathit%7Bencode%7D_2+%3D+%5Cmathit%7Bfoldr%7D%5C%3B%5Cmathit%7Bestep%7D_2%5C%3B0+%5Cqquad%5Cmathbf%7Bwhere%7D+%5C%5C+%5Cqquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dl%7D+%5Cmathit%7Bestep%7D_2+%3A%3A+%5Cmathit%7BSymbol%7D+%5Crightarrow+%5Cmathit%7BRational%7D+%5Crightarrow+%5Cmathit%7BRational%7D+%5C%5C+%5Cmathit%7Bestep%7D_2%5C%3Bs%5C%3Bx+%3D+%5Cmathit%7Bweight%7D%5C%3B%28%5Cmathit%7BencodeSym%7D%5C%3Bs%29%5C%3Bx+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{encode}_2 :: [\mathit{Symbol}] \rightarrow \mathit{Rational} \\ \mathit{encode}_2 = \mathit{foldr}\;\mathit{estep}_2\;0 \qquad\mathbf{where} \\ \qquad \begin{array}[t]{@{}l} \mathit{estep}_2 :: \mathit{Symbol} \rightarrow \mathit{Rational} \rightarrow \mathit{Rational} \\ \mathit{estep}_2\;s\;x = \mathit{weight}\;(\mathit{encodeSym}\;s)\;x \end{array} \end{array}")
. This means that we can prove that decoding inverts encoding, using the “Unfoldr–Foldr Theorem” stated in the Haskell documentation for 
, then 
. Actually, that’s too strong for us here, because our decoding always generates an infinite list; a weaker variation (hereby called the “Unfoldr–Foldr Theorem With Junk”) states that if 
to the output. It’s a nice exercise to prove this weaker theorem, by induction.
: 
—is in the unit interval, so indeed 
function on symbols, we can easily derive definitions 
gives the cumulative counts of all symbols preceding 
(say, in alphabetical order), 
the total of all symbol counts, and 
looks up an integer 
: 
using a scan).
bits of information (all logs in this blog are base 2). The next symbol 
, and so requires an additional 
bits; in total, that’s 
bits. So entropy considerations tell us that, roughly speaking, to incorporate symbol 
. Of course, in order to decode, we need to be able to invert this transformation, to extract 
first: 
on the remainder: 
; so we can’t yet reconstruct 
for any 
, so there is still precisely enough headroom in 
![\displaystyle \begin{array}{@{}l} \mathit{encode}_3 :: [\mathit{Symbol}] \rightarrow \mathit{Integer} \\ \mathit{encode}_3 = \mathit{foldr}\;\mathit{estep}_3\;0 \\ \mathit{estep}_3 :: \mathit{Symbol} \rightarrow \mathit{Integer} \rightarrow \mathit{Integer} \\ \mathit{estep}_3\;s\;x = \mathbf{let}\;(q,r) = \mathit{divMod}\;x\;(\mathit{count}\;s)\;\mathbf{in}\;q \times \mathit{total} + \mathit{cumul}\;s + r \medskip \\ \mathit{decode}_3 :: \mathit{Integer} \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_3 = \mathit{unfoldr}\;\mathit{dstep}_3 \\ \mathit{dstep}_3 :: \mathit{Integer} \rightarrow \mathsf{Maybe}\;(\mathit{Symbol}, \mathit{Integer}) \\ \mathit{dstep}_3\;x = \mathbf{let}\;(q,r) = \mathit{divMod}\;x\;\mathit{total} ; s = \mathit{find}\;r\;\mathbf{in}\; \mathit{Just}\;(s, \mathit{count}\;s \times q + r - \mathit{cumul}\;s) \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bencode%7D_3+%3A%3A+%5B%5Cmathit%7BSymbol%7D%5D+%5Crightarrow+%5Cmathit%7BInteger%7D+%5C%5C+%5Cmathit%7Bencode%7D_3+%3D+%5Cmathit%7Bfoldr%7D%5C%3B%5Cmathit%7Bestep%7D_3%5C%3B0+%5C%5C+%5Cmathit%7Bestep%7D_3+%3A%3A+%5Cmathit%7BSymbol%7D+%5Crightarrow+%5Cmathit%7BInteger%7D+%5Crightarrow+%5Cmathit%7BInteger%7D+%5C%5C+%5Cmathit%7Bestep%7D_3%5C%3Bs%5C%3Bx+%3D+%5Cmathbf%7Blet%7D%5C%3B%28q%2Cr%29+%3D+%5Cmathit%7BdivMod%7D%5C%3Bx%5C%3B%28%5Cmathit%7Bcount%7D%5C%3Bs%29%5C%3B%5Cmathbf%7Bin%7D%5C%3Bq+%5Ctimes+%5Cmathit%7Btotal%7D+%2B+%5Cmathit%7Bcumul%7D%5C%3Bs+%2B+r+%5Cmedskip+%5C%5C+%5Cmathit%7Bdecode%7D_3+%3A%3A+%5Cmathit%7BInteger%7D+%5Crightarrow+%5B%5Cmathit%7BSymbol%7D%5D+%5C%5C+%5Cmathit%7Bdecode%7D_3+%3D+%5Cmathit%7Bunfoldr%7D%5C%3B%5Cmathit%7Bdstep%7D_3+%5C%5C+%5Cmathit%7Bdstep%7D_3+%3A%3A+%5Cmathit%7BInteger%7D+%5Crightarrow+%5Cmathsf%7BMaybe%7D%5C%3B%28%5Cmathit%7BSymbol%7D%2C+%5Cmathit%7BInteger%7D%29+%5C%5C+%5Cmathit%7Bdstep%7D_3%5C%3Bx+%3D+%5Cmathbf%7Blet%7D%5C%3B%28q%2Cr%29+%3D+%5Cmathit%7BdivMod%7D%5C%3Bx%5C%3B%5Cmathit%7Btotal%7D+%3B+s+%3D+%5Cmathit%7Bfind%7D%5C%3Br%5C%3B%5Cmathbf%7Bin%7D%5C%3B+%5Cmathit%7BJust%7D%5C%3B%28s%2C+%5Cmathit%7Bcount%7D%5C%3Bs+%5Ctimes+q+%2B+r+-+%5Cmathit%7Bcumul%7D%5C%3Bs%29+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{encode}_3 :: [\mathit{Symbol}] \rightarrow \mathit{Integer} \\ \mathit{encode}_3 = \mathit{foldr}\;\mathit{estep}_3\;0 \\ \mathit{estep}_3 :: \mathit{Symbol} \rightarrow \mathit{Integer} \rightarrow \mathit{Integer} \\ \mathit{estep}_3\;s\;x = \mathbf{let}\;(q,r) = \mathit{divMod}\;x\;(\mathit{count}\;s)\;\mathbf{in}\;q \times \mathit{total} + \mathit{cumul}\;s + r \medskip \\ \mathit{decode}_3 :: \mathit{Integer} \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_3 = \mathit{unfoldr}\;\mathit{dstep}_3 \\ \mathit{dstep}_3 :: \mathit{Integer} \rightarrow \mathsf{Maybe}\;(\mathit{Symbol}, \mathit{Integer}) \\ \mathit{dstep}_3\;x = \mathbf{let}\;(q,r) = \mathit{divMod}\;x\;\mathit{total} ; s = \mathit{find}\;r\;\mathbf{in}\; \mathit{Just}\;(s, \mathit{count}\;s \times q + r - \mathit{cumul}\;s) \end{array}")
, and the last element 
is the encoding.
rather than 
is strictly increasing on states strictly greater than zero, and 
strictly decreasing; which means that the decoding process can stop when it returns to the lower bound. That is, if we pick some 
and define ![\displaystyle \begin{array}{@{}l} \mathit{encode}_4 :: [\mathit{Symbol}] \rightarrow \mathit{Integer} \\ \mathit{encode}_4 = \mathit{foldr}\;\mathit{estep}_3\;l \medskip \\ \mathit{decode}_4 :: \mathit{Integer} \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_4 = \mathit{unfoldr}\;\mathit{dstep}_4 \\ \mathit{dstep}_4 :: \mathit{Integer} \rightarrow \mathsf{Maybe}\;(\mathit{Symbol}, \mathit{Integer}) \\ \mathit{dstep}_4\;x = \mathbf{if}\; x==l \;\mathbf{then}\; \mathit{Nothing} \;\mathbf{else}\; \mathit{dstep}_3\;x \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bencode%7D_4+%3A%3A+%5B%5Cmathit%7BSymbol%7D%5D+%5Crightarrow+%5Cmathit%7BInteger%7D+%5C%5C+%5Cmathit%7Bencode%7D_4+%3D+%5Cmathit%7Bfoldr%7D%5C%3B%5Cmathit%7Bestep%7D_3%5C%3Bl+%5Cmedskip+%5C%5C+%5Cmathit%7Bdecode%7D_4+%3A%3A+%5Cmathit%7BInteger%7D+%5Crightarrow+%5B%5Cmathit%7BSymbol%7D%5D+%5C%5C+%5Cmathit%7Bdecode%7D_4+%3D+%5Cmathit%7Bunfoldr%7D%5C%3B%5Cmathit%7Bdstep%7D_4+%5C%5C+%5Cmathit%7Bdstep%7D_4+%3A%3A+%5Cmathit%7BInteger%7D+%5Crightarrow+%5Cmathsf%7BMaybe%7D%5C%3B%28%5Cmathit%7BSymbol%7D%2C+%5Cmathit%7BInteger%7D%29+%5C%5C+%5Cmathit%7Bdstep%7D_4%5C%3Bx+%3D+%5Cmathbf%7Bif%7D%5C%3B+x%3D%3Dl+%5C%3B%5Cmathbf%7Bthen%7D%5C%3B+%5Cmathit%7BNothing%7D+%5C%3B%5Cmathbf%7Belse%7D%5C%3B+%5Cmathit%7Bdstep%7D_3%5C%3Bx+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{encode}_4 :: [\mathit{Symbol}] \rightarrow \mathit{Integer} \\ \mathit{encode}_4 = \mathit{foldr}\;\mathit{estep}_3\;l \medskip \\ \mathit{decode}_4 :: \mathit{Integer} \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_4 = \mathit{unfoldr}\;\mathit{dstep}_4 \\ \mathit{dstep}_4 :: \mathit{Integer} \rightarrow \mathsf{Maybe}\;(\mathit{Symbol}, \mathit{Integer}) \\ \mathit{dstep}_4\;x = \mathbf{if}\; x==l \;\mathbf{then}\; \mathit{Nothing} \;\mathbf{else}\; \mathit{dstep}_3\;x \end{array}")
which we call a 
: ![\displaystyle \mathbf{type}\; \mathit{Number} = (\mathit{Integer}, [\mathit{Integer}])](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cmathbf%7Btype%7D%5C%3B+%5Cmathit%7BNumber%7D+%3D+%28%5Cmathit%7BInteger%7D%2C+%5B%5Cmathit%7BInteger%7D%5D%29+&bg=ffffff&fg=000000&s=0 "\displaystyle \mathbf{type}\; \mathit{Number} = (\mathit{Integer}, [\mathit{Integer}])")
(where we define 
for the upper bound of the range), under the abstraction relation 
and 
, the pair ![{(123,[4,5,6])}](https://s0.wp.com/latex.php?latex=%7B%28123%2C%5B4%2C5%2C6%5D%29%7D&bg=ffffff&fg=000000&s=0 "{(123,[4,5,6])}")
represents 
; and indeed, for any 
there is a unique representation satisfying the invariants. According to Duda, 
fits within a single machine word.
by shifting digits from the window to the remainder until this overflow would no longer happen, before consuming the symbol. ![\displaystyle \begin{array}{@{}l} \mathit{econsume}_5 :: [\mathit{Symbol}] \rightarrow \mathit{Number} \\ \mathit{econsume}_5 = \mathit{foldr}\;\mathit{estep}_5\;(l,[\,]) \medskip \\ \mathit{estep}_5 :: \mathit{Symbol} \rightarrow \mathit{Number} \rightarrow \mathit{Number} \\ \mathit{estep}_5\;s\;(x,\mathit{ys}) = \mathbf{let}\;(x',\mathit{ys}') = \mathit{enorm}_5\;s\;(x,\mathit{ys})\;\mathbf{in}\;(\mathit{estep}_3\;s\;x',\mathit{ys}') \medskip \\ \mathit{enorm}_5 :: \mathit{Symbol} \rightarrow \mathit{Number} \rightarrow \mathit{Number} \\ \mathit{enorm}_5\;s\;(x,\mathit{ys}) = \begin{array}[t]{@{}l@{}} \mathbf{if}\;\mathit{estep}_3\;s\;x < u \;\mathbf{then}\; (x,\mathit{ys})\;\mathbf{else}\; \\ \mathbf{let}\;(q,r) = \mathit{extract}\;x \;\mathbf{in}\; \mathit{enorm}_5\;s\;(q,r:\mathit{ys}) \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Beconsume%7D_5+%3A%3A+%5B%5Cmathit%7BSymbol%7D%5D+%5Crightarrow+%5Cmathit%7BNumber%7D+%5C%5C+%5Cmathit%7Beconsume%7D_5+%3D+%5Cmathit%7Bfoldr%7D%5C%3B%5Cmathit%7Bestep%7D_5%5C%3B%28l%2C%5B%5C%2C%5D%29+%5Cmedskip+%5C%5C+%5Cmathit%7Bestep%7D_5+%3A%3A+%5Cmathit%7BSymbol%7D+%5Crightarrow+%5Cmathit%7BNumber%7D+%5Crightarrow+%5Cmathit%7BNumber%7D+%5C%5C+%5Cmathit%7Bestep%7D_5%5C%3Bs%5C%3B%28x%2C%5Cmathit%7Bys%7D%29+%3D+%5Cmathbf%7Blet%7D%5C%3B%28x%27%2C%5Cmathit%7Bys%7D%27%29+%3D+%5Cmathit%7Benorm%7D_5%5C%3Bs%5C%3B%28x%2C%5Cmathit%7Bys%7D%29%5C%3B%5Cmathbf%7Bin%7D%5C%3B%28%5Cmathit%7Bestep%7D_3%5C%3Bs%5C%3Bx%27%2C%5Cmathit%7Bys%7D%27%29+%5Cmedskip+%5C%5C+%5Cmathit%7Benorm%7D_5+%3A%3A+%5Cmathit%7BSymbol%7D+%5Crightarrow+%5Cmathit%7BNumber%7D+%5Crightarrow+%5Cmathit%7BNumber%7D+%5C%5C+%5Cmathit%7Benorm%7D_5%5C%3Bs%5C%3B%28x%2C%5Cmathit%7Bys%7D%29+%3D+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dl%40%7B%7D%7D+%5Cmathbf%7Bif%7D%5C%3B%5Cmathit%7Bestep%7D_3%5C%3Bs%5C%3Bx+%3C+u+%5C%3B%5Cmathbf%7Bthen%7D%5C%3B+%28x%2C%5Cmathit%7Bys%7D%29%5C%3B%5Cmathbf%7Belse%7D%5C%3B+%5C%5C+%5Cmathbf%7Blet%7D%5C%3B%28q%2Cr%29+%3D+%5Cmathit%7Bextract%7D%5C%3Bx+%5C%3B%5Cmathbf%7Bin%7D%5C%3B+%5Cmathit%7Benorm%7D_5%5C%3Bs%5C%3B%28q%2Cr%3A%5Cmathit%7Bys%7D%29+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{econsume}_5 :: [\mathit{Symbol}] \rightarrow \mathit{Number} \\ \mathit{econsume}_5 = \mathit{foldr}\;\mathit{estep}_5\;(l,[\,]) \medskip \\ \mathit{estep}_5 :: \mathit{Symbol} \rightarrow \mathit{Number} \rightarrow \mathit{Number} \\ \mathit{estep}_5\;s\;(x,\mathit{ys}) = \mathbf{let}\;(x',\mathit{ys}') = \mathit{enorm}_5\;s\;(x,\mathit{ys})\;\mathbf{in}\;(\mathit{estep}_3\;s\;x',\mathit{ys}') \medskip \\ \mathit{enorm}_5 :: \mathit{Symbol} \rightarrow \mathit{Number} \rightarrow \mathit{Number} \\ \mathit{enorm}_5\;s\;(x,\mathit{ys}) = \begin{array}[t]{@{}l@{}} \mathbf{if}\;\mathit{estep}_3\;s\;x < u \;\mathbf{then}\; (x,\mathit{ys})\;\mathbf{else}\; \\ \mathbf{let}\;(q,r) = \mathit{extract}\;x \;\mathbf{in}\; \mathit{enorm}_5\;s\;(q,r:\mathit{ys}) \end{array} \end{array}")
and ![{(100,[\,])}](https://s0.wp.com/latex.php?latex=%7B%28100%2C%5B%5C%2C%5D%29%7D&bg=ffffff&fg=000000&s=0 "{(100,[\,])}")
, and goes through the states ![{(205,[\,])}](https://s0.wp.com/latex.php?latex=%7B%28205%2C%5B%5C%2C%5D%29%7D&bg=ffffff&fg=000000&s=0 "{(205,[\,])}")
and ![{(683,[\,])}](https://s0.wp.com/latex.php?latex=%7B%28683%2C%5B%5C%2C%5D%29%7D&bg=ffffff&fg=000000&s=0 "{(683,[\,])}")
on consuming the `c’ then the `b’; directly consuming the `a’ would make the window overflow, so we renormalize to ![{(68,[3])}](https://s0.wp.com/latex.php?latex=%7B%2868%2C%5B3%5D%29%7D&bg=ffffff&fg=000000&s=0 "{(68,[3])}")
; then it is safe to consume the `a’, leading to the final state ![{(340,[3])}](https://s0.wp.com/latex.php?latex=%7B%28340%2C%5B3%5D%29%7D&bg=ffffff&fg=000000&s=0 "{(340,[3])}")
.![\displaystyle \begin{array}{@{}l} \mathit{dproduce}_5 :: \mathit{Number} \rightarrow [\mathit{Symbol}] \\ \mathit{dproduce}_5 = \mathit{unfoldr}\;\mathit{dstep}_5 \medskip \\ \mathit{dstep}_5 :: \mathit{Number} \rightarrow \mathsf{Maybe}\;(\mathit{Symbol}, \mathit{Number}) \\ \mathit{dstep}_5\;(x,\mathit{ys}) = \begin{array}[t]{@{}l} \mathbf{let}\; \mathit{Just}\;(s, x') = \mathit{dstep}_3\;x ; (x'',\mathit{ys}'') = \mathit{dnorm}_5\;(x',\mathit{ys}) \;\mathbf{in} \\ \mathbf{if}\; x'' \ge l \;\mathbf{then}\; \mathit{Just}\;(s,(x'',\mathit{ys}'')) \;\mathbf{else}\; \mathit{Nothing} \medskip \end{array} \\ \mathit{dnorm}_5 :: \mathit{Number} \rightarrow \mathit{Number} \\ \mathit{dnorm}_5\;(x,y:\mathit{ys}) = \mathbf{if}\; x < l \;\mathbf{then}\; \mathit{dnorm}_5\; (\mathit{inject}\;x\;y, \mathit{ys}) \;\mathbf{else}\; (x,y:\mathit{ys}) \\ \mathit{dnorm}_5\;(x,[\,]) = (x,[\,]) \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bdproduce%7D_5+%3A%3A+%5Cmathit%7BNumber%7D+%5Crightarrow+%5B%5Cmathit%7BSymbol%7D%5D+%5C%5C+%5Cmathit%7Bdproduce%7D_5+%3D+%5Cmathit%7Bunfoldr%7D%5C%3B%5Cmathit%7Bdstep%7D_5+%5Cmedskip+%5C%5C+%5Cmathit%7Bdstep%7D_5+%3A%3A+%5Cmathit%7BNumber%7D+%5Crightarrow+%5Cmathsf%7BMaybe%7D%5C%3B%28%5Cmathit%7BSymbol%7D%2C+%5Cmathit%7BNumber%7D%29+%5C%5C+%5Cmathit%7Bdstep%7D_5%5C%3B%28x%2C%5Cmathit%7Bys%7D%29+%3D+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dl%7D+%5Cmathbf%7Blet%7D%5C%3B+%5Cmathit%7BJust%7D%5C%3B%28s%2C+x%27%29+%3D+%5Cmathit%7Bdstep%7D_3%5C%3Bx+%3B+%28x%27%27%2C%5Cmathit%7Bys%7D%27%27%29+%3D+%5Cmathit%7Bdnorm%7D_5%5C%3B%28x%27%2C%5Cmathit%7Bys%7D%29+%5C%3B%5Cmathbf%7Bin%7D+%5C%5C+%5Cmathbf%7Bif%7D%5C%3B+x%27%27+%5Cge+l+%5C%3B%5Cmathbf%7Bthen%7D%5C%3B+%5Cmathit%7BJust%7D%5C%3B%28s%2C%28x%27%27%2C%5Cmathit%7Bys%7D%27%27%29%29+%5C%3B%5Cmathbf%7Belse%7D%5C%3B+%5Cmathit%7BNothing%7D+%5Cmedskip+%5Cend%7Barray%7D+%5C%5C+%5Cmathit%7Bdnorm%7D_5+%3A%3A+%5Cmathit%7BNumber%7D+%5Crightarrow+%5Cmathit%7BNumber%7D+%5C%5C+%5Cmathit%7Bdnorm%7D_5%5C%3B%28x%2Cy%3A%5Cmathit%7Bys%7D%29+%3D+%5Cmathbf%7Bif%7D%5C%3B+x+%3C+l+%5C%3B%5Cmathbf%7Bthen%7D%5C%3B+%5Cmathit%7Bdnorm%7D_5%5C%3B+%28%5Cmathit%7Binject%7D%5C%3Bx%5C%3By%2C+%5Cmathit%7Bys%7D%29+%5C%3B%5Cmathbf%7Belse%7D%5C%3B+%28x%2Cy%3A%5Cmathit%7Bys%7D%29+%5C%5C+%5Cmathit%7Bdnorm%7D_5%5C%3B%28x%2C%5B%5C%2C%5D%29+%3D+%28x%2C%5B%5C%2C%5D%29+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{dproduce}_5 :: \mathit{Number} \rightarrow [\mathit{Symbol}] \\ \mathit{dproduce}_5 = \mathit{unfoldr}\;\mathit{dstep}_5 \medskip \\ \mathit{dstep}_5 :: \mathit{Number} \rightarrow \mathsf{Maybe}\;(\mathit{Symbol}, \mathit{Number}) \\ \mathit{dstep}_5\;(x,\mathit{ys}) = \begin{array}[t]{@{}l} \mathbf{let}\; \mathit{Just}\;(s, x') = \mathit{dstep}_3\;x ; (x'',\mathit{ys}'') = \mathit{dnorm}_5\;(x',\mathit{ys}) \;\mathbf{in} \\ \mathbf{if}\; x'' \ge l \;\mathbf{then}\; \mathit{Just}\;(s,(x'',\mathit{ys}'')) \;\mathbf{else}\; \mathit{Nothing} \medskip \end{array} \\ \mathit{dnorm}_5 :: \mathit{Number} \rightarrow \mathit{Number} \\ \mathit{dnorm}_5\;(x,y:\mathit{ys}) = \mathbf{if}\; x < l \;\mathbf{then}\; \mathit{dnorm}_5\; (\mathit{inject}\;x\;y, \mathit{ys}) \;\mathbf{else}\; (x,y:\mathit{ys}) \\ \mathit{dnorm}_5\;(x,[\,]) = (x,[\,]) \end{array}")
; the window value 68 has underflowed, so renormalization consumes the remaining digit 3, leading to the accumulator 
is an invariant of 
and 
if 
and 
. Then it is straightforward to verify that ![\displaystyle \mathit{dstep}_5\;(l,[\,]) = \mathit{Nothing}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cmathit%7Bdstep%7D_5%5C%3B%28l%2C%5B%5C%2C%5D%29+%3D+%5Cmathit%7BNothing%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \mathit{dstep}_5\;(l,[\,]) = \mathit{Nothing}")
![\displaystyle \begin{array}{@{}l} \mathit{eflush}_5 :: \mathit{Number} \rightarrow [\mathit{Integer}] \\ \mathit{eflush}_5\;(0,\mathit{ys}) = \mathit{ys} \\ \mathit{eflush}_5\;(x,\mathit{ys}) = \mathbf{let}\; (x',y) = \mathit{extract}\;x \;\mathbf{in}\; \mathit{eflush}_5\;(x',y:\mathit{ys}) \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Beflush%7D_5+%3A%3A+%5Cmathit%7BNumber%7D+%5Crightarrow+%5B%5Cmathit%7BInteger%7D%5D+%5C%5C+%5Cmathit%7Beflush%7D_5%5C%3B%280%2C%5Cmathit%7Bys%7D%29+%3D+%5Cmathit%7Bys%7D+%5C%5C+%5Cmathit%7Beflush%7D_5%5C%3B%28x%2C%5Cmathit%7Bys%7D%29+%3D+%5Cmathbf%7Blet%7D%5C%3B+%28x%27%2Cy%29+%3D+%5Cmathit%7Bextract%7D%5C%3Bx+%5C%3B%5Cmathbf%7Bin%7D%5C%3B+%5Cmathit%7Beflush%7D_5%5C%3B%28x%27%2Cy%3A%5Cmathit%7Bys%7D%29+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{eflush}_5 :: \mathit{Number} \rightarrow [\mathit{Integer}] \\ \mathit{eflush}_5\;(0,\mathit{ys}) = \mathit{ys} \\ \mathit{eflush}_5\;(x,\mathit{ys}) = \mathbf{let}\; (x',y) = \mathit{extract}\;x \;\mathbf{in}\; \mathit{eflush}_5\;(x',y:\mathit{ys}) \end{array}")
![{\mathit{eflush}_5\;(340,[3]) = [3,4,0,3]}](https://s0.wp.com/latex.php?latex=%7B%5Cmathit%7Beflush%7D_5%5C%3B%28340%2C%5B3%5D%29+%3D+%5B3%2C4%2C0%2C3%5D%7D&bg=ffffff&fg=000000&s=0 "{\mathit{eflush}_5\;(340,[3]) = [3,4,0,3]}")
. Then we can define ![\displaystyle \begin{array}{@{}l} \mathit{encode}_5 :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode}_5 = \mathit{eflush}_5 \cdot \mathit{econsume}_5 \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bencode%7D_5+%3A%3A+%5B%5Cmathit%7BSymbol%7D%5D+%5Crightarrow+%5B%5Cmathit%7BInteger%7D%5D+%5C%5C+%5Cmathit%7Bencode%7D_5+%3D+%5Cmathit%7Beflush%7D_5+%5Ccdot+%5Cmathit%7Beconsume%7D_5+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{encode}_5 :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode}_5 = \mathit{eflush}_5 \cdot \mathit{econsume}_5 \end{array}")
![\displaystyle \begin{array}{@{}l} \mathit{dstart}_5 :: [\mathit{Integer}] \rightarrow \mathit{Number} \\ \mathit{dstart}_5\;\mathit{ys} = \mathit{dnorm}_5\;(0,\mathit{ys}) \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bdstart%7D_5+%3A%3A+%5B%5Cmathit%7BInteger%7D%5D+%5Crightarrow+%5Cmathit%7BNumber%7D+%5C%5C+%5Cmathit%7Bdstart%7D_5%5C%3B%5Cmathit%7Bys%7D+%3D+%5Cmathit%7Bdnorm%7D_5%5C%3B%280%2C%5Cmathit%7Bys%7D%29+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{dstart}_5 :: [\mathit{Integer}] \rightarrow \mathit{Number} \\ \mathit{dstart}_5\;\mathit{ys} = \mathit{dnorm}_5\;(0,\mathit{ys}) \end{array}")
![{\mathit{dstart}_5\;[3,4,0,3] = (340,[3])}](https://s0.wp.com/latex.php?latex=%7B%5Cmathit%7Bdstart%7D_5%5C%3B%5B3%2C4%2C0%2C3%5D+%3D+%28340%2C%5B3%5D%29%7D&bg=ffffff&fg=000000&s=0 "{\mathit{dstart}_5\;[3,4,0,3] = (340,[3])}")
. Then we can define ![\displaystyle \begin{array}{@{}l} \mathit{decode}_5 :: [\mathit{Integer}] \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_5 = \mathit{dproduce}_5 \cdot \mathit{dstart}_5 \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bdecode%7D_5+%3A%3A+%5B%5Cmathit%7BInteger%7D%5D+%5Crightarrow+%5B%5Cmathit%7BSymbol%7D%5D+%5C%5C+%5Cmathit%7Bdecode%7D_5+%3D+%5Cmathit%7Bdproduce%7D_5+%5Ccdot+%5Cmathit%7Bdstart%7D_5+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{decode}_5 :: [\mathit{Integer}] \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_5 = \mathit{dproduce}_5 \cdot \mathit{dstart}_5 \end{array}")
yields the digits of the integer computed by 
. For example, 
, whereas ![{\mathit{encode}_5\;\mbox{\texttt{\char34{}abc\char34}} = [3,4,0,3]}](https://s0.wp.com/latex.php?latex=%7B%5Cmathit%7Bencode%7D_5%5C%3B%5Cmbox%7B%5Ctexttt%7B%5Cchar34%7B%7Dabc%5Cchar34%7D%7D+%3D+%5B3%2C4%2C0%2C3%5D%7D&bg=ffffff&fg=000000&s=0 "{\mathit{encode}_5\;\mbox{\texttt{\char34{}abc\char34}} = [3,4,0,3]}")
. We have really changed the effectiveness of the encoding in return for the increased efficiency. 
a fold; can we turn 
into an unfold? Yes, we can! The remainder in the accumulator should act as a queue of digits: digits get enqueued at the most significant end, so we need to dequeue them from the least significant end. So we define ![\displaystyle \begin{array}{@{}l} \mathit{edeal}_6 :: [\alpha] \rightarrow [\alpha] \\ \mathit{edeal}_6 = \mathit{unfoldr}\;\mathit{unsnoc} \;\mathbf{where} \\ \qquad \begin{array}[t]{@{}ll} \mathit{unsnoc}\;[\,] & = \mathit{Nothing} \\ \mathit{unsnoc}\;\mathit{ys} & = \mathbf{let}\; (\mathit{ys}',y) = (\mathit{init}\;\mathit{ys}, \mathit{last}\;\mathit{ys}) \;\mathbf{in}\; \mathit{Just}\;(y, \mathit{ys}') \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bedeal%7D_6+%3A%3A+%5B%5Calpha%5D+%5Crightarrow+%5B%5Calpha%5D+%5C%5C+%5Cmathit%7Bedeal%7D_6+%3D+%5Cmathit%7Bunfoldr%7D%5C%3B%5Cmathit%7Bunsnoc%7D+%5C%3B%5Cmathbf%7Bwhere%7D+%5C%5C+%5Cqquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dll%7D+%5Cmathit%7Bunsnoc%7D%5C%3B%5B%5C%2C%5D+%26+%3D+%5Cmathit%7BNothing%7D+%5C%5C+%5Cmathit%7Bunsnoc%7D%5C%3B%5Cmathit%7Bys%7D+%26+%3D+%5Cmathbf%7Blet%7D%5C%3B+%28%5Cmathit%7Bys%7D%27%2Cy%29+%3D+%28%5Cmathit%7Binit%7D%5C%3B%5Cmathit%7Bys%7D%2C+%5Cmathit%7Blast%7D%5C%3B%5Cmathit%7Bys%7D%29+%5C%3B%5Cmathbf%7Bin%7D%5C%3B+%5Cmathit%7BJust%7D%5C%3B%28y%2C+%5Cmathit%7Bys%7D%27%29+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{edeal}_6 :: [\alpha] \rightarrow [\alpha] \\ \mathit{edeal}_6 = \mathit{unfoldr}\;\mathit{unsnoc} \;\mathbf{where} \\ \qquad \begin{array}[t]{@{}ll} \mathit{unsnoc}\;[\,] & = \mathit{Nothing} \\ \mathit{unsnoc}\;\mathit{ys} & = \mathbf{let}\; (\mathit{ys}',y) = (\mathit{init}\;\mathit{ys}, \mathit{last}\;\mathit{ys}) \;\mathbf{in}\; \mathit{Just}\;(y, \mathit{ys}') \end{array} \end{array}")
and ![\displaystyle \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{efstep}_6 :: \mathit{Number} \rightarrow \mathsf{Maybe}\;(\mathit{Integer}, \mathit{Number})} \\ \mathit{efstep}_6\;(0,[\,]) & = \mathit{Nothing} \\ \mathit{efstep}_6\;(x,[\,]) & = \mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; \mathit{Just}\;(r,(q,[\,])) \\ \mathit{efstep}_6\;(x,\mathit{ys}) & = \mathbf{let}\; (\mathit{ys}',y) = (\mathit{init}\;\mathit{ys}, \mathit{last}\;\mathit{ys}) \;\mathbf{in}\; \mathit{Just}\;(y, (x,\mathit{ys}')) \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dll%7D+%5Cmulticolumn%7B2%7D%7B%40%7B%7Dl%7D%7B%5Cmathit%7Befstep%7D_6+%3A%3A+%5Cmathit%7BNumber%7D+%5Crightarrow+%5Cmathsf%7BMaybe%7D%5C%3B%28%5Cmathit%7BInteger%7D%2C+%5Cmathit%7BNumber%7D%29%7D+%5C%5C+%5Cmathit%7Befstep%7D_6%5C%3B%280%2C%5B%5C%2C%5D%29+%26+%3D+%5Cmathit%7BNothing%7D+%5C%5C+%5Cmathit%7Befstep%7D_6%5C%3B%28x%2C%5B%5C%2C%5D%29+%26+%3D+%5Cmathbf%7Blet%7D%5C%3B+%28q%2Cr%29+%3D+%5Cmathit%7Bextract%7D%5C%3Bx+%5C%3B%5Cmathbf%7Bin%7D%5C%3B+%5Cmathit%7BJust%7D%5C%3B%28r%2C%28q%2C%5B%5C%2C%5D%29%29+%5C%5C+%5Cmathit%7Befstep%7D_6%5C%3B%28x%2C%5Cmathit%7Bys%7D%29+%26+%3D+%5Cmathbf%7Blet%7D%5C%3B+%28%5Cmathit%7Bys%7D%27%2Cy%29+%3D+%28%5Cmathit%7Binit%7D%5C%3B%5Cmathit%7Bys%7D%2C+%5Cmathit%7Blast%7D%5C%3B%5Cmathit%7Bys%7D%29+%5C%3B%5Cmathbf%7Bin%7D%5C%3B+%5Cmathit%7BJust%7D%5C%3B%28y%2C+%28x%2C%5Cmathit%7Bys%7D%27%29%29+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{efstep}_6 :: \mathit{Number} \rightarrow \mathsf{Maybe}\;(\mathit{Integer}, \mathit{Number})} \\ \mathit{efstep}_6\;(0,[\,]) & = \mathit{Nothing} \\ \mathit{efstep}_6\;(x,[\,]) & = \mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; \mathit{Just}\;(r,(q,[\,])) \\ \mathit{efstep}_6\;(x,\mathit{ys}) & = \mathbf{let}\; (\mathit{ys}',y) = (\mathit{init}\;\mathit{ys}, \mathit{last}\;\mathit{ys}) \;\mathbf{in}\; \mathit{Just}\;(y, (x,\mathit{ys}')) \end{array}")
where ![\displaystyle \begin{array}{@{}l} \mathit{eflush}_6 :: \mathit{Number} \rightarrow [\mathit{Integer}] \\ \mathit{eflush}_6 = \mathit{reverse} \cdot \mathit{unfoldr}\;\mathit{efstep}_6 \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Beflush%7D_6+%3A%3A+%5Cmathit%7BNumber%7D+%5Crightarrow+%5B%5Cmathit%7BInteger%7D%5D+%5C%5C+%5Cmathit%7Beflush%7D_6+%3D+%5Cmathit%7Breverse%7D+%5Ccdot+%5Cmathit%7Bunfoldr%7D%5C%3B%5Cmathit%7Befstep%7D_6+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{eflush}_6 :: \mathit{Number} \rightarrow [\mathit{Integer}] \\ \mathit{eflush}_6 = \mathit{reverse} \cdot \mathit{unfoldr}\;\mathit{efstep}_6 \end{array}")
, since: 
, where ![\displaystyle \begin{array}{@{}l} \mathit{encode}_6 :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode}_6 = \mathit{reverse} \cdot \mathit{unfoldr}\;\mathit{efstep}_6 \cdot \mathit{foldl}\;(\mathit{flip}\;\mathit{estep}_5)\;(l,[\,]) \cdot \mathit{reverse} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bencode%7D_6+%3A%3A+%5B%5Cmathit%7BSymbol%7D%5D+%5Crightarrow+%5B%5Cmathit%7BInteger%7D%5D+%5C%5C+%5Cmathit%7Bencode%7D_6+%3D+%5Cmathit%7Breverse%7D+%5Ccdot+%5Cmathit%7Bunfoldr%7D%5C%3B%5Cmathit%7Befstep%7D_6+%5Ccdot+%5Cmathit%7Bfoldl%7D%5C%3B%28%5Cmathit%7Bflip%7D%5C%3B%5Cmathit%7Bestep%7D_5%29%5C%3B%28l%2C%5B%5C%2C%5D%29+%5Ccdot+%5Cmathit%7Breverse%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{encode}_6 :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode}_6 = \mathit{reverse} \cdot \mathit{unfoldr}\;\mathit{efstep}_6 \cdot \mathit{foldl}\;(\mathit{flip}\;\mathit{estep}_5)\;(l,[\,]) \cdot \mathit{reverse} \end{array}")
and 
—although we can stream digits out of the remainder: ![\displaystyle \begin{array}{@{}ll} \mathit{efstep}_6\;(123,[4,5,6]) & = \mathit{Just}\;(6,(123,[4,5])) \\ \mathit{estep}_5\;\mbox{\texttt{\char39{}c\char39}}\;(123,[4,5,6]) & = (248,[4,5,6]) \\ \mathit{efstep}_6\;(\mathit{estep}_5\;\mbox{\texttt{\char39{}c\char39}}\;(123,[4,5,6])) & = \mathit{Just}\;(6,(248,[4,5])) \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dll%7D+%5Cmathit%7Befstep%7D_6%5C%3B%28123%2C%5B4%2C5%2C6%5D%29+%26+%3D+%5Cmathit%7BJust%7D%5C%3B%286%2C%28123%2C%5B4%2C5%5D%29%29+%5C%5C+%5Cmathit%7Bestep%7D_5%5C%3B%5Cmbox%7B%5Ctexttt%7B%5Cchar39%7B%7Dc%5Cchar39%7D%7D%5C%3B%28123%2C%5B4%2C5%2C6%5D%29+%26+%3D+%28248%2C%5B4%2C5%2C6%5D%29+%5C%5C+%5Cmathit%7Befstep%7D_6%5C%3B%28%5Cmathit%7Bestep%7D_5%5C%3B%5Cmbox%7B%5Ctexttt%7B%5Cchar39%7B%7Dc%5Cchar39%7D%7D%5C%3B%28123%2C%5B4%2C5%2C6%5D%29%29+%26+%3D+%5Cmathit%7BJust%7D%5C%3B%286%2C%28248%2C%5B4%2C5%5D%29%29+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}ll} \mathit{efstep}_6\;(123,[4,5,6]) & = \mathit{Just}\;(6,(123,[4,5])) \\ \mathit{estep}_5\;\mbox{\texttt{\char39{}c\char39}}\;(123,[4,5,6]) & = (248,[4,5,6]) \\ \mathit{efstep}_6\;(\mathit{estep}_5\;\mbox{\texttt{\char39{}c\char39}}\;(123,[4,5,6])) & = \mathit{Just}\;(6,(248,[4,5])) \end{array}")
![\displaystyle \begin{array}{@{}ll} \mathit{efstep}_6\;(123,[\,]) & = \mathit{Just}\;(3,(12,[\,])) \\ \mathit{estep}_5\;\mbox{\texttt{\char39{}c\char39}}\;(123,[\,]) & = (248,[\,]) \\ \mathit{efstep}_6\;(\mathit{estep}_5\;\mbox{\texttt{\char39{}c\char39}}\;(123,[\,])) & = \mathit{Just}\;(8,(24,[\,])) \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dll%7D+%5Cmathit%7Befstep%7D_6%5C%3B%28123%2C%5B%5C%2C%5D%29+%26+%3D+%5Cmathit%7BJust%7D%5C%3B%283%2C%2812%2C%5B%5C%2C%5D%29%29+%5C%5C+%5Cmathit%7Bestep%7D_5%5C%3B%5Cmbox%7B%5Ctexttt%7B%5Cchar39%7B%7Dc%5Cchar39%7D%7D%5C%3B%28123%2C%5B%5C%2C%5D%29+%26+%3D+%28248%2C%5B%5C%2C%5D%29+%5C%5C+%5Cmathit%7Befstep%7D_6%5C%3B%28%5Cmathit%7Bestep%7D_5%5C%3B%5Cmbox%7B%5Ctexttt%7B%5Cchar39%7B%7Dc%5Cchar39%7D%7D%5C%3B%28123%2C%5B%5C%2C%5D%29%29+%26+%3D+%5Cmathit%7BJust%7D%5C%3B%288%2C%2824%2C%5B%5C%2C%5D%29%29+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}ll} \mathit{efstep}_6\;(123,[\,]) & = \mathit{Just}\;(3,(12,[\,])) \\ \mathit{estep}_5\;\mbox{\texttt{\char39{}c\char39}}\;(123,[\,]) & = (248,[\,]) \\ \mathit{efstep}_6\;(\mathit{estep}_5\;\mbox{\texttt{\char39{}c\char39}}\;(123,[\,])) & = \mathit{Just}\;(8,(24,[\,])) \end{array}")
![\displaystyle \mathit{apo} :: (\beta \rightarrow \mathsf{Maybe}\;(\gamma,\beta)) \rightarrow (\beta \rightarrow [\gamma]) \rightarrow \beta \rightarrow [\gamma]](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cmathit%7Bapo%7D+%3A%3A+%28%5Cbeta+%5Crightarrow+%5Cmathsf%7BMaybe%7D%5C%3B%28%5Cgamma%2C%5Cbeta%29%29+%5Crightarrow+%28%5Cbeta+%5Crightarrow+%5B%5Cgamma%5D%29+%5Crightarrow+%5Cbeta+%5Crightarrow+%5B%5Cgamma%5D+&bg=ffffff&fg=000000&s=0 "\displaystyle \mathit{apo} :: (\beta \rightarrow \mathsf{Maybe}\;(\gamma,\beta)) \rightarrow (\beta \rightarrow [\gamma]) \rightarrow \beta \rightarrow [\gamma]")
when it doesn’t hold for the reckless coalgebra 
and 
, where ![\displaystyle \begin{array}{@{}l} \mathit{encode}_7 :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode}_7 = \mathit{reverse} \cdot \mathit{fstream}\;\mathit{efstep}_7\;(\mathit{unfoldr}\;\mathit{efstep}_6)\;(\mathit{flip}\;\mathit{estep}_5)\;(l,[\,]) \cdot \mathit{reverse} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bencode%7D_7+%3A%3A+%5B%5Cmathit%7BSymbol%7D%5D+%5Crightarrow+%5B%5Cmathit%7BInteger%7D%5D+%5C%5C+%5Cmathit%7Bencode%7D_7+%3D+%5Cmathit%7Breverse%7D+%5Ccdot+%5Cmathit%7Bfstream%7D%5C%3B%5Cmathit%7Befstep%7D_7%5C%3B%28%5Cmathit%7Bunfoldr%7D%5C%3B%5Cmathit%7Befstep%7D_6%29%5C%3B%28%5Cmathit%7Bflip%7D%5C%3B%5Cmathit%7Bestep%7D_5%29%5C%3B%28l%2C%5B%5C%2C%5D%29+%5Ccdot+%5Cmathit%7Breverse%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{encode}_7 :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode}_7 = \mathit{reverse} \cdot \mathit{fstream}\;\mathit{efstep}_7\;(\mathit{unfoldr}\;\mathit{efstep}_6)\;(\mathit{flip}\;\mathit{estep}_5)\;(l,[\,]) \cdot \mathit{reverse} \end{array}")
streams its output. On the downside, this has to read the input text in reverse, and also write the output digit sequence in reverse.
an unfold; can we turn 
into a fold? Yes, we can! In fact, we have ![{\mathit{dstart}_5 = \mathit{foldl}\;\mathit{dsstep}_8\;(0,[\,])}](https://s0.wp.com/latex.php?latex=%7B%5Cmathit%7Bdstart%7D_5+%3D+%5Cmathit%7Bfoldl%7D%5C%3B%5Cmathit%7Bdsstep%7D_8%5C%3B%280%2C%5B%5C%2C%5D%29%7D&bg=ffffff&fg=000000&s=0 "{\mathit{dstart}_5 = \mathit{foldl}\;\mathit{dsstep}_8\;(0,[\,])}")
, where ![\displaystyle \begin{array}{@{}ll} \mathit{dsstep}_8\;(x,[\,])\;y & = \mathbf{if}\; x < l \;\mathbf{then}\; (\mathit{inject}\;x\;y, [\,]) \;\mathbf{else}\; (x, [y]) \\ \mathit{dsstep}_8\;(x,\mathit{ys})\;y & = (x, \mathit{ys} \mathbin{{+}\!\!\!{+}} [y]) \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dll%7D+%5Cmathit%7Bdsstep%7D_8%5C%3B%28x%2C%5B%5C%2C%5D%29%5C%3By+%26+%3D+%5Cmathbf%7Bif%7D%5C%3B+x+%3C+l+%5C%3B%5Cmathbf%7Bthen%7D%5C%3B+%28%5Cmathit%7Binject%7D%5C%3Bx%5C%3By%2C+%5B%5C%2C%5D%29+%5C%3B%5Cmathbf%7Belse%7D%5C%3B+%28x%2C+%5By%5D%29+%5C%5C+%5Cmathit%7Bdsstep%7D_8%5C%3B%28x%2C%5Cmathit%7Bys%7D%29%5C%3By+%26+%3D+%28x%2C+%5Cmathit%7Bys%7D+%5Cmathbin%7B%7B%2B%7D%5C%21%5C%21%5C%21%7B%2B%7D%7D+%5By%5D%29+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}ll} \mathit{dsstep}_8\;(x,[\,])\;y & = \mathbf{if}\; x < l \;\mathbf{then}\; (\mathit{inject}\;x\;y, [\,]) \;\mathbf{else}\; (x, [y]) \\ \mathit{dsstep}_8\;(x,\mathit{ys})\;y & = (x, \mathit{ys} \mathbin{{+}\!\!\!{+}} [y]) \end{array}")
. Therefore 
on finite inputs, where ![\displaystyle \begin{array}{@{}l} \mathit{decode}_8 :: [\mathit{Integer}] \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_8 = \mathit{stream}\;\mathit{dstep}_5\;\mathit{dsstep}_8\;(0,[\,]) \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bdecode%7D_8+%3A%3A+%5B%5Cmathit%7BInteger%7D%5D+%5Crightarrow+%5B%5Cmathit%7BSymbol%7D%5D+%5C%5C+%5Cmathit%7Bdecode%7D_8+%3D+%5Cmathit%7Bstream%7D%5C%3B%5Cmathit%7Bdstep%7D_5%5C%3B%5Cmathit%7Bdsstep%7D_8%5C%3B%280%2C%5B%5C%2C%5D%29+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{decode}_8 :: [\mathit{Integer}] \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_8 = \mathit{stream}\;\mathit{dstep}_5\;\mathit{dsstep}_8\;(0,[\,]) \end{array}")
streams. It is perhaps a little more symmetric to move the ![\displaystyle \begin{array}{@{}l} \mathit{encode}_9 :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode}_9 = \mathit{fstream}\;g'\;(\mathit{unfoldr}\;g)\;f\;(l,[\,]) \cdot \mathit{reverse} \;\mathbf{where} \\ \qquad \begin{array}[t]{@{}ll} f\;(x,\mathit{ys})\;s & = \begin{array}[t]{@{}ll} \mathbf{if} & x < b \times (l \mathbin{\underline{\smash{\mathit{div}}}} total) \times \mathit{count}\;s \\ \mathbf{then} & \mathbf{let}\; (q,r) = \mathit{divMod}\;x\;(\mathit{count}\;s) \;\mathbf{in}\; (q \times \mathit{total} + \mathit{cumul}\;s + r,\mathit{ys}) \\ \mathbf{else} & \mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; f\;(q, r : \mathit{ys})\;s \end{array} \\ g\;(0,[\,]) & = \mathit{Nothing} \\ g\;(x,[\,]) & = \mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; \mathit{Just}\;(r,(q,[\,])) \\ g\;(x,\mathit{ys}) & = \mathbf{let}\; (\mathit{ys}',y) = (\mathit{init}\;\mathit{ys}, \mathit{last}\;\mathit{ys}) \;\mathbf{in}\; \mathit{Just}\;(y, (x,\mathit{ys}')) \\ g'\;(x,\mathit{ys}) & = \mathbf{if}\; \mathit{null}\;\mathit{ys} \;\mathbf{then}\; \mathit{Nothing} \;\mathbf{else}\; g\;(x,\mathit{ys}) \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bencode%7D_9+%3A%3A+%5B%5Cmathit%7BSymbol%7D%5D+%5Crightarrow+%5B%5Cmathit%7BInteger%7D%5D+%5C%5C+%5Cmathit%7Bencode%7D_9+%3D+%5Cmathit%7Bfstream%7D%5C%3Bg%27%5C%3B%28%5Cmathit%7Bunfoldr%7D%5C%3Bg%29%5C%3Bf%5C%3B%28l%2C%5B%5C%2C%5D%29+%5Ccdot+%5Cmathit%7Breverse%7D+%5C%3B%5Cmathbf%7Bwhere%7D+%5C%5C+%5Cqquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dll%7D+f%5C%3B%28x%2C%5Cmathit%7Bys%7D%29%5C%3Bs+%26+%3D+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dll%7D+%5Cmathbf%7Bif%7D+%26+x+%3C+b+%5Ctimes+%28l+%5Cmathbin%7B%5Cunderline%7B%5Csmash%7B%5Cmathit%7Bdiv%7D%7D%7D%7D+total%29+%5Ctimes+%5Cmathit%7Bcount%7D%5C%3Bs+%5C%5C+%5Cmathbf%7Bthen%7D+%26+%5Cmathbf%7Blet%7D%5C%3B+%28q%2Cr%29+%3D+%5Cmathit%7BdivMod%7D%5C%3Bx%5C%3B%28%5Cmathit%7Bcount%7D%5C%3Bs%29+%5C%3B%5Cmathbf%7Bin%7D%5C%3B+%28q+%5Ctimes+%5Cmathit%7Btotal%7D+%2B+%5Cmathit%7Bcumul%7D%5C%3Bs+%2B+r%2C%5Cmathit%7Bys%7D%29+%5C%5C+%5Cmathbf%7Belse%7D+%26+%5Cmathbf%7Blet%7D%5C%3B+%28q%2Cr%29+%3D+%5Cmathit%7Bextract%7D%5C%3Bx+%5C%3B%5Cmathbf%7Bin%7D%5C%3B+f%5C%3B%28q%2C+r+%3A+%5Cmathit%7Bys%7D%29%5C%3Bs+%5Cend%7Barray%7D+%5C%5C+g%5C%3B%280%2C%5B%5C%2C%5D%29+%26+%3D+%5Cmathit%7BNothing%7D+%5C%5C+g%5C%3B%28x%2C%5B%5C%2C%5D%29+%26+%3D+%5Cmathbf%7Blet%7D%5C%3B+%28q%2Cr%29+%3D+%5Cmathit%7Bextract%7D%5C%3Bx+%5C%3B%5Cmathbf%7Bin%7D%5C%3B+%5Cmathit%7BJust%7D%5C%3B%28r%2C%28q%2C%5B%5C%2C%5D%29%29+%5C%5C+g%5C%3B%28x%2C%5Cmathit%7Bys%7D%29+%26+%3D+%5Cmathbf%7Blet%7D%5C%3B+%28%5Cmathit%7Bys%7D%27%2Cy%29+%3D+%28%5Cmathit%7Binit%7D%5C%3B%5Cmathit%7Bys%7D%2C+%5Cmathit%7Blast%7D%5C%3B%5Cmathit%7Bys%7D%29+%5C%3B%5Cmathbf%7Bin%7D%5C%3B+%5Cmathit%7BJust%7D%5C%3B%28y%2C+%28x%2C%5Cmathit%7Bys%7D%27%29%29+%5C%5C+g%27%5C%3B%28x%2C%5Cmathit%7Bys%7D%29+%26+%3D+%5Cmathbf%7Bif%7D%5C%3B+%5Cmathit%7Bnull%7D%5C%3B%5Cmathit%7Bys%7D+%5C%3B%5Cmathbf%7Bthen%7D%5C%3B+%5Cmathit%7BNothing%7D+%5C%3B%5Cmathbf%7Belse%7D%5C%3B+g%5C%3B%28x%2C%5Cmathit%7Bys%7D%29+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{encode}_9 :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode}_9 = \mathit{fstream}\;g'\;(\mathit{unfoldr}\;g)\;f\;(l,[\,]) \cdot \mathit{reverse} \;\mathbf{where} \\ \qquad \begin{array}[t]{@{}ll} f\;(x,\mathit{ys})\;s & = \begin{array}[t]{@{}ll} \mathbf{if} & x < b \times (l \mathbin{\underline{\smash{\mathit{div}}}} total) \times \mathit{count}\;s \\ \mathbf{then} & \mathbf{let}\; (q,r) = \mathit{divMod}\;x\;(\mathit{count}\;s) \;\mathbf{in}\; (q \times \mathit{total} + \mathit{cumul}\;s + r,\mathit{ys}) \\ \mathbf{else} & \mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; f\;(q, r : \mathit{ys})\;s \end{array} \\ g\;(0,[\,]) & = \mathit{Nothing} \\ g\;(x,[\,]) & = \mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; \mathit{Just}\;(r,(q,[\,])) \\ g\;(x,\mathit{ys}) & = \mathbf{let}\; (\mathit{ys}',y) = (\mathit{init}\;\mathit{ys}, \mathit{last}\;\mathit{ys}) \;\mathbf{in}\; \mathit{Just}\;(y, (x,\mathit{ys}')) \\ g'\;(x,\mathit{ys}) & = \mathbf{if}\; \mathit{null}\;\mathit{ys} \;\mathbf{then}\; \mathit{Nothing} \;\mathbf{else}\; g\;(x,\mathit{ys}) \end{array} \end{array}")
![\displaystyle \begin{array}{@{}l} \mathit{decode}_9 :: [\mathit{Integer}] \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_9 = \mathit{stream}\;g\;f\;(0,[\,]) \cdot \mathit{reverse} \;\mathbf{where} \\ \qquad \begin{array}[t]{@{}ll} g\;(x,\mathit{ys}) & = \begin{array}[t]{@{}lll} \mathbf{let} & (q,r) & = \mathit{divMod}\;x\;\mathit{total} \\ & s & = \mathit{find}\;r \\ & (x'',\mathit{ys}'') & = n\;(\mathit{count}\;s \times q + r - \mathit{cumul}\;s,\mathit{ys}) \\ \mathbf{in} & \multicolumn{2}{l}{\mathbf{if}\; x'' \ge l \;\mathbf{then}\; \mathit{Just}\;(s,(x'',\mathit{ys}'')) \;\mathbf{else}\; \mathit{Nothing}} \end{array} \\ n\;(x,\mathit{ys}) & = \begin{array}[t]{@{}l} \mathbf{if}\; x\ge l \lor \mathit{null}\;\mathit{ys} \;\mathbf{then}\; (x,\mathit{ys}) \;\mathbf{else} \\ \mathbf{let}\; (y:\mathit{ys}') = \mathit{ys} \;\mathbf{in}\; n\;(\mathit{inject}\;x\;y, \mathit{ys}') \end{array} \\ f\;(x,[\,]) y & = n\;(x,[y]) \\ f\;(x,\mathit{ys})\;y & = (x, \mathit{ys} \mathbin{{+}\!\!\!{+}} [y]) \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bdecode%7D_9+%3A%3A+%5B%5Cmathit%7BInteger%7D%5D+%5Crightarrow+%5B%5Cmathit%7BSymbol%7D%5D+%5C%5C+%5Cmathit%7Bdecode%7D_9+%3D+%5Cmathit%7Bstream%7D%5C%3Bg%5C%3Bf%5C%3B%280%2C%5B%5C%2C%5D%29+%5Ccdot+%5Cmathit%7Breverse%7D+%5C%3B%5Cmathbf%7Bwhere%7D+%5C%5C+%5Cqquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dll%7D+g%5C%3B%28x%2C%5Cmathit%7Bys%7D%29+%26+%3D+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dlll%7D+%5Cmathbf%7Blet%7D+%26+%28q%2Cr%29+%26+%3D+%5Cmathit%7BdivMod%7D%5C%3Bx%5C%3B%5Cmathit%7Btotal%7D+%5C%5C+%26+s+%26+%3D+%5Cmathit%7Bfind%7D%5C%3Br+%5C%5C+%26+%28x%27%27%2C%5Cmathit%7Bys%7D%27%27%29+%26+%3D+n%5C%3B%28%5Cmathit%7Bcount%7D%5C%3Bs+%5Ctimes+q+%2B+r+-+%5Cmathit%7Bcumul%7D%5C%3Bs%2C%5Cmathit%7Bys%7D%29+%5C%5C+%5Cmathbf%7Bin%7D+%26+%5Cmulticolumn%7B2%7D%7Bl%7D%7B%5Cmathbf%7Bif%7D%5C%3B+x%27%27+%5Cge+l+%5C%3B%5Cmathbf%7Bthen%7D%5C%3B+%5Cmathit%7BJust%7D%5C%3B%28s%2C%28x%27%27%2C%5Cmathit%7Bys%7D%27%27%29%29+%5C%3B%5Cmathbf%7Belse%7D%5C%3B+%5Cmathit%7BNothing%7D%7D+%5Cend%7Barray%7D+%5C%5C+n%5C%3B%28x%2C%5Cmathit%7Bys%7D%29+%26+%3D+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dl%7D+%5Cmathbf%7Bif%7D%5C%3B+x%5Cge+l+%5Clor+%5Cmathit%7Bnull%7D%5C%3B%5Cmathit%7Bys%7D+%5C%3B%5Cmathbf%7Bthen%7D%5C%3B+%28x%2C%5Cmathit%7Bys%7D%29+%5C%3B%5Cmathbf%7Belse%7D+%5C%5C+%5Cmathbf%7Blet%7D%5C%3B+%28y%3A%5Cmathit%7Bys%7D%27%29+%3D+%5Cmathit%7Bys%7D+%5C%3B%5Cmathbf%7Bin%7D%5C%3B+n%5C%3B%28%5Cmathit%7Binject%7D%5C%3Bx%5C%3By%2C+%5Cmathit%7Bys%7D%27%29+%5Cend%7Barray%7D+%5C%5C+f%5C%3B%28x%2C%5B%5C%2C%5D%29+y+%26+%3D+n%5C%3B%28x%2C%5By%5D%29+%5C%5C+f%5C%3B%28x%2C%5Cmathit%7Bys%7D%29%5C%3By+%26+%3D+%28x%2C+%5Cmathit%7Bys%7D+%5Cmathbin%7B%7B%2B%7D%5C%21%5C%21%5C%21%7B%2B%7D%7D+%5By%5D%29+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{decode}_9 :: [\mathit{Integer}] \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_9 = \mathit{stream}\;g\;f\;(0,[\,]) \cdot \mathit{reverse} \;\mathbf{where} \\ \qquad \begin{array}[t]{@{}ll} g\;(x,\mathit{ys}) & = \begin{array}[t]{@{}lll} \mathbf{let} & (q,r) & = \mathit{divMod}\;x\;\mathit{total} \\ & s & = \mathit{find}\;r \\ & (x'',\mathit{ys}'') & = n\;(\mathit{count}\;s \times q + r - \mathit{cumul}\;s,\mathit{ys}) \\ \mathbf{in} & \multicolumn{2}{l}{\mathbf{if}\; x'' \ge l \;\mathbf{then}\; \mathit{Just}\;(s,(x'',\mathit{ys}'')) \;\mathbf{else}\; \mathit{Nothing}} \end{array} \\ n\;(x,\mathit{ys}) & = \begin{array}[t]{@{}l} \mathbf{if}\; x\ge l \lor \mathit{null}\;\mathit{ys} \;\mathbf{then}\; (x,\mathit{ys}) \;\mathbf{else} \\ \mathbf{let}\; (y:\mathit{ys}') = \mathit{ys} \;\mathbf{in}\; n\;(\mathit{inject}\;x\;y, \mathit{ys}') \end{array} \\ f\;(x,[\,]) y & = n\;(x,[y]) \\ f\;(x,\mathit{ys})\;y & = (x, \mathit{ys} \mathbin{{+}\!\!\!{+}} [y]) \end{array} \end{array}")
![\displaystyle \begin{array}{@{}l} \mathit{encode} :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode} = h_1\;l \cdot \mathit{reverse} \qquad \mathbf{where} \\ \qquad \begin{array}[t]{@{}ll} h_1\;x\;(s:\mathit{ss}') & = \begin{array}[t]{@{}ll} \mathbf{if} & x < b \times (l \mathbin{\underline{\smash{\mathit{div}}}} \mathit{total}) \times \mathit{count}\;s \\ \mathbf{then} & \mathbf{let}\; (q,r) = \mathit{divMod}\;x\;(\mathit{count}\;s) \;\mathbf{in}\; h_1\;(q \times total + \mathit{cumul}\;s + r)\;\mathit{ss}' \\ \mathbf{else} & \mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; r : h_1\;q\;(s:\mathit{ss}') \end{array} \\ h_1\;x\;[\,] & = h_2\;x \\ h_2\;x & = \mathbf{if}\; x==0 \;\mathbf{then}\; [\,] \;\mathbf{else}\;\mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; r : h_2\;q \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bencode%7D+%3A%3A+%5B%5Cmathit%7BSymbol%7D%5D+%5Crightarrow+%5B%5Cmathit%7BInteger%7D%5D+%5C%5C+%5Cmathit%7Bencode%7D+%3D+h_1%5C%3Bl+%5Ccdot+%5Cmathit%7Breverse%7D+%5Cqquad+%5Cmathbf%7Bwhere%7D+%5C%5C+%5Cqquad+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dll%7D+h_1%5C%3Bx%5C%3B%28s%3A%5Cmathit%7Bss%7D%27%29+%26+%3D+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dll%7D+%5Cmathbf%7Bif%7D+%26+x+%3C+b+%5Ctimes+%28l+%5Cmathbin%7B%5Cunderline%7B%5Csmash%7B%5Cmathit%7Bdiv%7D%7D%7D%7D+%5Cmathit%7Btotal%7D%29+%5Ctimes+%5Cmathit%7Bcount%7D%5C%3Bs+%5C%5C+%5Cmathbf%7Bthen%7D+%26+%5Cmathbf%7Blet%7D%5C%3B+%28q%2Cr%29+%3D+%5Cmathit%7BdivMod%7D%5C%3Bx%5C%3B%28%5Cmathit%7Bcount%7D%5C%3Bs%29+%5C%3B%5Cmathbf%7Bin%7D%5C%3B+h_1%5C%3B%28q+%5Ctimes+total+%2B+%5Cmathit%7Bcumul%7D%5C%3Bs+%2B+r%29%5C%3B%5Cmathit%7Bss%7D%27+%5C%5C+%5Cmathbf%7Belse%7D+%26+%5Cmathbf%7Blet%7D%5C%3B+%28q%2Cr%29+%3D+%5Cmathit%7Bextract%7D%5C%3Bx+%5C%3B%5Cmathbf%7Bin%7D%5C%3B+r+%3A+h_1%5C%3Bq%5C%3B%28s%3A%5Cmathit%7Bss%7D%27%29+%5Cend%7Barray%7D+%5C%5C+h_1%5C%3Bx%5C%3B%5B%5C%2C%5D+%26+%3D+h_2%5C%3Bx+%5C%5C+h_2%5C%3Bx+%26+%3D+%5Cmathbf%7Bif%7D%5C%3B+x%3D%3D0+%5C%3B%5Cmathbf%7Bthen%7D%5C%3B+%5B%5C%2C%5D+%5C%3B%5Cmathbf%7Belse%7D%5C%3B%5Cmathbf%7Blet%7D%5C%3B+%28q%2Cr%29+%3D+%5Cmathit%7Bextract%7D%5C%3Bx+%5C%3B%5Cmathbf%7Bin%7D%5C%3B+r+%3A+h_2%5C%3Bq+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{encode} :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode} = h_1\;l \cdot \mathit{reverse} \qquad \mathbf{where} \\ \qquad \begin{array}[t]{@{}ll} h_1\;x\;(s:\mathit{ss}') & = \begin{array}[t]{@{}ll} \mathbf{if} & x < b \times (l \mathbin{\underline{\smash{\mathit{div}}}} \mathit{total}) \times \mathit{count}\;s \\ \mathbf{then} & \mathbf{let}\; (q,r) = \mathit{divMod}\;x\;(\mathit{count}\;s) \;\mathbf{in}\; h_1\;(q \times total + \mathit{cumul}\;s + r)\;\mathit{ss}' \\ \mathbf{else} & \mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; r : h_1\;q\;(s:\mathit{ss}') \end{array} \\ h_1\;x\;[\,] & = h_2\;x \\ h_2\;x & = \mathbf{if}\; x==0 \;\mathbf{then}\; [\,] \;\mathbf{else}\;\mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; r : h_2\;q \end{array} \end{array}")
![\displaystyle \begin{array}{@{}l} \mathit{decode} :: [\mathit{Integer}] \rightarrow [\mathit{Symbol}] \\ \mathit{decode} = h_0\;0 \cdot \mathit{reverse} \qquad \mathbf{where} \\ \qquad \begin{array}{@{}lll} h_0\;x\;(y:\mathit{ys}) & \mid x < l & = h_0\;(\mathit{inject}\;x\;y)\;\mathit{ys} \\ h_0\;x\;\mathit{ys} && = h_1\;x\;\mathit{ys} \\ h_1\;x\;\mathit{ys} && = \begin{array}[t]{@{}ll} \mathbf{let} & \begin{array}[t]{@{}ll} (q,r) & = \mathit{divMod}\;x\;\mathit{total} \\ s & = \mathit{find}\;r \\ x' & = \mathit{count}\;s \times q + r - \mathit{cumul}\;s \end{array} \\ \mathbf{in} & h_2\;s\;x'\;\mathit{ys} \end{array} \\ h_2\;s\;x\;(y:\mathit{ys}) & \mid x < l & = h_2\;s\;(\mathit{inject}\;x\;y)\;\mathit{ys} \\ h_2\;s\;x\;\mathit{ys} & \mid x \ge l & = s : h_1\;x\;\mathit{ys} \\ h_2\;s\;x\;[\,] && = [\,] \end{array} \end{array}](https://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7B%40%7B%7Dl%7D+%5Cmathit%7Bdecode%7D+%3A%3A+%5B%5Cmathit%7BInteger%7D%5D+%5Crightarrow+%5B%5Cmathit%7BSymbol%7D%5D+%5C%5C+%5Cmathit%7Bdecode%7D+%3D+h_0%5C%3B0+%5Ccdot+%5Cmathit%7Breverse%7D+%5Cqquad+%5Cmathbf%7Bwhere%7D+%5C%5C+%5Cqquad+%5Cbegin%7Barray%7D%7B%40%7B%7Dlll%7D+h_0%5C%3Bx%5C%3B%28y%3A%5Cmathit%7Bys%7D%29+%26+%5Cmid+x+%3C+l+%26+%3D+h_0%5C%3B%28%5Cmathit%7Binject%7D%5C%3Bx%5C%3By%29%5C%3B%5Cmathit%7Bys%7D+%5C%5C+h_0%5C%3Bx%5C%3B%5Cmathit%7Bys%7D+%26%26+%3D+h_1%5C%3Bx%5C%3B%5Cmathit%7Bys%7D+%5C%5C+h_1%5C%3Bx%5C%3B%5Cmathit%7Bys%7D+%26%26+%3D+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dll%7D+%5Cmathbf%7Blet%7D+%26+%5Cbegin%7Barray%7D%5Bt%5D%7B%40%7B%7Dll%7D+%28q%2Cr%29+%26+%3D+%5Cmathit%7BdivMod%7D%5C%3Bx%5C%3B%5Cmathit%7Btotal%7D+%5C%5C+s+%26+%3D+%5Cmathit%7Bfind%7D%5C%3Br+%5C%5C+x%27+%26+%3D+%5Cmathit%7Bcount%7D%5C%3Bs+%5Ctimes+q+%2B+r+-+%5Cmathit%7Bcumul%7D%5C%3Bs+%5Cend%7Barray%7D+%5C%5C+%5Cmathbf%7Bin%7D+%26+h_2%5C%3Bs%5C%3Bx%27%5C%3B%5Cmathit%7Bys%7D+%5Cend%7Barray%7D+%5C%5C+h_2%5C%3Bs%5C%3Bx%5C%3B%28y%3A%5Cmathit%7Bys%7D%29+%26+%5Cmid+x+%3C+l+%26+%3D+h_2%5C%3Bs%5C%3B%28%5Cmathit%7Binject%7D%5C%3Bx%5C%3By%29%5C%3B%5Cmathit%7Bys%7D+%5C%5C+h_2%5C%3Bs%5C%3Bx%5C%3B%5Cmathit%7Bys%7D+%26+%5Cmid+x+%5Cge+l+%26+%3D+s+%3A+h_1%5C%3Bx%5C%3B%5Cmathit%7Bys%7D+%5C%5C+h_2%5C%3Bs%5C%3Bx%5C%3B%5B%5C%2C%5D+%26%26+%3D+%5B%5C%2C%5D+%5Cend%7Barray%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{@{}l} \mathit{decode} :: [\mathit{Integer}] \rightarrow [\mathit{Symbol}] \\ \mathit{decode} = h_0\;0 \cdot \mathit{reverse} \qquad \mathbf{where} \\ \qquad \begin{array}{@{}lll} h_0\;x\;(y:\mathit{ys}) & \mid x < l & = h_0\;(\mathit{inject}\;x\;y)\;\mathit{ys} \\ h_0\;x\;\mathit{ys} && = h_1\;x\;\mathit{ys} \\ h_1\;x\;\mathit{ys} && = \begin{array}[t]{@{}ll} \mathbf{let} & \begin{array}[t]{@{}ll} (q,r) & = \mathit{divMod}\;x\;\mathit{total} \\ s & = \mathit{find}\;r \\ x' & = \mathit{count}\;s \times q + r - \mathit{cumul}\;s \end{array} \\ \mathbf{in} & h_2\;s\;x'\;\mathit{ys} \end{array} \\ h_2\;s\;x\;(y:\mathit{ys}) & \mid x < l & = h_2\;s\;(\mathit{inject}\;x\;y)\;\mathit{ys} \\ h_2\;s\;x\;\mathit{ys} & \mid x \ge l & = s : h_1\;x\;\mathit{ys} \\ h_2\;s\;x\;[\,] && = [\,] \end{array} \end{array}")
