Skip to content

Commit 2f03dec

Browse files
committed
San serif headings, Typst format of ADT chapter
- Use Lato as the font for heading - Tweak heading size - Add `exercise` function to stdlib - Reformat algebraic data type chapter to Typst syntax
1 parent 21d6e1e commit 2f03dec

File tree

8 files changed

+68
-55
lines changed

8 files changed

+68
-55
lines changed

src/pages/adt/algebra.typ

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#import "../stdlib.typ": info, warning, solution
1+
#import "../stdlib.typ": info, warning, solution, exercise
22
== The Algebra of Algebraic Data Types
33

44

@@ -56,7 +56,7 @@ type IntOrString = Either[Int, String]
5656
```
5757

5858

59-
==== Exercise: Identities {-}
59+
#exercise[Identities]
6060

6161

6262
Can you work out which Scala type corresponds to the identity $1$ for product types?
@@ -87,8 +87,8 @@ enum Permissions {
8787
Written in mathematical notation, this is
8888

8989
$
90-
"Person" = "String" times "Permissions"
91-
"Permissions" = "User" + "Moderator"
90+
"Person" &= "String" times "Permissions" \
91+
"Permissions" &= "User" + "Moderator"
9292
$
9393

9494
Performing substitution gets us

src/pages/adt/conclusions.typ

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#import "../stdlib.typ": info, warning, solution
1+
#import "../stdlib.typ": href
22
== Conclusions
33

44

@@ -25,18 +25,18 @@ Below are some references that you might find useful if you want to dig in furth
2525

2626
Algebraic data types are standard in introductory material on functional programming.
2727
Structural recursion is certainly extremely common in functional programming, but strangely seems to rarely be explicitly defined as I've done here.
28-
I learned about both from #cite(<felleisen18:htdp>, form: "prose").
28+
I learned about both from _How to Design Programs_ @felleisen18:htdp.
2929

3030
I'm not aware of any approachable yet thorough treatment of either algebraic data types or structural recursion.
3131
Both seem to have become assumed background of any researcher in the field of programming languages,
3232
and relatively recent work is caked in layers of mathematics and obtuse notation that I find difficult reading.
3333
The infamous _Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire_ @meijer91:bananas is an example of such work.
3434
I suspect the core ideas of both date back to at least the emergence of computability theory in the 1930s, well before any digital computers existed.
3535

36-
The earliest reference I've found to structural recursion is #cite(<burstall69:proving>, form: "prose").
37-
Algebraic data types don't seem to have been fully developed, along with pattern matching, until #link("https://en.wikipedia.org/wiki/NPL_(programming_language)")[NPL] in 1977.
38-
NPL was quickly followed by the more influential language #link("https://en.wikipedia.org/wiki/Hope_(programming_language)")[Hope], which spread the concept to other programming languages.
36+
The earliest reference I've found to structural recursion is _Proving Properties of Programs by Structural Induction_ @burstall69:proving.
37+
Algebraic data types don't seem to have been fully developed, along with pattern matching, until #href("https://en.wikipedia.org/wiki/NPL_(programming_language)")[NPL] in 1977.
38+
NPL was quickly followed by the more influential language #href("https://en.wikipedia.org/wiki/Hope_(programming_language)")[Hope], which spread the concept to other programming languages.
3939

40-
Corecursion is a bit better documented in the contemporary literature. _How to Design Co-Programs_ #cite(<gibbons21:htdcp>, form: "prose") covers the main ideas we have looked at here, while #cite(<gibbons98:unfold>, form: "prose") discusses uses of `unfold`.
40+
Corecursion is a bit better documented in the contemporary literature. _How to Design Co-Programs_ @gibbons21:htdcp covers the main ideas we have looked at here, while _The under-appreciated unfold_ @gibbons98:unfold discusses uses of `unfold`.
4141

42-
#cite(<mcbride01:deriv>, form: "prose") describes the derivative of algebraic data types.
42+
_The Derivative of a Regular Type is its Type of One-Hole Contexts_ @mcbride01:deriv describes the derivative of algebraic data types.

src/pages/adt/scala.typ

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#import "../stdlib.typ": info, warning, solution
1+
#import "../stdlib.typ": exercise, solution
22
== Algebraic Data Types in Scala
33

44

@@ -47,7 +47,7 @@ enum A {
4747
}
4848
```
4949

50-
In other words we don't write `final case class` inside an `enum`. You also can't nest `enum` inside `enum`. Nested logical ors can be rewritten into a single logical or containing only logical ands (known as disjunctive normal form) so this is not a limitation in practice. However the Scala 2 representation is still available in Scala 3 should you want more expressivity.
50+
In other words we don't write `final case class` inside an `enum`. You also can't nest an `enum` inside an `enum`. Nested logical ors can be rewritten into a single logical or containing only logical ands (known as disjunctive normal form) so this is not a limitation in practice. However the Scala 2 representation is still available in Scala 3 should you want more expressivity.
5151

5252

5353
=== Algebraic Data Types in Scala 2
@@ -212,8 +212,7 @@ We've seen that the Scala 3 representation of algebraic data types, using `enum`
212212
- Scala 2's representation can express things that are almost, but not quite, algebraic data types. For example, if you define a method on an `enum` you must be able to define it for all the members of the `enum`. Sometimes you want a case of an `enum` to have methods that are only defined for that case. To implement this you'll need to use the Scala 2 representation instead.
213213

214214

215-
==== Exercise: Tree {-}
216-
215+
#exercise[Tree]
217216

218217
To gain a bit of practice defining algebraic data types, code the following description in Scala (your choice of version, or do both.)
219218

src/pages/adt/structural-corecursion.typ

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#import "../stdlib.typ": info, warning, solution
1+
#import "../stdlib.typ": info, warning, solution, exercise
22
== Structural Corecursion
33

44

@@ -9,10 +9,7 @@ Whereas we can use structural recursion whenever the input of a method or functi
99
we can use structural corecursion whenever the output of a method or function is an algebraic data type.
1010

1111

12-
#info[
13-
==== Duality in Functional Programming {-}
14-
15-
12+
#info(title: [Duality in Functional Programming])[
1613
Two concepts or structures are duals if one can be translated in a one-to-one fashion to the other.
1714
Duality is one of the main themes of this book.
1815
By relating concepts as duals we can transfer knowledge from one domain to another.
@@ -363,7 +360,7 @@ MyList.fill(5)(getAndInc())
363360
```
364361

365362

366-
==== Exercise: Iterate {-}
363+
#exercise[Iterate]
367364

368365

369366
Implement `iterate` using the same reasoning as we did for `fill`.
@@ -397,7 +394,7 @@ MyList.iterate(0, 5)(x => x - 1)
397394
]
398395

399396

400-
==== Exercise: Map {-}
397+
#exercise[Map]
401398

402399

403400
Once you've completed `iterate`, try to implement `map` in terms of `unfold`. You'll need to use the destructors to implement it.

src/pages/adt/structural-recursion.typ

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#import "../stdlib.typ": info, warning, solution
1+
#import "../stdlib.typ": info, warning, solution, exercise
22
== Structural Recursion
33

44

@@ -315,7 +315,7 @@ In these situations we can use dynamic dispatch instead.
315315
We'll learn more about this when we look at generalized algebraic data types.
316316

317317

318-
==== Exercise: Methods for Tree {-}
318+
#exercise[Methods for Tree]
319319

320320

321321
In a previous exercise we created a `Tree` algebraic data type:
@@ -572,7 +572,7 @@ Returning to `MyList`, it has:
572572
- `Pair` is a constructor with one parameter of type `A` and one recursive parameter, and hence the corresponding function has type `(A, B) => B`.
573573

574574

575-
==== Exercise: Tree Fold {-}
575+
#exercise[Tree Fold]
576576

577577

578578
Implement a fold for `Tree` defined earlier.
@@ -640,7 +640,7 @@ enum Tree[A] {
640640
]
641641

642642

643-
==== Exercise: Using Fold {-}
643+
#exercise[Using Fold]
644644

645645

646646
Prove to yourself that you can replace structural recursion with calls to fold, by redefining `size`, `contains`, and `map` for `Tree` using only fold.

src/pages/fps.typ

Lines changed: 21 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#import "stdlib.typ": title, authors, heading-multiplier, heading-space-base, heading-base
1+
#import "stdlib.typ": title, authors
22

33
#set document(
44
title: title,
@@ -34,7 +34,10 @@
3434
// Start parts on an odd page
3535
#show figure.where(kind: "part"): it => {
3636
pagebreak(weak: true, to: "odd")
37-
set text(size: 24pt * 1.2 * 1.2)
37+
set text(
38+
font: "Lato",
39+
size: 12pt * 1.333 * 1.333 * 1.333
40+
)
3841
align(left)[
3942
#strong[#it.supplement #it.counter.display(it.numbering): #it.body]
4043
]
@@ -43,30 +46,33 @@
4346
// Chapter heading starts on an odd page. Don't create a page break if the
4447
// page is already empty.
4548
pagebreak(weak: true, to: "odd")
46-
set text(size: 24pt * 1.2 * 1.2)
49+
set text(
50+
font: "Lato",
51+
size: 12pt * 1.333 * 1.333 * 1.333)
4752
it
48-
v(12pt * 1.2 * 1.2)
53+
v(12pt * 1.333)
4954
}
5055
#show heading.where(level: 2): it => {
51-
set text(size: 24pt * 1.2)
56+
v(12pt)
57+
set text(
58+
font: "Lato",
59+
size: 12pt * 1.333 * 1.333)
5260
it
53-
v(12pt * 1.2 * 1.2)
61+
v(12pt * 1.333)
5462
}
5563
#show heading.where(level: 3): it => {
56-
v(heading-space-base)
57-
set text(size: heading-base)
58-
it
59-
v(12pt)
60-
}
61-
#show heading.where(level: 4): it => {
6264
v(12pt / 1.2)
63-
set text(size: 1.44em / 1.2)
65+
set text(
66+
font: "Lato",
67+
size: 12pt * 1.333)
6468
it
6569
v(12pt)
6670
}
67-
#show heading.where(level: 5): it => {
71+
#show heading.where(level: 4): it => {
6872
v(12pt / 1.2 / 1.2)
69-
set text(size: 1.44em / 1.2 / 1.2)
73+
set text(
74+
font: "Lato",
75+
size: 12pt)
7076
it
7177
v(12pt)
7278
}

src/pages/parts/frontmatter.typ

Lines changed: 18 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#import "../stdlib.typ": title-page, heading-multiplier, heading-space-base, heading-base
1+
#import "../stdlib.typ": title-page
22

33
#let parts-and-headings = figure.where(kind: "part", outlined: true).or(heading.where(outlined: true))
44

@@ -7,25 +7,33 @@
77
// Chapter heading starts on an odd page. Don't create a page break if the
88
// page is already empty.
99
pagebreak(weak: true, to: "odd")
10-
set text(size: 24pt * 1.2 * 1.2)
10+
set text(
11+
font: "Lato",
12+
size: 12pt * 1.333 * 1.333 * 1.333)
1113
it
12-
v(12pt * 1.2 * 1.2)
14+
v(12pt * 1.333)
1315
}
1416
#show heading.where(level: 2): it => {
15-
v(heading-space-base)
16-
set text(size: heading-base)
17-
it
1817
v(12pt)
18+
set text(
19+
font: "Lato",
20+
size: 12pt * 1.333 * 1.333)
21+
it
22+
v(12pt * 1.333)
1923
}
2024
#show heading.where(level: 3): it => {
2125
v(12pt / 1.2)
22-
set text(size: 24pt / 1.2)
26+
set text(
27+
font: "Lato",
28+
size: 12pt * 1.333)
2329
it
2430
v(12pt)
2531
}
2632
#show heading.where(level: 4): it => {
2733
v(12pt / 1.2 / 1.2)
28-
set text(size: 24pt / 1.2 / 1.2)
34+
set text(
35+
font: "Lato",
36+
size: 12pt)
2937
it
3038
v(12pt)
3139
}
@@ -91,6 +99,8 @@ This book is dedicated to those who laid the path that I have followed, to those
9199
#pagebreak(to: "odd")
92100
#set page(numbering: "i")
93101
#set heading(numbering: none)
102+
#show link :set text(rgb("#996666"))
103+
94104
#include "../preface/preface.typ"
95105
#include "../preface/versions.typ"
96106
#include "../preface/conventions.typ"

src/pages/stdlib.typ

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
1-
#let callout(body, title: "", fill: blue, title-color: white, body-color: black) = {
1+
#let callout(body, title: none, fill: blue, title-color: white, body-color: black) = {
22
block(
33
stroke: (left: 8pt + fill),
44
fill: color.mix((white, 70%), (fill, 30%)),
55
width: 100%,
66
inset: 16pt
77
)[
8-
#if title.len() == 0 {
8+
#if title == none {
99
text(body-color)[#body]
1010
} else {
1111
[
12-
#heading(level: 4, outlined: false, title)
12+
#heading(depth: 4, numbering: none, outlined: false, title)
1313
#text(body-color)[#body]
1414
]
1515
}
@@ -84,6 +84,7 @@
8484
caption: []
8585
)
8686

87-
#let heading-multiplier = 1.2
88-
#let heading-base = 24pt
89-
#let heading-space-base = 12pt
87+
88+
#let exercise(title) = {
89+
heading(depth: 4, numbering: none, outlined: false, "Exercise: " + title)
90+
}

0 commit comments

Comments
 (0)