L

Mapping between the course and the book

Short version: study week N = book chapter N.

More details below.

Week 1 lecture videos:

video short-hands: Lw.l.p is week w, lecture l, part p The l=0 case are the “extra lectures on Haskell”.

L1.2.4	38:20	Types	§1.2
L1.0.1	00:00	TDD: id, const, (.)	§1.2
L1.0.2	00:00	(,), swap, fst	§1.2
L1.0.2	10:58	tupling transform	§1.2
L1.0.3	00:00	Either, Left, Right	§1.2
L1.0.3	04:12	either, patterns	§1.2
L1.1.1	00:00	L1.1 Course admin
L1.1.1	18:00	DSL definition	§1.1.1
L1.1.1	20:00	Jamboard examples	§1.7
L1.1.1	25:00	“the function f(x)”	§1.7
L1.1.1	27:00	Types	§1.1
L1.1.1	31:00	enum Bool->Bool	§1.1.2
L1.1.2	00:00	Haskell intro	§1.2
L1.1.2	05:20	enum Bool->Bool	§1.1.2
L1.1.2	09:50	floating point	§1.1.3
L1.1.2	15:00	Associative law	§1.6
L1.1.2	18:47	DSL for expressions	§1.2
L1.1.2	26:30	Expr. of one var.	§1.7
L1.1.2	43:00	TA intr. themselves
L1.2.1	00:00	L1.2 Course admin
L1.2.2	00:00	N->Z->Q->R->C
L1.2.3	01:00	Live code complex	§1.4
L1.2.4	00:00	Complex cont.	§1.4
L1.2.4	02:57	Eq check + deriving	§1.4
L1.2.4	14:18	DSL complex	§1.5

Week 2 lecture videos:

L2.1.4	12:35	lift2 and friends	§1.3
L2.1.1	00:00	L2.1 admin	§2
L2.1.2	00:00	Propositional Calculus	§2.1
L2.1.2	03:20	Truth table for (=>)	§2.1.2
L2.1.2	06:24	Truth tab. swap	§2.1.2
L2.1.2	10:30	Tautology	§2.1.2
L2.1.2	13:37	data Prop, eval start	§2.1.1
L2.1.2	26:08	AndIntro, OrIntroL	§2.1.3
L2.1.2	30:06	fst, snd, orElim	§2.1.6
L2.1.3	00:00	Pure set theory	§2.3
L2.1.3	08:49	union, card examples	§2.3
L2.1.3	17:05	union computation table	§2.3
L2.1.4	00:00	live coding Prop, eval	§2.1
L2.1.4	03:40	impl. eval without Name	§2.1
L2.1.4	07:21	eval: adding Name case	§2.1
L2.2.1	00:00	First Order Logic	§2.2
L2.2.1	04:29	FOL predicate examples	§2.2
L2.2.1	08:39	Quantifiers	§2.2.2
L2.2.1	15:38	data FOL, data Dom	§2.2
L2.2.1	21:38	GADTs extension mention	§2.2
L2.2.1	23:00	Interpret FOL-syntax	§2.2
L2.2.1	27:48	Typed quantifiers	§2.2.4
L2.2.1	32:58	de Morgan, not quant.	§2.2.4
L2.2.2	00:00	Proof by contradiction	§2.4.1
L2.2.2	14:34	Proof by cases	§2.4.2
L2.2.3	00:00	Live code: proof terms	§2.1.5
L2.2.3	08:38	inhabited types are Tru	§2.1.6
L2.2.3	13:02	Or p q => Or q p	§2.1.6
L2.2.3	15:18	Not(Not(Or p (Not p)))	§2.1.7
L2.3.1	00:00	Prop and its eval	§2.1.1
L2.3.1	03:16	data Proof + checkProof	§2.1.3
L2.3.1	09:06	checkProof examples	§2.1.4

Week 3 lecture videos:

L3.3.1	25:51	numeric instances for functions	§3.5.3
L3.1.1	00:00	Limit of function	§2.5.3
L3.1.1	06:01	Scope check lim logic	§2.5.3
L3.1.2	00:00	Lim properties and types	§3.1
L3.1.2	10:30	Deriv. of function	§3.1
L3.1.3	00:00	Deriv. examples	§3.1
L3.1.3	05:00	D (^2) = (2*)	§3.1
L3.1.3	12:12	D (f + g) = D f + D g	§3.1
L3.1.4	00:00	Live coding deriv in Haskell	§3.6
L3.1.4	07:41	deriv :: FunExp -> FunExp	§3.6
L3.2.1	00:00	Lecture 3.2 admin
L3.2.2	00:00	Partial derivatives quote	§3.2
L3.2.2	13:01	Partial derivatives types	§3.4,§3.2
L3.2.2	25:26	Expressions, functions, notation	§3.2
L3.2.2	30:48	Partial derivatives examples	§3.2
L3.2.3	00:00	Lagrangian case study	§3.3
L3.2.3	21:51	Lagrangian example	§3.3
L3.2.4	00:00	Haskell type classes in general	§3.5
L3.2.4	04:41	class Additive, Double, FunExp	§3.5
L3.3.1	00:00	data FunExp, eval, R->R	§3
L3.3.1	04:45	deriv :: FunExp -> FunExp	§3.6
L3.3.1	17:20	class Additive, Multiplicative	§3.5

Week 4 lecture videos:

L4.3.2	00:00	Live coding Monoid, Ring, Field	§4.1
L4.1.1	00:00	Homomorphisms, H2, H1, H0	§4.2
L4.1.2	00:00	Example: H2(odd,+,xor)	§4.3.1
L4.1.2	17:50	not Exists op. H2(isPrime,+,op)	§4.3.2
L4.1.3	00:00	Live coding H2(h,(+),(*))	§4.3
L4.1.4	00:00	Compositional semantics & Folds	§4.3
L4.1.4	07:24	fold for integer expressions	§4.4
L4.1.4	16:06	Define your own equality	§4.4
L4.1.4	18:59	evenIE as a fold instance	§4.4
L4.1.5	00:00	Make your own type class	§4.4
L4.2.1	00:00	Prove deriv is not a homomorphism	§4.6
L4.2.1	13:40	Core of the proof by contradiction	§4.6
L4.2.2	00:00	tupling: der2 : F -> (F, F)	§4.6
L4.2.3	00:00	live coding der2, tupling transform	§4.6
L4.2.3	08:30	der2 :: F -> Bi F; homomorphism	§4.6
L4.2.3	19:27	type class for FunExp + instances	§4.5
L4.3.1	00:00	Structural homomorphism	§4.2

Week 5 lecture videos:

L5.2.5	00:00	Power Series, deriv, integ, exp example	§5.6
L5.1.1	00:00	Live coding applyFD	§4.6.1
L5.1.1	21:43	Bi a = (pos, speed)	§4.6.1
L5.1.1	27:31	equational reasoning: mulBi from mulFD	§4.6.1
L5.1.2	00:00	Polynomials: types + eval + examples	§5.1
L5.1.2	00:00	Chebyshev polynomials	§5.1
L5.1.3	00:00	Polynomials and homomorphisms	§5.1
L5.1.3	00:00	Equational reasoning (eval for Poly (+))	§5.1
L5.2.1	00:00	Is degree maybe a homomorphism?	§5.2, §5.3
L5.2.2	00:00	Polynomial division	§5.4, §5.5
L5.2.3	00:00	Live coding polynomials: types, eval	§5.1
L5.2.4	00:00	Coding the polynomial Ring in Haskell	§5.1

Week 6 lecture videos:

L6.2.2	00:00	Power series transform in Haskell	§6.4
L6.1.1	00:00	Power Series and Ordinary Differential Equations	§6.4
L6.1.2	00:00	Power Series transform for solving ODEs	§6.4
L6.1.3	00:00	Taylor & Maclaurin series	§6.1&§6.3
L6.1.4	00:00	Live coding: Power Series reminder	§6.3
L6.1.4	12:25	Specification + type of “derivative series”	§6.1
L6.1.4	19:11	Implement derDS, integDS, xDS, etc.	§6.2
L6.1.4	32:51	Implement mulDS (for “derivative series”)	§6
L6.2.1	00:00	FunExp special: fromRational . toRational	§6.6
L6.2.1	03:30	FunExp recap: the Transcendental part	§6.6
L6.2.1	13:20	Generic evaluator example: exp (-x²)	§6.6
L6.2.1	17:30	derivative series Transcendental instances	§6.5

Week 7 lecture videos: [guest lectures by Nicola Botta]

Week 8 lecture videos:

L8.2.3	00:00	DSLsofMath course / book overview	DSLM
L8.1.1	00:00	Towards the Laplace transform	§8.2
L8.1.2	00:00	Laplace of exp, sin, cos	§8.2.1
L8.1.3	00:00	Laplace transform solving an ODE	§8.2
L8.2.1	00:00	Live coding Complex, e^ix = cos x + i*sin x	§8.1
L8.2.2	00:00	Laplace cos from exp, math. notation, FunExp	§8.4

1. Types, Functions, and DSLs for Expressions (7-42)

The whole chapter is included in the course.
(Some of the material is also parts of the prerequisites.)

1.1 Types of data and functions {p8}

L1.1.1	27:00	Types	§1.1
L1.1.1	18:00	DSL definition	§1.1.1
L1.1.1	31:00	enum Bool->Bool	§1.1.2
L1.1.2	05:20	enum Bool->Bool	§1.1.2
L1.1.2	09:50	floating point	§1.1.3

1.2 Types in Haskell: type, newtype, and data {p14}

L1.0.1	00:00	TDD: id, const, (.)	§1.2
L1.0.2	00:00	(,), swap, fst	§1.2
L1.0.2	10:58	tupling transform	§1.2,1.8
L1.0.3	00:00	Either, Left, Right	§1.2
L1.0.3	04:12	either, patterns	§1.2
L1.1.2	00:00	Haskell intro	§1.2
L1.1.2	18:47	DSL for expressions	§1.2
L1.2.4	38:20	Types	§1.2

1.3 Notation and abstract syntax for sequences {p16}

Included in the course but not presented in a week 1 lecture.

L2.1.4

12:35

lift2 and friends

§1.3

1.4 A DSL of complex numbers {p18}

L1.2.3	01:00	Live code complex	§1.4
L1.2.4	00:00	Complex cont.	§1.4
L1.2.4	02:57	Eq check + deriving	§1.4

1.5 A syntax for (complex) arithmetical expressions {p24}

L1.2.4

14:18

DSL complex

§1.5

1.6 Laws, properties and testing {p26}

The section is included in the course but only partly presented in the lectures.

L1.1.2

15:00

Associative law

§1.6

1.7 Types of functions, expressions and operators {p29}

L1.1.1	20:00	Jamboard examples	§1.7
L1.1.1	25:00	“the function f(x)”	§1.7
L1.1.2	26:30	Expr. of one var.	§1.7

2. DSLs for logic and proofs (43-80)

L2.1.1

00:00

L2.1 admin

§2

2.1 Propositional Calculus {p43}

L2.1.2	00:00	Propositional Calculus	§2.1
L2.1.4	00:00	live coding Prop, eval	§2.1
L2.1.4	03:40	impl. eval without Name	§2.1
L2.1.4	07:21	eval: adding Name case	§2.1
L2.1.2	13:37	data Prop, eval start	§2.1.1
L2.3.1	00:00	Prop and its eval	§2.1.1
L2.1.2	03:20	Truth table for (=>)	§2.1.2
L2.1.2	06:24	Truth tab. swap	§2.1.2
L2.1.2	10:30	Tautology	§2.1.2
L2.1.2	26:08	AndIntro, OrIntroL	§2.1.3
L2.3.1	03:16	data Proof + checkProof	§2.1.3
L2.3.1	09:06	checkProof examples	§2.1.4
L2.2.3	00:00	Live code: proof terms	§2.1.5
L2.1.2	30:06	fst, snd, orElim	§2.1.6
L2.2.3	08:38	inhabited types are Tru	§2.1.6
L2.2.3	13:02	Or p q => Or q p	§2.1.6
L2.2.3	15:18	Not(Not(Or p (Not p)))	§2.1.7

2.2 First Order Logic {p57}

L2.2.1	00:00	First Order Logic	§2.2
L2.2.1	04:29	FOL predicate examples	§2.2
L2.2.1	15:38	data FOL, data Dom	§2.2
L2.2.1	21:38	GADTs extension mention	§2.2
L2.2.1	23:00	Interpret FOL-syntax	§2.2
L2.2.1	08:39	Quantifiers	§2.2.2
L2.2.1	27:48	Typed quantifiers	§2.2.4
L2.2.1	32:58	de Morgan, not quant.	§2.2.4

2.3 An aside: Pure set theory {p64}

L2.1.3	00:00	Pure set theory	§2.3
L2.1.3	08:49	union, card examples	§2.3
L2.1.3	17:05	union computation table	§2.3

2.4 Example proofs: contradiction, cases, primes {p66}

L2.2.2	00:00	Proof by contradiction	§2.4.1
L2.2.2	14:34	Proof by cases	§2.4.2

2.5 Basic concepts of calculus {p69}

L3.1.1	00:00	Limit of function	§2.5.3
L3.1.1	06:01	Scope check lim logic	§2.5.3

2.6 Exercises {p75}

3. Types in Mathematics (81-100)

L3.3.1

00:00

data FunExp, eval, R->R

§3

3.1 Typing Mathematics: derivative of a function {p81}

L3.1.2	00:00	Lim properties and types	§3.1
L3.1.2	10:30	Deriv. of function	§3.1
L3.1.3	00:00	Deriv. examples	§3.1
L3.1.3	05:00	D (^2) = (2*)	§3.1
L3.1.3	12:12	D (f + g) = D f + D g	§3.1

3.2 Typing Mathematics: partial derivative {p82}

L3.2.2	00:00	Partial derivatives quote	§3.2
L3.2.2	13:01	Partial derivatives types	§3.2
L3.2.2	25:26	Expressions, functions, notation	§3.2
L3.2.2	30:48	Partial derivatives examples	§3.2

3.3 Typing Mathematics: Lagrangian case study {p85}

L3.2.3	00:00	Lagrangian case study	§3.3
L3.2.3	21:51	Lagrangian example	§3.3

3.4 Incremental analysis with types {p88}

L3.2.2

13:01

Partial derivatives types

§3.4,§3.2

3.5 Type classes {p90}

L3.2.4	00:00	Haskell type classes	§3.5
L3.2.4	04:41	class Additive, Double, FunExp	§3.5
L3.3.1	17:20	class Additive, Multiplicative	§3.5
L3.3.1	25:51	numeric instances for functions	§3.5.3

3.6 Computing derivatives {p95}

L3.1.4	00:00	Live coding deriv in Haskell	§3.6
L3.1.4	07:41	deriv :: FunExp -> FunExp	§3.6
L3.3.1	04:45	cont. deriv :: FunExp -> FunExp	§3.6

3.7 Exercises {p98}

4. Compositionality and Algebras (101-140)

4.1 Algebraic Structures {p102}

L4.3.2

00:00

Live coding Monoid, Ring, Field

§4.1

4.2 Homomorphisms {p105}

L4.1.1	00:00	Homomorphisms, H2, H1, H0	§4.2
L4.3.1	00:00	Structural homomorphism	§4.2

4.3 Compositional semantics {p109}

L4.1.2	00:00	Example: H2(odd,+,xor)	§4.3.1
L4.1.2	17:50	not Exists op. H2(isPrime,+,op)	§4.3.2
L4.1.3	00:00	Live coding H2(h,(+),(*))	§4.3
L4.1.4	00:00	Compositional semantics & Folds	§4.3

4.4 Folds {p111}

L4.1.4	07:24	fold for integer expressions	§4.4
L4.1.4	16:06	Define your own equality	§4.4
L4.1.4	18:59	evenIE as a fold instance	§4.4
L4.1.5	00:00	Make your own type class	§4.4

4.5 Initial and Free Structures {p116}

L4.2.3

19:27

type class for FunExp + instances

§4.5

4.6 Computing derivatives, reprise {p122}

L4.2.1	00:00	Prove deriv is not a homomorphism	§4.6
L4.2.1	13:40	Core of the proof by contradiction	§4.6
L4.2.2	00:00	tupling: der2 : F -> (F, F)	§4.6
L4.2.3	00:00	live coding der2, tupling transform	§4.6
L4.2.3	08:30	der2 :: F -> Bi F; homomorphism	§4.6
L5.1.1	00:00	Live coding applyFD	§4.6.1
L5.1.1	21:43	Bi a = (pos, speed)	§4.6.1
L5.1.1	27:31	equational reasoning: mulBi from mulFD	§4.6.1

4.7 Summary {p126}

4.8 Beyond Algebras: Co-algebra and the Stream calculus {p128}

4.9 A solved exercise {p129}

4.10 Exercises {p134}

5. Polynomials and Power Series (141-157)

5.1 Polynomials {p141}

L5.1.2	00:00	Polynomials: types + eval + examples	§5.1
L5.1.2	00:00	Chebyshev polynomials	§5.1
L5.1.3	00:00	Polynomials and homomorphisms	§5.1
L5.1.3	00:00	Equational reasoning (eval for Poly (+))	§5.1
L5.2.3	00:00	Live coding polynomials: types, eval	§5.1
L5.2.4	00:00	Coding the polynomial Ring in Haskell	§5.1

5.2 Division and the degree of the zero polynomial {p147}

L5.2.1

00:00

Is degree maybe a homomorphism?

§5.2, §5.3

5.3 Polynomial degree as a homomorphism {p148}

L5.2.1

00:00

Is degree maybe a homomorphism?

§5.2, §5.3

5.4 Power Series {p149}

L5.2.2

00:00

Polynomial division

§5.4, §5.5

5.5 Operations on power series {p152}

L5.2.2

00:00

Polynomial division

§5.4, §5.5

5.6 Formal derivative {p153}

L5.2.5

00:00

Power Series, deriv, integ, exp example

§5.6

5.7 Exercises {p155}

6. Taylor and Maclaurin series (158-174)

L6.1.4

32:51

Implement mulDS (for “derivative series”)

§6

6.1 Taylor series {p161}

L6.1.3	00:00	Taylor & Maclaurin series	§6.1&§6.3
L6.1.4	12:25	Specification + type of “derivative series”	§6.1

6.2 Derivatives and Integrals for Maclaurin series {p164}

L6.1.4

19:11

Implement derDS, integDS, xDS, etc.

§6.2

6.3 Integral for Formal Power series {p164}

L6.1.3	00:00	Taylor & Maclaurin series	§6.1&§6.3
L6.1.4	00:00	Live coding: Power Series reminder	§6.3

6.4 Simple differential equations {p165}

L6.1.1	00:00	Power Series and Ordinary Differential Equations	§6.4
L6.1.2	00:00	Power Series transform for solving ODEs	§6.4
L6.2.2	00:00	Power series transform in Haskell	§6.4

6.5 Exponentials and trigonometric functions {p168}

L6.2.1

17:30

derivative series Transcendental instances

§6.5

6.6 Associated code {p170}

L6.2.1	00:00	FunExp special: fromRational . toRational	§6.6
L6.2.1	03:30	FunExp recap: the Transcendental part	§6.6
L6.2.1	13:20	Generic evaluator example: exp (-x²)	§6.6

6.7 Exercises {p172}

7. Elements of Linear Algebra (175-203)

7.1 Representing vectors as functions {p178}

7.2 Linear transformations {p181}

7.3 Inner products {p184}

7.4 Examples of matrix algebra {p186}

7.5 *Monadic dynamical systems {p197}

7.6 Associated code {p200}

7.7 Exercises {p202}

8. Exponentials and Laplace (204-218)

8.1 The Exponential Function {p204}

L8.2.1

00:00

Live coding Complex, e^ix = cos x + i*sin x

§8.1

8.2 The Laplace transform {p209}

L8.1.1	00:00	Towards the Laplace transform	§8.2
L8.1.2	00:00	Laplace of exp, sin, cos	§8.2.1
L8.1.3	00:00	Laplace transform solving an ODE	§8.2

Name		Name	Last commit message	Last commit date
00		00
01		01
02		02
03		03
04		04
05		05
06		06
07		07
08		08
09		09
Appendix		Appendix
DSLsofMath		DSLsofMath
div		div
misc		misc
snapshots		snapshots
.dir-locals.el		.dir-locals.el
.gitignore		.gitignore
A2_Skeleton.lhs		A2_Skeleton.lhs
A5_landscape.patch		A5_landscape.patch
A6_landscape.patch		A6_landscape.patch
BasicConcepts.md		BasicConcepts.md
BookLogo.org		BookLogo.org
DSLMtalk.lhs		DSLMtalk.lhs
DSLsofMath.cabal		DSLsofMath.cabal
DSLsofMath.lhs		DSLsofMath.lhs
DSLsofMathBook.lhs		DSLsofMathBook.lhs
DSLsofMathNotes.lhs		DSLsofMathNotes.lhs
End.lhs		End.lhs
LICENSE		LICENSE
Makefile		Makefile
New_cuyama.jpg		New_cuyama.jpg
README.org		README.org
RecEx.md		RecEx.md
Setup.hs		Setup.hs
SolvedExercises.md		SolvedExercises.md
TestAll.lhs		TestAll.lhs
backcover.txt		backcover.txt
cabal.project.local		cabal.project.local
citations.txt		citations.txt
dslm.format		dslm.format
dslmagda.fmt		dslmagda.fmt
errata.org		errata.org
log.txt		log.txt
mapping-2016-2018.md		mapping-2016-2018.md
newunicodedefs.tex		newunicodedefs.tex
pj.bib		pj.bib
ref.bib		ref.bib
shell.nix		shell.nix
stack.yaml		stack.yaml
toc.org		toc.org

FilesExpand file tree

L

Directory actions

More options

Directory actions

More options

Latest commit

History

L

Folders and files

README.org

Mapping between the course and the book

Week 1 lecture videos:

Week 2 lecture videos:

Week 3 lecture videos:

Week 4 lecture videos:

Week 5 lecture videos:

Week 6 lecture videos:

Week 7 lecture videos: [guest lectures by Nicola Botta]

Week 8 lecture videos:

1. Types, Functions, and DSLs for Expressions (7-42)

1.1 Types of data and functions {p8}

1.2 Types in Haskell: type, newtype, and data {p14}

1.3 Notation and abstract syntax for sequences {p16}

1.4 A DSL of complex numbers {p18}

1.5 A syntax for (complex) arithmetical expressions {p24}

1.6 Laws, properties and testing {p26}

1.7 Types of functions, expressions and operators {p29}

2. DSLs for logic and proofs (43-80)

2.1 Propositional Calculus {p43}

2.2 First Order Logic {p57}

2.3 An aside: Pure set theory {p64}

2.4 Example proofs: contradiction, cases, primes {p66}

2.5 Basic concepts of calculus {p69}

2.6 Exercises {p75}

3. Types in Mathematics (81-100)

3.1 Typing Mathematics: derivative of a function {p81}

3.2 Typing Mathematics: partial derivative {p82}

3.3 Typing Mathematics: Lagrangian case study {p85}

3.4 Incremental analysis with types {p88}

3.5 Type classes {p90}

3.6 Computing derivatives {p95}

3.7 Exercises {p98}

4. Compositionality and Algebras (101-140)

4.1 Algebraic Structures {p102}

4.2 Homomorphisms {p105}

4.3 Compositional semantics {p109}

4.4 Folds {p111}

4.5 Initial and Free Structures {p116}

4.6 Computing derivatives, reprise {p122}

4.7 Summary {p126}

4.8 Beyond Algebras: Co-algebra and the Stream calculus {p128}

4.9 A solved exercise {p129}

4.10 Exercises {p134}

5. Polynomials and Power Series (141-157)

5.1 Polynomials {p141}

5.2 Division and the degree of the zero polynomial {p147}

5.3 Polynomial degree as a homomorphism {p148}

5.4 Power Series {p149}

5.5 Operations on power series {p152}

5.6 Formal derivative {p153}

5.7 Exercises {p155}

6. Taylor and Maclaurin series (158-174)

6.1 Taylor series {p161}

6.2 Derivatives and Integrals for Maclaurin series {p164}

6.3 Integral for Formal Power series {p164}

6.4 Simple differential equations {p165}

6.5 Exponentials and trigonometric functions {p168}

6.6 Associated code {p170}

6.7 Exercises {p172}

7. Elements of Linear Algebra (175-203)

7.1 Representing vectors as functions {p178}

7.2 Linear transformations {p181}

7.3 Inner products {p184}

7.4 Examples of matrix algebra {p186}

7.5 *Monadic dynamical systems {p197}

7.6 Associated code {p200}

7.7 Exercises {p202}

8. Exponentials and Laplace (204-218)

8.1 The Exponential Function {p204}