Self-publishing my first book

It all started in 2013, when one of my former coworkers told me about this weird mathematical programming language called Haskell. I already had an interest in mathematics, so it didn’t take long before I started looking into it. I visited the awesome community on Freenode and was suggested to read Learn You a Haskell for Great Good.

I was amazed by both the book and the language. I started to blog about the things I learned. Algebraic data types eventually turned out to be my bachelor thesis in 2015. As the number of blog posts kept increasing, I thought of writing a book on dependent types. I collected all the blog posts, edited them, put them in a logical order and asked some friends to review the chapters. Finally, in September 2018 I self-published my first book, Gentle Introduction to Dependent Types with Idris.

My book has exceeded the sales expectations I had. I didn’t do any paid marketing at all. The only marketing was maybe doing a few posts on social media. It was a great experience for me, my writing skills improved, and I learned a lot about books, reading, and writing, receiving feedback.

Here’s a summary of what I’ve learned during the process:

Receive feedback as early as possible – what makes sense to you does not necessarily make sense to all readers. I found reviewers by pinging some friends and googling for bloggers interested in the same topic. Reviewers’ feedback is very valuable. It is important to keep low ego and revise parts that really suck, but it needs to work both ways – reviewers must be providing constructive criticism
Writing a book is harder than blogging (it requires logical flow, every paragraph needs to have context similar to previous, etc). Putting thoughts randomly on a blog is OK but a book has to have a kind of structure. Writing, in general, is hard and requires a lot of patience
I didn’t know everything when I started writing the book – only some parts. I found it’s interesting and fun to learn as you go – you eventually become an “expert” in the field
Grammar – keep simple statements, active voice, paragraphs, etc
Continuously read and revise

For the writing process, I started copying and pasting my blog contents to a Google Drive document and shared it with the reviewers. After a while, I found out about Leanpub, and moved all of the content to a GitHub repository using Leanpub’s extended Markdown which also supports LaTeX. Reviewers would then either create GitHub issues or pull requests. Leanpub allows you to export your book as a pdf/mobi/epub format. It also allows exporting of a so-called “print book” format, so I could build my book with a few clicks and upload it to Amazon’s Kindle Direct Publishing service. I also used Grammarly and aspell.

It was interesting to me how writing a book in today’s age is very simple with all the tools that are available to us.

I’m thankful to my family, the reviewers, my former and current coworkers, and everybody else directly or indirectly involved.

CoC base terms – Type and Prop

In mathematics, a judgement is a logical statement in the meta language
An inference rule means that for a given list of judgements $J_1, J_2, \ldots, J_n$ , we can infer that $J$ , which we denote as $\frac{J_1, J_2, \ldots, J_N}{J}$
Calculus of Constructions is a type theory based on intuitionistic logic.

If 1 and 2 don’t make much sense, I found this picture on Twitter to be useful:

For $K$ being either $\text{Type}$ or $\text{Prop}$ , Calculus of Constructions has the following inference rule:

${\Gamma \ \vdash A \ : \ K \over {\Gamma, \ x:A \ \vdash \ x:A}}$

What this rule means is that $x$ can only be of type $A$ , if $A$ is of type $\text{Type}$ , or $A$ is of type $\text{Prop}$ .

The questions that I had were:

What are the (dis)advantages of limiting $A$ to be $K$ ?
Alternatively, what are the (dis)advantages of allowing infinite subtyping (allowing terms to be used as types)?
Why do we have these base types $\text{Type}$ and $\text{Prop}$ ?

First of all, we can already “emulate” something like “infinite subtyping” in Coq. For example, to “construct” foo : 3 : Nat : Type we can implement F : nat -> Type, then we have that F 3 : Type. Further, we can implement F' : F 3 -> Type, so F' foo is possible. It’s still of type Type but it kinda works.

But, what happens if we lift this restriction? Well that’s not an easy thing to do. At the very least we need some kind of well-formedness condition in place of $A : K$ , otherwise we can get judgements like $x : (\text{true} + 0) \ \vdash \ x : (\text{true} + 0)$ . So plainly lifting that restriction not only allows arbitrary terms that are not types, it even allows ill-typed terms which do not type-check.

So foo : 3 : Nat : Type kind of makes no sense. To the left, we have the values we actually compute on; types classify those, and can in turn be classified. In other words, a : b means that a is an element of the “collection” b, but some of these elements are not collections.

So the reason why we have types/values distinction is computation and we can’t really bring them at the “same” level, even though dependent types try to blur the line between the two. We can have values in types, and types in values, but there’s still a difference.

This is why that judgement rule is so important 🙂

As usual, somebody had already considered this 🙂 I started a discussion on #coq@freenode and ##dependent@freenode and got some great answers. Thanks to pgiarrusso, lyxia, and mietek.

If—

If you can keep your head when all about you
Are losing theirs and blaming it on you,
If you can trust yourself when all men doubt you,
But make allowance for their doubting too.
If you can wait and not be tired by waiting,
Or being lied about, don’t deal in lies,
Or being hated, don’t give way to hating,
And yet don’t look too good, nor talk too wise:

If you can dream—and not make dreams your master;
If you can think—and not make thoughts your aim;
If you can meet with Triumph and Disaster,
And treat those two impostors just the same;
If you can bear to hear the truth you’ve spoken
Twisted by knaves to make a trap for fools,
Or watch the things you gave your life to, broken,
And stoop and build ’em up with worn-out tools:

If you can make a heap of all your winnings
And risk it on one turn of pitch-and-toss,
And lose, and start again at your beginnings
And never breathe a word about your loss;
If you can force your heart and nerve and sinew
To serve your turn long after they are gone,
And so hold on when there is nothing in you
Except the Will which says to them: “Hold on!”

If you can talk with crowds and keep your virtue,
Or walk with Kings—nor lose the common touch,
If neither foes nor loving friends can hurt you,
If all men count with you, but none too much;
If you can fill the unforgiving minute
With sixty seconds’ worth of distance run,
Yours is the Earth and everything that’s in it,
And—which is more—you’ll be a Man, my son!

Rudyard Kipling, 1910

Proving Monoids with Idris

I was watching an interesting video, Opening Keynote by Edward Kmett at Lambda World 2018. Note in the beginning of that video how in Haskell you’d put code comments in place of proofs.

Enter Idris.

As a short example, we can abstract a proven Monoid as an interface:

interface ProvenMonoid m where
	mappend : m -> m -> m
	mempty  : m
	assocProof : (a, b, c : m) -> mappend a (mappend b c) = mappend (mappend a b) c
	idProofL   : (a : m) -> mappend mempty a = a
	idProofR   : (a : m) -> mappend a mempty = a

Do Nats make a Monoid? Sure they do, and here’s the proof for that:

implementation ProvenMonoid Nat where
	mappend x y = x + y
	mempty      = 0

	-- Proofs that this monoid is really a monoid.
	assocProof  = plusAssociative
	idProofL    = plusZeroLeftNeutral
	idProofR    = plusZeroRightNeutral

Note that plusAssociative, plusZeroLeftNeutral, and plusZeroRightNeutral are already part of Idris’ prelude. In the next example we’ll do an actual proof ourselves instead of re-using existing proofs.

What about List of Nats? Yep.

implementation ProvenMonoid (List Nat) where
	mappend x y = x ++ y
	mempty      = []

	-- Proofs that this monoid is really a monoid.
	assocProof [] b c      = Refl
	assocProof (a::as) b c = rewrite assocProof as b c in Refl
	idProofL a             = Refl
	idProofR []            = Refl
	idProofR (x::xs)       = rewrite idProofR xs in Refl

Some valid questions are:

Why should I care about monoids?
- Edward covers this in the video at around 3:00.
Why should I care about proving monoids?
- Let’s assume that there’s an algorithm running in production that relies on Monoids. What we don’t want to happen is associativity to break, because if it does then the “combine” function applied on all of the produced results will likely be wrong.

🙂

EDIT: Updated first example per u/gallais’s comment.

Partial orders in Idris

A binary relation $R$ is a partial order if the following properties are satisfied:

Reflexivity, i.e. $\forall a, a R a$
Transitivity, i.e. $\forall a, b, c, a R b \land b R c \to a R c$
Antisymmetry, i.e. $\forall a, b, a R b \land b R a \to a = b$

Let’s abstract this in Idris as an interface:

interface PartialOrder (a : Type) (Order : a -> a -> Type) | Order where
    total proofReflexive     : Order n n
    total proofTransitive    : Order n m -> Order m p -> Order n p
    total proofAntisymmetric : Order n m -> Order m n -> n = m

The interface PartialOrder accepts a Type and a relation Order on it. Since the interface has more than two parameters, we specify that Order is a determining parameter (the parameter used to resolve the instance). Each function definition corresponds to the properties above.

This interface is too abstract as it is, so let’s build a concrete implementation for it:

implementation PartialOrder Nat LTE where
    proofReflexive {n = Z}   = LTEZero
    proofReflexive {n = S _} = LTESucc proofReflexive

    proofTransitive LTEZero           _                 = LTEZero
    proofTransitive (LTESucc n_lte_m) (LTESucc m_lte_p) = LTESucc (proofTransitive n_lte_m m_lte_p)

    proofAntisymmetric LTEZero           LTEZero           = Refl
    proofAntisymmetric (LTESucc n_lte_m) (LTESucc m_lte_n) = let IH = proofAntisymmetric n_lte_m m_lte_n in rewrite IH in Refl

Now you can go and tell your friends that the data type LTE on Nats makes a partial order 🙂