Total Combinations
Here’s a quick puzzle: from a finite alphabet, produce an infinite list of infinite strings, each of them unique.
It’s not a super hard problem, but here are some examples of what you
might get. Given the alphabet of 0
and 1
, for
instance, you could produce the following:
0000000...
1000000...
0100000...
1100000...
0010000...
1010000...
0110000...
1110000...
0001000...
In other words, the enumeration of the binary numbers (leastsignificantdigit first). We’ll just deal with bits first:
data Bit = O  I
instance Show Bit where
showsPrec _ O = (:) '0'
showsPrec _ I = (:) '1'
showList xs s = foldr f s xs
where
O a = '0' : a
f I a = '1' : a f
Thinking recursively, we can see that the tail of each list is actually the original sequence, doubledup:
0000000...
1000000...
0100000...
1100000...
0010000...
1010000...
0110000...
1110000...
0001000...
As it happens, we get something like this pattern with the monad instance for lists anyway:
>>> (,) <$> [O,I] <*> "abc"
0,'a'),(0,'b'),(0,'c'),(1,'a'),(1,'b'),(1,'c')] [(
Well, actually it’s the wrong way around. We want to loop through the
first list the quickest, incrementing the second slower. No
worries, we can just use a flipped version of
<*>
:
infixl 4 <<>
(<<>) :: Applicative f => f (a > b) > f a > f b
<<> xs = flip ($) <$> xs <*> fs
fs
>>> (,) <$> [O,I] <<> "abc"
0,'a'),(1,'a'),(0,'b'),(1,'b'),(0,'c'),(1,'c')] [(
Brilliant! So we can write our function now, yes?
= (:) <$> [O,I] <<> bins bins
Nope! That won’t ever produce an answer, unfortunately.
Productivity
The issue with our definition above is that it’s not lazy enough: it demands information that it hasn’t produced yet, so it gets caught in an infinite loop before it can do anything!
We need to kickstart it a little, so it can produce output before it asks itself for more. Because we know what the first line is going to be, we can just tell it that:
= (:) <$> [O,I] <<> (repeat O : tail bins)
bins
>>> mapM_ print (take 8 (map (take 3) bins))
000
100
010
110
001
101
011
111
The property that this function has that the previous didn’t is
productivity: the dual of termination. See, we want to avoid a
kind of infinite loops in bins
, but we don’t want
to avoid infinite things altogether: the list it produces is meant to be
infinite, for goodness’ sake. Instead, what it needs to do is produce
every new value in finite time.
Checking Productivity
In total languages, like Agda, termination checking is a must. To express computation like that above, though, you often also want a productivity checker. Agda can do that, too.
Let’s get started then. First, a stream:
infixr 5 _◂_
record Stream {a} (A : Set a) : Set a where
coinductive
constructor _◂_
field
: A
head : Stream A
tail open Stream
In Haskell, there was no need to define a separate stream type: the type of lists contains both finite and infinite lists.
Agda can get a little more specific: here, we’ve used the
coinductive
keyword, which means we’re free to create
infinite Stream
s. Rather than the usual termination
checking (which would kick in when we consume a recursive, inductive
type), we now get productivity checking: when creating a
Stream
, the tail
must always be available in
finite time. For a finite type, we’d have used the
inductive
keyword instead; this wouldn’t be much use,
though, since there’s no way to create a finite Stream
without a nil constructor!^{1}
One of the interesting things about working with infinite data (when you’re forced to notice that it’s infinite, as you are in Agda) is that everything gets flipped. So you have to prove productivity, not totality; you use product types, rather than sums; and to define functions, you use copatterns, rather than patterns.
Copatterns
Copatterns are a handy syntactic construct for writing functions about record types. Let’s start with an example, and then I’ll try explain a little:
: ∀ {a} {A : Set a} → A → Stream A
pure (pure x) = x
head (pure x) = pure x tail
Here, we’re defining pure
on streams:
pure x
produces an infinite stream of x
. Its
equivalent would be repeat in Haskell:
repeat :: a > [a]
repeat x = x : repeat x
Except instead of describing what it is, you describe how it
acts (it’s kind of an intensional vs. extensional thing). In
other words, if you want to make a stream xs
, you have to
answer the questions “what’s the head of xs
?” and “what’s
the tail of xs
?”
Contrast this with patternmatching: we’re producing (rather than
consuming) a value, and in pattern matching, you have to answer a
question for each case. If you want to consume a list
xs
, you have to answer the questions “what do you do when
it’s nil?” and “what do you do when it’s cons?”
Anyway, I think the symmetry is kind of cool. Let’s get back to writing our functions.
Sized Types
Unfortunately, we don’t have enough to prove productivity yet. As an
explanation why, let’s first try produce the famous fibs
list. Written here in Haskell:
= 0 : 1 : zipWith (+) fibs (tail fibs) fibs
Instead of zipWith
, let’s define <*>
.
That will let us use idiom
brackets.
_<*>_ : ∀ {a b} {A : Set a} {B : Set b}
→ Stream (A → B)
→ Stream A
→ Stream B
(fs <*> xs) = head fs (head xs)
head (fs <*> xs) = tail fs <*> tail xs tail
And here’s fibs
:
: Stream ℕ
fibs = 0
head fibs (tail fibs) = 1
head (tail fibs) = ⦇ fibs + tail fibs ⦈ tail
But it doesn’t pass the productivity checker! Because we use a
higherorder function (<*>
), Agda won’t look at how
much it dips into the infinite supply of values. This is a problem: we
need it to know that <*>
only needs the heads of its
arguments to produce a head, and so on. The solution? Encode this
information in the types.
infixr 5 _◂_
record Stream {i : Size} {a} (A : Set a) : Set a where
coinductive
constructor _◂_
field
: A
head : ∀ {j : Size< i} → Stream {j} A
tail open Stream
Now, Stream
has an implicit size parameter.
Basically, Stream {i} A
can produce i
more
values. So cons
, then, gives a stream one extra value to
produce:
: ∀ {i a} {A : Set a} → A → Stream {i} A → Stream {↑ i} A
cons (cons x xs) = x
head (cons x xs) = xs tail
Conversely, we can write a different definition of tail
that consumes one value^{2}:
: ∀ {i a} {A : Set a} → Stream {↑ i} A → Stream {i} A
tail′ {i} xs = tail xs {i} tail′
For <*>
, we want to show that its result can
produce just as much values as its inputs can:
_<*>_ : ∀ {i a b} {A : Set a} {B : Set b}
→ Stream {i} (A → B)
→ Stream {i} A
→ Stream {i} B
(fs <*> xs) = head fs (head xs)
head (fs <*> xs) = tail fs <*> tail xs tail
How does this help the termination/productivity checker? Well, for
terminating functions, we have to keep giving the tail
field smaller and smaller sizes, meaning that we’ll eventually hit zero
(and terminate). For productivity, we now have a way to talk about
“definedness” in types, so we can make sure that a recursive call
doesn’t dip into a supply it hasn’t produced yet.
One more thing: Size
types have strange typing rules,
mainly for ergonomic purposes (this is why we’re not just using an
ℕ
parameter). One of them is that if you don’t specify the
size, it’s defaulted to ∞
, so functions written without
size annotations don’t have to be changed with this new definition:
: ∀ {a} {A : Set a} → A → Stream A
pure (pure x) = x
head (pure x) = pure x tail
Finally fibs
:
: ∀ {i} → Stream {i} ℕ
fibs = 0
head fibs (tail fibs) = 1
head (tail fibs) = ⦇ fibs + tail fibs ⦈ tail
Bugs!
Before I show the Agda solution, I’d like to point out some bugs that were revealed in the Haskell version by trying to implement it totally. First of all, the function signature. “Takes an alphabet and produces unique strings” seems like this:
strings :: [a] > [[a]]
But what should you produce in this case:
strings []
So it must be a nonempty list, giving us the following type and definition:
strings :: NonEmpty a > [[a]]
: xs) = (:) <$> (x:xs) <<> (repeat x : tail (strings (x : xs))) strings (x
But this has a bug too! What happens if we pass in the following:
: []) strings (x
So this fails the specification: there is only one unique infinite
string from that alphabet (pure x
). Interestingly, though,
our implementation above also won’t produce any output beyond the first
element. I suppose, in a way, these things cancel each other out: our
function does indeed produce all of the unique strings, it’s just a pity
that it goes into an infinite loop to do so!
Bringing it all Together
Finally, we have our function:
: ∀ {i a} {A : Set a} → A × A × List A → Stream {i} (Stream A)
strings (strings (x , _ , _)) = pure x
head (strings {A = A} xs@(x₁ , x₂ , xt)) = go x₂ xt (strings xs)
tail where
: ∀ {i} → A → List A → Stream {i} (Stream A) → Stream {i} (Stream A)
go (head (go y ys zs)) = y
head (head (go y ys zs)) = head zs
tail (go _ [] zs) = go x₁ (x₂ ∷ xt) (tail zs)
tail (go _ (y ∷ ys) zs) = go y ys zs tail
As you can see, we do need to kickstart it without a recursive call
(the first line is pure x
). Then, go
takes as
a third argument the “tails” argument, and does the kind of backwards
Cartesian product we want. However, since we’re into the second element
of the stream now, we want to avoid repeating what we already said,
which is why we have to give go
x₂
, rather
than x₁
. This is what forces us to take at least two
elements, rather than at least one, also: we can’t just take the tail of
the call to go
(this is what we did in the Haskell version
of strings
with the NonEmpty
list), as the
recursive call to strings then doesn’t decrease in size:
: ∀ {i a} {A : Set a} → A × List A → Stream {i} (Stream A)
strings (strings (x , _)) = pure x
head (strings {A = A} xs@(x , xt)) = tail (go x xt (strings xs))
tail where
: ∀ {i} → A → List A → Stream {i} (Stream A) → Stream {i} (Stream A)
go (head (go y ys zs)) = y
head (head (go y ys zs)) = head zs
tail (go _ [] zs) = go x xt (tail zs)
tail (go _ (y ∷ ys) zs) = go y ys zs tail
Agda will warn about termination on this function. Now, if you slap a pragma on it, it will produce the correct results for enough arguments, but give it one and you’ll get an infinite loop, just as you were warned!
Further Work
I’m having a lot of fun with copatterns for various algorithms (especially combinatorics). I’m planning on working on two particular tasks with them for the next posts in this series:
 Proving
strings

I’d like to prove that
strings
does indeed produce a stream of unique values. Following from that, it would be cool to do a Cantor diagonalisation on its output.  Permutations

Haskell’s permutations implementation in Data.List does some interesting tricks to make it as lazy as possible. It would be great to write an implementation that is verified to be as lazy as possible: the pattern of “definedness” is complex, though, so I don’t know if it’s possible with Agda’s current sized types.
Thanks to gelisam for pointing out the poor phrasing here. Updated on 2018/10/16↩︎
You might wonder why the definition of
tail
doesn’t have this signature to begin with. The reason is that our record type must be parameterized (not indexed) over its size (as it’s a record type), so we use a lessthan proof instead.↩︎