-
-
Notifications
You must be signed in to change notification settings - Fork 133
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
4 changed files
with
169 additions
and
20 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,5 +1,119 @@ | ||
## The Algebra of Algebraic Data Types | ||
|
||
Algebra of algebraic data types | ||
A question that sometimes comes up is where the "algebra" in algebraic data types comes from. I want to talk about this a little bit and show some of the algebraic manipulations that can be done on algebraic data types. | ||
|
||
Exponential types, quotient types. | ||
The term algebra is used in the sense of abstract algebra, an area of mathematics. | ||
Abstract algebra deals with algebraic data structures. | ||
An algebraic structure consists of a set of values, operations on that set, and properties that those operations must maintain. | ||
An example is integers, the operations addition and multiplication, and the familiar properties of these operations such as associativity, which says that $a + (b + c) = (a + b) + c$. | ||
The abstract in abstract algebra means that the field doesn't deal with concrete values like integers---that would be far too easy to understand---and instead with abstractions with wacky names like semigroup and monoid. | ||
We'll see a lot more of these soon enough! | ||
|
||
Algebraic data structures correspond to an algebraic structure called a ring. | ||
A ring has two operations, which are conventionally denoted with $+$ and $\times$. | ||
You'll perhaps guess that these correspond to sum and product types respectively, and you'd be absolutely correct. | ||
What about the properties of these operations? | ||
We'll they are similar to what we know from basic algebra: | ||
|
||
- $+$ and $\times$ are associative, so $a + (b + c) = (a + b) + c$ and likewise for $\times$; | ||
- $a + b = b + a$, known as commutivitiy; | ||
- there is an identity $0$ such that $a + 0 = a$; | ||
- there is an identity $1$ such that $a \times 1 = a$; | ||
- there is distribution, such that $a \times (b + c) = (a \times b) + (a \times c)$ | ||
|
||
So far, so abstract. | ||
Let's make it concrete by looking at actual examples in Scala. | ||
|
||
Remember the algebraic data types work with types, so the operations $+$ and $\times$ take types as parameters. | ||
So $Int \times String$ is equivalent to | ||
|
||
```scala mdoc:silent | ||
final case class IntAndString(int: Int, string: String) | ||
``` | ||
|
||
To avoid creating all these names we can use tuples instead | ||
|
||
```scala mdoc:reset:silent | ||
type IntAndString = (Int, String) | ||
``` | ||
|
||
We can do the same thing for $+$. $Int + String$ is | ||
|
||
```scala mdoc:silent | ||
enum IntOrString { | ||
case IsInt(int: Int) | ||
case IsString(string: String) | ||
} | ||
``` | ||
|
||
or just | ||
|
||
```scala mdoc:reset:silent | ||
type IntOrString = Either[Int, String] | ||
``` | ||
|
||
#### Exercise: Identities {-} | ||
|
||
Can you work out which Scala type corresponds to the identity $1$ for product types? | ||
|
||
<div class="solution"> | ||
It's `Unit`, because adding `Unit` to any product doesn't add any more information. | ||
So, `Int` contains exactly as much information as $Int \times Unit$ (written as the tuple `(Int, Unit)` in Scala). | ||
</div> | ||
|
||
What about the Scala type corresponding to the identity $0$ for sum types? | ||
|
||
<div class="solution"> | ||
It's `Nothing`, following the same reasoning as products: a case of `Nothing` adds no further information (and we cannot even create a value with this type.) | ||
</div> | ||
|
||
|
||
What about the distribution law? This allows us to manipulate algebraic data types to form equivalent, but perhaps more useful, representations. | ||
Consider this example of a user data type. | ||
|
||
```scala mdoc:silent | ||
final case class Person(name: String, permissions: Permissions) | ||
enum Permissions { | ||
case User | ||
case Moderator | ||
} | ||
``` | ||
|
||
Written in mathematical notation, this is | ||
|
||
$$ | ||
Person = String \times Permissions | ||
$$ | ||
$$ | ||
Permissions = User + Moderator | ||
$$ | ||
|
||
Performing substitution gets us | ||
|
||
$$ | ||
Person = String \times (User + Moderator) | ||
$$ | ||
|
||
Applying distribution results in | ||
|
||
$$ | ||
Person = (String \times User) + (String \times Moderator) | ||
$$ | ||
|
||
which in Scala we can represent as | ||
|
||
```scala mdoc:reset:silent | ||
enum Person { | ||
case User(name: String) | ||
case Moderator(name: String) | ||
} | ||
``` | ||
|
||
Is this representation more useful? I can't say without the context of where the code is being used. However I can say that knowing this manipulation is possible, and correct, is useful. | ||
|
||
There is a lot more that could be said about algebraic data types, but at this point I feel we're really getting into the weeds. | ||
I'll finish up with a few pointers to other interesting facts: | ||
|
||
- Exponential types exist. They are functions! A function `A => B` is equivalent to $b^a$. | ||
- Quotient types also exist, but they are a bit weird. Read up about them if you're interested. | ||
- Another interesting algebraic manipulation is taking the derivative of an algebraic data type. This gives us a type of iterator, known as a zipper, for that type. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,5 +1,23 @@ | ||
## Conclusions | ||
|
||
We have covered a lot of material in this chapter. The key points are: | ||
|
||
[How to Design Co-Programs](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/copro.pdf) | ||
- algebraic data types represent data expressed as logical ands and logical ors of types; | ||
- algebraic data types are the main way to represent data in Scala; | ||
- structural recursion gives a skeleton for converting a given algebraic data type into any other type; | ||
- structural corecursion gives a skeleton for converting any type into a given algebraic data type; and | ||
- there are other reasoning principles (primarily, following the types) that help us complete structural recursions and corecursions. | ||
|
||
There is a lot packed into this chapter. | ||
We'll see many more examples thoughout the rest of the book, which will help reinforce the concepts. | ||
Below are some references that you might find useful if you want to dig in further into the concepts covered in this chapter. | ||
|
||
|
||
Algebraic data types are standard in introductory material on functional programming, but structural recursion seems to be much less commonly known. | ||
I learned about both from [How to Design Program](https://htdp.org/). | ||
I'm not aware of any concise reference for algebraic data types and structural recursion. | ||
This original material, whatever it is, seems to be too old to be available online and now concepts have become so commonly known that they are assumed background knowledge in most sources. | ||
|
||
Corecursion is a bit better documented. [How to Design Co-Programs](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/copro.pdf) covers the main idea we have looked at here. [The Under-Appreciated Unfold](https://dl.acm.org/doi/pdf/10.1145/289423.289455) discusses uses of `unfold`. | ||
|
||
[The Derivative of a Regular Type is its Type of One-Hole Contexts] (https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=7de4f6fddb11254d1fd5f8adfd67b6e0c9439eaa) describes the derivative of algebraic data types. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters