Edit codata

src/pages/codata/codata.md

@@ -1,6 +1,8 @@
 ## Data and Codata
 
-Data describes what things are, while codata describes what things can do. Data is defined in terms of constructors that produce elements of the data types. Let's take a very simple algebraic data type: a `Bool` is either `True` or `False`. We know we can represent this in Scala as
+Data describes what things are, while codata describes what things can do. 
+
+We have seen that data is defined by giving constructors that produce elements of the data type. Let's take a very simple algebraic data type: a `Bool` is either `True` or `False`. We know we can represent this in Scala as
 
 ```scala mdoc:silent
 enum Bool {
@@ -12,7 +14,7 @@ enum Bool {
 The definition tells us there are two ways to construct an element of type `Bool`.
 Furthermore, if we have such an element we can tell exactly which case it is, by using a pattern match for example. Similarly, if the instances themselves hold data, as in `List` for example, we can always extract all the data within them. Again, we can use pattern matching to achieve this.
 
-Codata, on the other hand, is defined in terms of operations we can perform on the elements of the type. These operations are sometimes called destructors (which we've already encountered), observations, or eliminators. Common example of codata are data structures such as sets. We might define the operations on a `Set` with elements of type `A` as:
+Codata, in contrast, is defined in terms of operations we can perform on the elements of the type. These operations are sometimes called **destructors** (which we've already encountered), **observations**, or **eliminators**. Common example of codata are data structures such as sets. We might define the operations on a `Set` with elements of type `A` as:
 
 - `contains` which takes a `Set[A]` and an element `A` and returns a `Boolean` indicating if the set contains the element,
 - `insert` which takes a `Set[A]` and an element `A` and returns a `Set[A]` containing all the elements from the original set and the new element, and
@@ -34,11 +36,19 @@ trait Set[A] {
 }
 ```
 
-This definition does not tell us anything about the internal representation of the set. It could use a hash table, a tree, or something more exotic. It does, however, tell us what we can do with the set. We know we can take the union, but not the intersection, for example. If you come from the object-oriented world you might recognize the description of codata above as programming to an interface. In many ways codata is just taking concepts from the object-oriented world and presenting them in a way that is consistent with the rest of the functional programming paradigm.
+This definition does not tell us anything about the internal representation of the set. It could use a hash table, a tree, or something more exotic. It does, however, tell us what we can do with the set. We know we can take the union, but not the intersection, for example. 
+
+If you come from the object-oriented world you might recognize the description of codata above as programming to an interface. In many ways codata is just taking concepts from the object-oriented world and presenting them in a way that is consistent with the rest of the functional programming paradigm.
+
+Let's now be a little more precise in our definition. 
+
+Data is defined as a sum of products. Each element in the sum is a constructor, and the products are the parameters that the constructors take. We can think of constructors as functions with take input and produce an element of data.
+
+Codata is defined as a product of functions, these functions being the destructors, or observations, or eliminators. The input to a destructor is always an element of the codata type and possibly some other parameters. The output is usually something that is not of the codata type. Structural corecursion produces codata.
 
-Let's now be a little more precise in our definition. Codata is defined as a product of functions. These functions are known as destructors, or observations, or eliminators. The input to a destructor is always an element of the codata type and possibly some other parameters. The output is usually something that is not of the codata type. Structural corecursion produces codata.
+Compare the definition to data. 
 
-Compare the definition to data. Data is defined as a sum of products. Each element in the sum is a constructor, and the products are the parameters that the constructors take. Data is consumed using structural recursion. The input to a structural recursion is always an element of the data type and possibly some other parameters. The output is usually something else. 
+Data is consumed using structural recursion. The input to a structural recursion is always an element of the data type and possibly some other parameters. The output is usually something else. 
 
 
 In the previous chapter we discussed both destructors and structural corecursion, so why introduce them again? The reason is that codata allows us to do things that we cannot do with data. For example, codata can represent structures with an infinite number of elements, such as list that never ends or a server loop that runs indefinitely. Structural corecursion provides the strategy for writing programs that deal with these structures. For example, we can write demand-driven programs, which compute as much of a result as the rest of the program requires, as corecursions. 

src/pages/codata/index.md

@@ -3,18 +3,21 @@
 In this chapter we will look at **codata**, the dual of algebraic data types.
 Algebraic data types focus on how things are constructed.
 Codata, in contrast, focuses on how things are used.
-Defining codata means defining an interface of operations that can be performed on the type.
+Defining codata means defining an set of operations that can be performed on the type.
 This is very similar to the use of interfaces in object-oriented programming, and this is the first reason that we are interested in codata: codata puts object-oriented programming into a coherent conceptual framework with the other strategies we are discussing.
 That's not all, however.
-Codata also allows us to create structures with an infinite number of elements, such as a list that never ends or a server loop that runs indefinitely. Structural corecursion is the strategy for writing programs that handle codata, including infinite structures. Structural corecursion allows us to, for example, write demand-driven programs, which compute as much of a result as the rest of the program requires. 
+Codata also allows us to create structures with an infinite number of elements, such as a list that never ends or a server loop that runs indefinitely. 
 Codata also gives a different form of extensibility to algebraic data.
 Whereas we can easily write new functions that transform algebraic data, we cannot add new cases to the definition of an algebraic data type without changing the existing code.
 The reverse is true for codata. We can easily create new implementations of codata, but functions that transform codata are limited by the interface the codata defines.
+In the previous chapter we saw structural recursion and structural corecursion could be used to guide us in writing programs using algebraic data types.
+The same holds for codata.
+We can use codata forms of structural recursion and corecursion to guide us in writing programs that consume and produce codata respectively.
 
-We'll start by more carefully defining codata alongside some concrete examples. 
+We'll start by defining codata and seeing some examples. 
 We'll then talk about representing codata in Scala, and the relationship to object-oriented programming.
-Once we can create codata, we'll see how to work with it using structural corecursion.
+Once we can create codata, we'll see how to work with it using structural recursion and corecursion, using an example of an infinite structure.
 Next we will look at transforming algebraic data to codata, and vice versa.
-We will then focus on what makes codata distinctive, looking first at infinite structures and then differences in extensibility.
+We will finish by examining differences in extensibility.
 
 A quick note about terminology before we proceed. We might expect the term algebraic codata for the dual of algebraic data, but conventionally just codata is used. I expect this is because data is usually understood to have a wider meaning than just algebraic data, but codata is not used outside of programming language theory. For simplicity and symmetry, within this chapter I'll just use data to refer to algebraic data types.

src/pages/codata/infinite.md

@@ -1,6 +1,6 @@
 ## Structural Corecursion and Infinite Codata
 
-In this section we'll explore structural corecursion with an example of codata representing a potentially infinite set of elements. In particular, we will build a library for streams, sometimes known as lazy lists. These are the codata equivalent of lists. Where a list must have a finite length a stream's length may be unbounded.
+In this section we'll explore structural corecursion using an example of codata that represents a potentially infinite set of elements. In particular, we will build a library for streams, sometimes known as lazy lists. These are the codata equivalent of lists. Where a list must have a finite length, a stream's length may be unbounded.
 
 Let's start by reviewing structural corecursion. The key idea is to use the output type of the method to drive the process of writing the method. We previously looked at structural corecursion when we were producing data.
 In this case we saw that structural corecursion works by considering all the possible outputs, which are the constructors of the algebraic data type, and then working out the conditions under which we'd call each constructor. The process is similar for codata, but instead of considering each possible constructor we instead consider each method or function in the codata type, and what it's implementation should be.
@@ -104,7 +104,12 @@ trait Stream[A] {
 }
 ```
 
-We can use either the structural recursion or structural corecursion strategies for algebraic data to implement `take`. Since we've already covered these in detail I won't go through them here. The important point is that `take` only uses the destructors when interacting with the `Stream`. The pattern of code
+We can use either the structural recursion or structural corecursion strategies for algebraic data to implement `take`. Since we've already covered these in detail I won't go through them here. The important point is that `take` only uses the destructors when interacting with the `Stream`. The pattern of code that uses the `Stream`
+
+```scala
+if isEmpty then ???
+else head ??? tail
+```
 
 **Describe derivation of this method. First, it's defined solely in terms of destructors. Second it's a structural recursion and structural corecursion. Then pattern for using codata / Stream**