Category: theory

The basics of coinduction

I don’t remember when I first heard the terms “coinduction” and “corecursion” but it must have been quite long ago. I had this impression that they are yet another of these difficult theoretical concepts and that I should learn about them one day. That “one day” happened recently while reading chapter 5 of “Certified Programming with Dependent Types”. It turns out that basics of coinduction are actually quite simple. In this post I’ll share with you what I already know on the subject.

Recursion in Haskell

Let’s begin with looking at Haskell because it is a good example of language not formalizing coinduction in any way. Two features of Haskell are of interest to us. First one is laziness. Thanks to Haskell being lazy we can write definitions like these (in GHCi):

ghci> let ones = 1 : ones
ghci> let fib = zipWith (+) (1:fib) (1:1:fib)

ones is – as the name implies – an infinite sequence (list) of ones. fib is a sequence of Fibonacci numbers. Both these definitions produce infinite lists but we can use these definitions safely because laziness allows us to force a finite number of elements in the sequence:

ghci> take 5 ones
[1,1,1,1,1]
ghci> take 10 fib
[2,3,5,8,13,21,34,55,89,144]

Now consider this definition:

ghci> let inf = 1 + inf

No matter how hard we try there is no way to use the definition of inf in a safe way. It always causes an infinite loop:

ghci> (0 /= inf)
*** Exception: <<loop>>

The difference between definitions of ones or fib an the definition of inf is that the former use something what is called a guarded recursion. The term guarded comes from the fact that recursive reference to self is hidden under datatype constructor (or: guarded by a constructor). The way lazy evaluation is implemented gives a guarantee that we can stop the recursion by not evaluating the recursive constructor argument. This kind of infinite recursion can also be called productive recursion, which means that although recursion is infinite each recursive call is guaranteed to produce something (in my examples either a 1 or next Fibonacci number). By contrast recursion in the definition of inf is not guarded or productive in any way.

Haskell happily accepts the definition of inf even though it is completely useless. When we write Haskell programs we of course don’t want them to fall into silly infinite loops but the only tool we have to prevent us from writing such code is our intelligence. Situation changes when it comes to….

Dependently-typed programming languages

These languages deeply care about termination. By “termination” I mean ensuring that a program written by the user is guaranteed to terminate for any input. I am aware of two reasons why these languages care about termination. First reason is theoretical: without termination the resulting language is inconsistent as logic. This happens because non-terminating term can prove any proposition. Consider this non-terminating Coq definition:

Fixpoint evil (A : Prop) : A := evil A.

If that definition was accepted we could use it to prove any proposition. Recall that when it comes to viewing types as proofs and programs as evidence “proving a proposition” means constructing a term of a given type. evil would allow to construct a term inhabiting any type A. (Prop is a kind of logical propositions so A is a type.) Since dependently-typed languages aim to be consistent logics they must reject non-terminating programs. Second reason for checking termination is practical: dependently typed languages admit functions in type signatures. If we allowed non-terminating functions then typechecking would also become non-terminating and again this is something we don’t want. (Note that Haskell gives you UndecidableInstances that can cause typechecking to fall into an infinite loop).

Now, if you paid attention on your Theoretical Computer Science classes all of this should ring a bell: the halting problem! The halting problem says that the problem of determining whether a given Turing machine (read: a given computer program) will ever terminate is undecidable. So how is that possible that languages like Agda, Coq or Idris can answer that question? That’s simple: they are not Turing-complete (or at least their terminating subsets are not Turing complete). (UPDATE: but see Conor McBride’s comment below.) They prohibit user from using some constructs, probably the most important one being general recursion. Think of general recursion as any kind of recursion imaginable. Dependently typed languages require structural recursion on subterms of the arguments. That means that if a function receives an argument of an inductive data type (think: algebraic data type/generalized algebraic data type) then you can only make recursive calls on terms that are syntactic subcomponents of the argument. Consider this definition of map in Idris:

map : (a -> b) -> List a -> List b
map f []      = []
map f (x::xs) = f x :: map f xs

In the second equation we use pattern matching to deconstruct the list argument. The recursive call is made on xs, which is structurally smaller then the original argument. This guarantees that any call to map will terminate. There is a silent assumption here that the List A argument passed to map is finite, but with the rules given so far it is not possible to construct infinite list.

So we just eliminated non-termination by limiting what can be done with recursion. This means that our Haskell definitions of ones and fib would not be accepted in a dependently-typed language because they don’t recurse on an argument that gets smaller and as a result they construct an infinite data structure. Does that mean we are stuck with having only finite data structures? Luckily, no.

Coinduction to the rescue

Coinduction provides a way of defining and operating on infinite data structures as long as we can prove that our operations are safe, that is they are guarded and productive. In what follows I will use Coq because it seems that it has better support for coinduction than Agda or Idris (and if I’m wrong here please correct me).

Coq, Agda and Idris all require that a datatype that can contain infinite values has a special declaration. Coq uses CoInductive keyword instead of Inductive keyword used for standard inductive data types. In a similar fashion Idris uses codata instead of data, while Agda requires ∞ annotation on a coinductive constructor argument.

Let’s define a type of infinite nat streams in Coq:

CoInductive stream : Set :=
| Cons : nat -> stream -> stream.

I could have defined a polymorphic stream but for the purpose of this post stream of nats will do. I could have also defined a Nil constructor to allow finite coinductive streams – declaring data as coinductive means it can have infinite values, not that it must have infinite values.

Now that we have infinite streams let’s revisit our examples from Haskell: ones and fib. ones is simple:

CoFixpoint ones : stream := Cons 1 ones.

We just had to use CoFixpoint keyword to tell Coq that our definition will be corecursive and it is happily accepted even though a similar recursive definition (ie. using Fixpoint keyword) would be rejected. Allow me to quote directly from CPDT:

whereas recursive definitions were necessary to use values of recursive inductive types effectively, here we find that we need co-recursive definitions to build values of co-inductive types effectively.

That one sentence pins down an important difference between induction and coinduction.

Now let’s define zipWith and try our second example fib:

CoFixpoint zipWith (f : nat -> nat -> nat) (a : stream)
                   (b : stream) : stream :=
  match a, b with
    | Cons x xs, Cons y ys => Cons (f x y) (zipWith f xs ys)
  end.
 
CoFixpoint fib : stream :=
   zipWith plus (Cons 1 fib) (Cons 1 (Cons 1 fib)).

Unfortunately this definition is rejected by Coq due to “unguarded recursive call”. What exactly goes wrong? Coq requires that all recursive calls in a corecursive definition are:

  1. direct arguments to a data constructor
  2. not inside function arguments

Our definition of fib violates the second condition – both recursive calls to fib are hidden inside arguments to zipWith function. Why does Coq enforce such a restriction? Consider this simple example:

Definition tl (s : stream) : stream :=
  match s with
    | Cons _ tl' => tl'
  end.
 
CoFixpoint bad : stream := tl (Cons 1 bad).

tl is a standard tail function that discards the first element of a stream and returns its tail. Just like our definition of fib the definition of bad places the corecursive call inside a function argument. I hope it is easy to see that accepting the definition of bad would lead to non-termination – inlining definition of tl and simplifying it leads us to:

CoFixpoint bad : stream := bad.

and that is bad. You might be thinking that the definition of bad really has no chance of working whereas our definition of fib could in fact be run safely without the risk of non-termination. So how do we persuade Coq that our corecursive definition of fib is in fact valid? Unfortunately there seems to be no simple answer. What was meant to be a simple exercise in coinduction turned out to be a real research problem. This past Monday I spent well over an hour with my friend staring at the code and trying to come up with a solution. We didn’t find one but instead we found a really nice paper “Using Structural Recursion for Corecursion” by Yves Bertot and Ekaterina Komendantskaya. The paper presents a way of converting definitions like fib to a guarded and productive form accepted by Coq. Unfortunately the converted definition looses the linear computational complexity of the original definition so the conversion method is far from perfect. I encourage to read the paper. It is not long and is written in a very accessible way. Another set of possible solutions is given in chapter 7 of CPDT but I am very far from labelling them as “accessible”.

I hope this post demonstrates that basics ideas behind coinduction are actually quite simple. For me this whole subject of coinduction looks really fascinating and I plan to dive deeper into it. I already have my eyes set on several research papers about coinduction so there’s a good chance that I’ll write more about it in future posts.

Data is evidence

Recently I’ve been reading “Types and Programming Langauages” book by Benjamin C. Pierce. It’s a great introduction to theory behind type systems of both functional and object-oriented languages. In the first chapter there’s this really brilliant sentence that says what a type system does:

A type system can be regarded as calculating a kind of static approximation to the run-time behaviours of the terms in a program.

So if a type system is a static approximation of program’s behaviour at runtime a natural question to ask is: “how accurate this approximation can be?” Turns out it can be very accurate.

Let’s assume that we have following definition of natural numbers1:

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

First constructor – zero – says that zero is a natural number. Second – suc – says that successor of any natural number is also a natural number. This representation allows to encode 0 as zero, 1 as suc zero, 2 as suc (suc zero) and so on2. Let’s also define a type of booleans to represent logical true and false:

data Bool : Set where
  false : Bool
  true  : Bool

We can now define a operator that returns true if its arguments are in greater-equal relation and false if they are not:

__ : Nat → Nat → Bool
m     ≥ zero  = true
zero  ≥ suc n = false
suc m ≥ suc n = m ≥ n

This definition has three cases. First says that any natural number is greater than or equal to zero. Second says that zero is not greater than any successor. Final case says that two non-zero natural numbers are in ≥ relation if their predecessors are also in that relation. What if we replace false with true in our definition?

__ : Nat → Nat → Bool
m     ≥ zero  = true
zero  ≥ suc n = true
suc m ≥ suc n = m ≥ n

Well… nothing. We get a function that has nonsense semantics but other than that it is well-typed. The type system won’t catch this mistake. The reason for this is that our function returns a result but it doesn’t say why that result is true. And since doesn’t give us any evidence that result is correct there is no way of statically checking whether the implementation is correct or not.

But it turns out that we can do better using dependent types. We can write a comparison function that proves its result correct. Let’s forget our definition of and instead define datatype called :

data __ : Nat → Nat → Set where
  ge0 : {  y : Nat}         → y     ≥ zero
  geS : {x y : Nat} → x ≥ y → suc x ≥ suc y

This type has two Nat indices that parametrize it. For example: 5 ≥ 3 and 2 ≥ 0 are two distinct types. Notice that each constructor can only be used to construct values of a specific type: ge0 constructs a value that belongs to types like 0 ≥ 0, 1 ≥ 0, 3 ≥ 0 and so on. geS given a value of type x ≥ y constructs a value of type suc x ≥ suc y.

There are a few interesting properties of datatype. Notice that not only ge0 can construct value of types y ≥ 0, but it is also the only possible value of such types. In other words the only value of 0 ≥ 0, 1 ≥ 0 or 3 ≥ 0 is ge0. Types like 5 ≥ 3 also have only one value (in case of 5 ≥ 3 it is geS (geS (geS ge0))). That’s why we call a singleton type. Note also that there is no way to construct values of type 0 ≥ 3 or 5 ≥ 2 – there are no constructors that we could use to get a value of that type. We will thus say that datatype is a witness (or evidence): if we can construct a value for a given two indices then this value is a witness that relation represented by the datatype holds. For example geS (geS ge0)) is a witness that relations 2 ≥ 2 and 2 ≥ 5 hold but there is no way to provide evidence that 0 ≥ 1 holds. Notice that previous definition of function had three cases: one base case for true, one base case for false and one inductive case. The datatype has only two cases: one being equivalent of true and one inductive. Because the value of exists if and only if its two parameters are in ≥ relation there is no need to represent false explicitly.

We have a way to express proof that one value is greater than another. Let’s now construct a datatype that can say whether one value is greater than another and supply us with a proof of that fact:

data Order : Nat → Nat → Set where
  ge : {x : Nat} {y : Nat} → x ≥ y → Order x y
  le : {x : Nat} {y : Nat} → y ≥ x → Order x y

Order is indexed by two natural numbers. These numbers can be anything – there is no restriction on any of the constructors. We can construct values of Order using one of two constructors: ge and le. Constructing value of Order using ge constructor requires a value of type x ≥ y. In other words it requires a proof that x is greater than or equal to y. Constructing value of Order using le constructor requires the opposite proof – that y ≥ x. Order datatype is equivalent of Bool except that it is specialized to one particular relation instead of being a general statement of truth or false. It also carries a proof of the fact that it states.

Now we can write a function that compares two natural numbers and returns a result that says whether first number is greater than or equal to the second one3:

order : (x : Nat)(y : Nat) → Order x y
order x       zero    = ge ge0
order zero    (suc b) = le ge0
order (suc a) (suc b) with order a b
order (suc a) (suc b) | ge a≥b = ge (geS a≥b)
order (suc a) (suc b) | le b≥a = le (geS b≥a)

In this implementation ge plays the role of true and le plays the role of false. But if we try to replace le with ge the way we previously replaced false with true the result will not be well-typed:

order : (x : Nat)(y : Nat) → Order x y
order x       zero    = ge ge0
order zero    (suc b) = ge ge0 -- TYPE ERROR
order (suc a) (suc b) with order a b
order (suc a) (suc b) | ge a≥b = ge (geS a≥b)
order (suc a) (suc b) | le b≥a = le (geS b≥a)

Why? It is a direct result of the definitions that we used. In the second equation of order, x is zero and y is suc b. To construct a value of Order x y using ge constructor we must provide a proof that x ≥ y. In this case we would have to prove that zero ≥ suc b, but as discussed previously there is no constructor of that could construct value of this type. Thus the whole expression is ill-typed and the incorrectness of our definition is caught at compile time.

Summary

The idea that types can represent logical propositions and values can be viewed as proofs of these propositions is not new – it is known as Curry-Howard correspondence (or isomorphism) and I bet many of you have heard that name. Example presented here is taken from “Why Dependent Types Matter”. See this recent post for a few more words about this paper.

  1. All code in this post is in Agda. []
  2. For the sake of readability I will write Nats as numerals, not as applications of suc and zero. So remember that whenever I write 2 I mean suc (suc zero) []
  3. Note that in Agda a≥b is a valid identifier, not an application of []

The Lambda Papers

I’m reading about functional programming as much as I can. Aside from staying up-to-date with the latest publications I also spend some time reading the older papers. Among the classics are true pearls: John Backus’ “Can Programming Be Liberated from the von Neumann Style. A Functional Style and Its Algebra of Programs” took hours to read but was an eye-opener for me (I think this was the first paper on FP I ever read) and Phil Wadler’s “Comprehending monads” and “The essence of functional programming” are a beautiful demonstration of power and elegance of monads. But today I want to write about The Lambda Papers – a series of approximately 10 papers (mostly AI Lab Memos) written by Guy Steele and Gerald Sussman between 1975 and 1980. I originally heard about them while browsing Lambda The Ultimate (which, by the way, takes its name from these papers).

ltuiLambda papers revolve around the programming language Scheme, a simple dialect of Lisp developed by Steele and Sussman at MIT in the seventies. So far I have read two of these papers – “Lambda: The ultimate imperative” and “Lambda: The ultimate declarative”. The first one discusses the implementation of programming constructs know from imperative languages – for example GOTOs, blocks, assignments, loops or exceptions – in Scheme. Authors demonstrate that lambda expressions, that is anonymous functions, suffice to implement all these imperative constructs. Moreover, they show that using lambdas we can easily implement different scoping strategies (dynamic vs. static) and calling conventions (call by name vs. call by value vs. call by need). “Lambda: The ultimate declarative” continues the discussion of GOTO expressions started in “Lambda: The ultimate imperative”. Main focus in placed on relation between GOTOs, function calls and operations that modify environment (function call is one of them, assignments are another). The paper provides some really deep insight into the mechanisms of compiling function calls. For example, authors demonstrate that in compiled Scheme code it is not necessary to make any function calls – GOTOs (unconditional jumps) are all that is needed. There’s also an interesting discussion on defining data types using closures and named variables vs. temporaries (unnamed variables generated by the compiler). Paper concludes with a thought that the expressive power of Lisp makes it a good candidate for an intermediate language used in compilers.

As I already mentioned I consider these papers to be one of the best papers I have read. I am truly impressed with the amount of knowledge squeezed into these 90 pages. Probably the most surprising thing is that after almost 40 years since their original publication Lambda Papers remain relevant. It is interesting to see that some ideas are mentioned briefly in those papers and today these ideas have evolved into really important concepts. For example Steele mentions in “Lambda: The ultimate declarative” about the idea of annotating functions with information about possible side effects, which is done in Haskell’s type system to separate pure and impure code. I have also found it interesting to learn a bit about history of computer science and trace the origin of concepts like thunks and continuations.

That’s only the outline of the Lambda Papers. They provide a lot more insightful information and I strongly encourage anyone interested in programming languages to read these two publications. They are not too difficult – if you know Scheme you’ll be able to grasp them.

Staypressed theme by Themocracy