Work on indexed codata

src/pages/indexed-types/codata.md

@@ -12,8 +12,7 @@ trait Switch {
 ```
 
 There are no constraints on this interface as defined; we can turn any switch on, even if it is already on, and vice versa.
-Let's start implementing the constraint we are after.
-Our first step is to add a type parameter, which will hold the state of the `Switch`.
+The first step to implement such a constraint is to add a type parameter, which will hold the state of the `Switch`.
 
 ```scala mdoc:reset:silent
 trait Switch[A] {
@@ -22,10 +21,13 @@ trait Switch[A] {
 }
 ```
 
-This type parameter doesn't correspond to any data we store in `Switch`, so it is sometimes called a phantom type.
+This type parameter doesn't correspond to any data we store in `Switch`, so it is a phantom type.
 This is the first part of implementing indexed codata.
-We still need to add the constraints.
-This has two parts: defining types to represent on and off, and then adding the constraints to the relevant methods on `Switch`.
+We are now going to add constraints that say we can only call a certain method when this type parameter corresponds to a particular concrete type.
+It is in this way that indexed codata goes beyond what phantom types alone can do: we can inspect, at compile-time, the type of a type parameter and make decisions based on this type.
+
+Implementing these constraints has two parts.
+The first is defining types to represent on and off. 
 
 Here are the types.
 
@@ -34,7 +36,8 @@ trait On
 trait Off
 ```
 
-Now we can add the constraints.
+The second step is to add the constraints to the relevant methods on `Switch`.
+Here is how we do it.
 
 ```scala mdoc:silent
 trait Switch[A] {
@@ -70,3 +73,9 @@ Incorrect uses fail to compile.
 ```scala mdoc:fail
 SimpleSwitch.on.on
 ```
+
+The constraint is made of two parts: using clauses, which we learned about in [@sec:type-classes], and the [`A =:= B`][scala.=:=] construction, which is new. `=:=` represents a type equality. If a given instance `A =:= B` exists, then the type `A` is equal to the type `B`. (Note we can write this with the more familiar prefix notation `=:=[A, B]` if we prefer.) We never create these instances; instead the compiler creates them for us. In the `on` method, we are asking the compiler to construct an instance `A =:= Off`, which can only be done if `A` is `Off`. This in turn means we can only call the method when the `Switch` is `Off`. This is the core idea of indexed codata: we reflect states as types, and restrict method calls to a subset of states.
+
+
+### API Protocols
+

src/pages/indexed-types/phantom-type.md

@@ -54,6 +54,10 @@ in further processing.
 For example, force times length gives torque (with the SI unit of newton-metres).
 However we cannot define a `*` method on `Length` that can only be called if the `Unit` is `Metre` using just the tool of phantom types.
 Similarly, we cannot define, say, a `toString` method that uses the `Unit` type to appropriately print the result.
+Solving these problems leads us to indexed codata, so let's now look at that.
+
+
+
 We'll solve all these problems in due course, but before we move on let's see another, more complex, example of phantom types to give you a better understanding of their power.
 
 Our next example will represent a subset of [HTML][html], the language used to write web pages, in a typesafe way.
@@ -70,5 +74,18 @@ An example of HTML is below.
 </html>
 ```
 
+In HTML the content of the page is marked up with tags, like `<h1>`, that give it meaning. 
+For example, `<h1>` means a heading at level one, and `<p>` means a paragraph.
+An opening tag is closed by a corresponding closing tag such as `</h1>` for `<h1>` and `</p>` for `<p>`.
+
+There are rules that control where tags are allowed. The complete set of tags, and their associated rules, is very complex. We'll use the following much simplified rules:
+
+- the `body` tag can only contain block level tags;
+- block level tags are `h1` and `p` and can only contain inline tags; and
+- inline tags are `strong` and `em` and can only contain inline tags.
+
+We're missing one thing: we need to be able to end our recursion in text content. In fact we have two different kinds of tags: those that can contain text content in addition to other tags (we'll call these content tags) and those that cannot (which we will call structural tags.)
+
+
 [mars]: https://en.wikipedia.org/wiki/Mars_Climate_Orbiter#Cause_of_failure
 [html]: https://html.spec.whatwg.org/multipage/

src/pages/links.md

@@ -1,4 +1,5 @@
 [scala.Option]: http://www.scala-lang.org/api/current/scala/Option.html
+[scala.=:=]: https://www.scala-lang.org/api/current/scala/=:=.html#
 
 [cats.package]: http://typelevel.org/cats/api/cats/
 [cats.Apply]: http://typelevel.org/cats/api/cats/Apply.html