Editing pass on types as constraints chapter

Author: noelwelsh

src/pages/types/conclusions.typ

@@ -1,15 +1,21 @@
 #import "../stdlib.typ": narrative-cite, href
 == Conclusions <sec:types:conclusions>
 
+In this chapter we've looked at using types to represent constraints,
+which allows the compiler to help us ensure these constraints are met throughout our program.
+We call this strategy "types as constraints".
+We constrasted this strategy to the better known view of types that focuses on representation.
+Finally, we saw opaque types as a lightweight tool that decouples types from their representation,
+allowing us to define a type that uses the same representation as some other type.
+
 The view of types as constraints is perhaps best presented in Alexis King's blog post #href("https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/")[Parse, don't validate].
+#narrative-cite(<morris73:types>) is a very early paper (typewritten in two column justified text, a truly virtuoso performance on the type writer!) that also presents the intensional view of types. I feel it ends a bit abruptly, but has the seed of many ideas that will only be fully developed much later. You can see the suggestion of opaque types as discussed in this chapter, and also module systems and existential types.
 
 From a programming language perspective, #narrative-cite(<pierce02:tapl>) is the standard reference on type systems.
 They define a type system as "a tractable syntactic method for proving the absence of certain program behaviours by classifying phrases by the kinds of values they compute".
 The introduction provides a very nice overview of the role of type systems in programming languages, as well as pointers to the broader study of type systems in mathematics and philosophy. 
 
-#narrative-cite(<morris73:types>) is a very early paper (typewritten in two column justified text, a truly virtuoso performance on the type writer!) that presents the intensional view of types. I feel it ends a bit abruptly, but has the seed of many ideas that will only be fully developed much later. You can see the suggestion of opaque types as discussed in this chapter, and also module systems and existential types.
-
-Having said that types are not sets, it feels only fair to mention there are type systems that treat types as sets. #narrative-cite(<castagna23:elixir>) describes one such system. 
+Having said that types are not sets, it feels only fair to mention there are type systems that do treat types as sets. #narrative-cite(<castagna23:elixir>) describes one such system. 
 These type systems emphasize the extensional view, and have a very different feel to conventional type systems.
 
 I'm very far from an expert in mathematical type theory. As such, I found #narrative-cite(<klev19:comparison>) useful to relate type theory to something I better understand, set theory.

src/pages/types/constraints.typ

@@ -3,24 +3,22 @@
 
 Most applications work by progressively adding structure to inputs.
 We might receive data from, say, the network or a database.
-We perform some checks on that data, and remove instances that are invalid.
+We perform some checks on that data and remove instances that are invalid.
 We then do some more work, which entails further checks, and so on.
 
 For example, imagine we're implementing a sign up flow.
 We start by asking for a user name and email address.
 Basic checks could be requiring names that are not empty, and email addresses that contain an `@`.
 We won't even let the user submit the form if these checks fail.
-If this looks ok, we'll move on to further checks.
-For example, we might validate email addresses
-by sending them a verification email.
+Once the form is submitted we'll move on to further checks.
+For example, we might validate email addresses by sending them a verification email.
 
 How should we represent these multiple levels of validation?
 For example, how do we distinguish a string representing a name from one that is an email address?
 How about an unverified email from a verified one?
-If you've worked on enough projects you've probably seen many approaches to this.
-Many code bases use names in an ad hoc do this.
+The most common approach that I've seen, across many code bases, is to use ad hoc naming conventions.
 For example, we might use the name `email` and `verifiedEmail` to distinguish the different kinds of email addresses
-in method parameters and data structure members,
+in method parameters and data structure,
 while still representing both as strings.
 #footnote[
     #href("https://en.wikipedia.org/wiki/Hungarian_notation")[Hungarian notation] is a more formal approach to
@@ -30,13 +28,14 @@ while still representing both as strings.
 ]
 
 Types provide a compelling alternative to naming schemes.
-It provides all the advantages of naming schemes,
-while also representing this information in a form the compiler can check for us.
+They enforce consistency of nomenclature,
+while also representing this information in a form the compiler can check.
 For example, if we have `EmailAddress` and `VerifiedEmailAddress` types,
-the compiler will tell us if we try to use an `EmailAddress` where a `VerifiedEmailAddress` is required,
+not only do we have standard names,
+but the compiler will tell us if we try to use an `EmailAddress` where a `VerifiedEmailAddress` is required,
 or a `String` where an `EmailAddress` is required.
 Furthermore, when we see an `EmailAddress` we know it's already been through some validation,
-so we don't need to repeat this validation (or worse, forget to do it.)
+so we don't needlessly repeat validation, or worse, forget to do it.
 This brings us to two principles:
 
 1. Types should represent what we know about values, or in other words the invariants or constraints on values. A `String` could be any sequence of characters. A `VerifiedEmailAddress` is also a sequence of characters, but it's one that represents an email address that we have verified is active.
@@ -57,7 +56,7 @@ def domain(email: String): Option[String]
 
 indicating that the `String` might not be a valid email.
 In this case we push the error handling,
-which reflects the constraint that we only work with valid email addresses,
+reflecting the constraint that we only work with valid email addresses,
 onto the downstream code that deals with the result of calling this method.
 
 When we work with types as constraints the signature becomes
@@ -69,22 +68,23 @@ def domain(email: EmailAddress): String
 There is now no possibility of error, as an email address must contain a domain.
 However, we have pushed the constraint, obtaining an `EmailAddress`,
 onto the upstream code that calls this method.
-At some point we must bottom out and have conversions that could fail,
+At some point we must have conversions that could fail,
+which requires error handling,
 but this approach pushes error handling to the edges of the program.
 This tends to result in a better user experience,
 as the user is immediately notified of problems,
-and also makes the code simpler to work with as less error handling is required.
+and also makes the code simpler to work with as overall less error handling is required.
 
-Finally, although this strategy is easiest to explain in the context of validation,
-it's not restricted to only this use.
-As an example, let's think about writing code that presents an API for updates to a database table.
+Although this strategy is easiest to explain in the context of validation,
+it's not restricted to this use case.
+As an example, imagine writing an API for updates to a database table.
 Some columns allow nulls and some do not.
-When updating a nullable column we could accept an `Option`,
-with the `None` case meaning setting the column to null.
+When updating a nullable column our API could accept an `Option`,
+with the `None` case meaning the column is set to null.
 When updating a non-nullable column we could also accept an `Option`,
-with the `None` case meaning we retain the existing value.
+with the `None` case meaning we retain the column's existing value.
 These two different meaning of the same type are a sure way to introduce errors,
 with users nulling out columns they intended to leave unchanged.
+The solution is the same: use different types for the different kinds of columns.
 Here the constraints are not on the values represented by the type,
-but on the behaviour associated with the type.
-The same type should not have different behaviours in the same API.
+but on the behaviour associated with them.

src/pages/types/index.typ

@@ -3,15 +3,15 @@
 
 Our very first strategy is using *types as constraints*.
 We'll start by discussing two different ways we can think of types:
-by what it is, sometimes known as an *extensional* view; and
-by what it can do, sometimes known as an *intensional* view.
-The latter view is not as well known,
+by a type is, sometimes known as an *extensional* view; and
+by what a type can do, sometimes known as an *intensional* view.
+The latter view is less familiar,
 but is necessary to get the most from an expressive type system
 and is the core of the strategy.
-Hence we'll spend some time elaborating on this idea, and discussing examples.
+Hence we'll spend some time elaborating on this idea and discussing examples.
 
 Once we understand the concept of types as constraints,
 we'll look at a Scala 3 feature, known as *opaque types*.
-Opaque types allow us to create distinct types that have the same runtime representation as another type.
+Opaque types allow us to create a distinct type that has the same runtime representation as another type.
 As such, they provide a way to decouple representation from operations,
 and allow us to work with a purely intensional view.

src/pages/types/opaque.typ

@@ -14,7 +14,7 @@ opaque type EmailAddress = String
 
 This is enough to define the type `EmailAddress` as represented by a `String`.
 However, it's a useless definition as it lacks any way to construct an `EmailAddress`.
-To properly understand how we can define a constructor, we need to understand that opaque types divide our code base into two distinct parts: that where our type is transparent, where we know the underlying representation, and the remainder where it is opaque.
+To properly understand how we can define a constructor, we need to understand that opaque types divide our code base into two distinct parts: where our type is transparent, which is where we know the underlying representation, and the remainder where it is opaque.
 The rule is pretty simple: an opaque type is transparent within the scope in which it is defined, so within an enclosing object or class.
 If there is no enclosing scope, as in the example above,
 it is transparent only within the file in which it is defined.
@@ -94,13 +94,13 @@ yet it is a different type.
 Alternatively, we can view it as a semantic gain.
 An `EmailAddress` _is_ a sequence of characters,
 the same as a `String`,
-but it has additional properties.
+but it has additional constraints.
 In this case we verify it contains exactly one `@` character,
-and our email addresses are case insensitive.
+and ensure it is case insensitive.
 
 We've seen how to define opaque types and their constructors.
 What about other methods?
-For example, for an `EmailAddress` we might want to get the username and domain.
+For example, for an `EmailAddress` we might want methods to get the username and domain.
 We can use extension methods to do this.
 As with the constructor, we just need to define these extension methods in a place where the type is transparent.
 
@@ -138,17 +138,108 @@ email.username
 email.domain
 ```
 
+There are two other features of opaque types that we should mention:
+
+1. they can have type parameters; and
+2. they can have type bounds.
+
+Let's see an example of these two features used together. 
+Earlier we saw an example of using an `Option` to represent two different types of database columns:
+nullable columns, where `None` mean to set the column to null, and non-nullable, where `None` means to keep the existing value.
+We can define these as opaque types with a type parameter.
+
+```scala mdoc:silent
+// null is a reserved word in Scala, so we use the name nil
+// instead.
+opaque type Nilable[+A] = Option[A]
+object Nilable {
+  def apply[A](value: A): Nilable[A] = Some(value)
+
+  def fromOption[A](option: Option[A]): Nilable[A] = option
+
+  val nil: Nilable[Nothing] = None
+}
+
+opaque type Default[+A] = Option[A]
+object Default {
+  def apply[A](value: A): Default[A] = Some(value)
+
+  def fromOption[A](option: Option[A]): Default[A] = option
+
+  val default: Default[Nothing] = None
+}
+```
+
+This works just as we'd expect, but we users will probably want to use the `Option` API on `Nilable` and `Default`.
+We can avoid tediously reimplementing it as extension methods by declaring that `Nilable` and `Default` are subtypes of `Option`.
+
+```scala mdoc:reset:silent
+opaque type Nilable[+A] <: Option[A] = Option[A]
+object Nilable {
+  def apply[A](value: A): Nilable[A] = Some(value)
+
+  def fromOption[A](option: Option[A]): Nilable[A] = option
+
+  val nil: Nilable[Nothing] = None
+}
+
+opaque type Default[+A] <: Option[A] = Option[A]
+object Default {
+  def apply[A](value: A): Default[A] = Some(value)
+
+  def fromOption[A](option: Option[A]): Default[A] = option
+
+  val default: Default[Nothing] = None
+}
+```
+
+The type bound `Default[+A] <: Option[A]` says that `Default` is a subtype of `Option`,
+and crucially this information is publically available.
+Therefore all of the methods on `Option` are available on `Default`.
+
+```scala mdoc:reset:invisible
+object Wrapper {
+  opaque type Nilable[+A] <: Option[A] = Option[A]
+  object Nilable {
+    def apply[A](value: A): Nilable[A] = Some(value)
+    def fromOption[A](option: Option[A]): Nilable[A] = option
+    val nil: Nilable[Nothing] = None
+  }
+  
+  opaque type Default[+A] <: Option[A] = Option[A]
+  object Default {
+    def apply[A](value: A): Default[A] = Some(value)
+    def fromOption[A](option: Option[A]): Default[A] = option
+    val default: Default[Nothing] = None
+  }
+}
+import Wrapper.*
+```
+
+We can verify this with a few examples.
+
+```scala mdoc
+Nilable(1).orElse(Nilable.nil)
+
+Default(1).map(_ + 1)
+```
+
+Notice that the results have type `Option`,
+because the methods on `Option` that we call have return type `Option`.
+We can easily convert back to `Nilable` or `Default` as required by using the `fromOption` constructor.
+
+
 === Best Practices
 
 We've seen all the important technical details for opaque types,
-so let's now discuss some of the best practices---the craft---of using them.
+so let's now discuss some of the best practices of using them.
 
-The first point I want to address is the constructor. "Types as constraints" is the strategy we're covering in this chapter.
+The first point I want to address is illustrated by the constructor for `EmailAddress`. 
 There is a constraint on the `String` input to the constructor: it must contain an `@` character.
-We should represent this as a type!
-We could create another opaque type, called something like `StringWithAnAtCharacter`, but this approaches leads to infinite regress.
-We cannot push constraints forward indefinitely.
-At some point we have to work with primitive types and return a result that indicates the possibility of error.
+This is a constraint and we should represent this as a type!
+We could create another opaque type, called something like `StringWithAnAtCharacter`, but this approach leads to infinite regress.
+We cannot push constraints upstream indefinitely.
+At some point we have to return a result that indicates the possibility of error.
 So our constructor would be better if it returned, say, an `Option` or `Either` to indicate that construction can fail.
 
 There are cases where we know the constructor cannot fail,
@@ -157,7 +248,7 @@ For example, if we're loading email addresses from a list that is known to be go
 For this reason I recommend including a constructor that doesn't do any validation.
 I usually call this method `unsafeApply`, to indicate to the reader that certain checks are not being done.
 These changes are shown below.
-For simplicity I've used `Option` as the result type.
+For simplicity I've used `Option` as the result type to indicate the possibility of failure.
 
 ```scala mdoc:reset:silent
 type EmailAddress = String
@@ -173,9 +264,9 @@ object EmailAddress {
 }
 ```
 
-At some point we'll almost certainly need to convert from our opaque type back to its underlying type.
+We'll almost certainly need to convert from our opaque type back to its underlying type at some point in our code.
 I've seen a few conventions for naming such a method; `value` and `get` are popular.
-However, I prefer a more descriptive `toType`, replacing `Type` with the concreate type name,
+However, I prefer a more descriptive `toType`, replacing `Type` with the concrete type name,
 as this extends to conversions to other types.
 For `EmailAddress` this means an extension method `toString`, as shown below.
 Notice that the method simply returns the `address` value,
@@ -197,12 +288,11 @@ For example, a (two-dimensional) point requires two coordinates, so there is no
     We could use an `Array[Double]` or `Tuple2[Double, Double]`,
     but it's simpler to just define a class in the usual way.
 ].
-We also cannot define opaque types with type parameters.
 In these cases we're probably looking for an algebraic data type,
 which is discussed in @sec:adt.
 
 The second case is when we need to reimplement one of the methods, most commonly `toString`, that opaque types cannot override.
 For example,
-if we're creating types that represent personal information such as addresses and passwords, we might want to ensure they cannot be accidentally exposed in logs.
+we might want to ensure that types representing personal information, such as addresses and passwords, cannot be accidentally exposed in logs.
 Overriding `toString` helps ensure this, but we cannot do this for opaque types.