diff --git a/.github/workflows/build-pdf.yml b/.github/workflows/build-pdf.yml index abdb48dda..7e3a6a7ec 100644 --- a/.github/workflows/build-pdf.yml +++ b/.github/workflows/build-pdf.yml @@ -30,7 +30,7 @@ jobs: id: full-pdf uses: docker://winitzki/sofp-docker-build:latest with: - args: "LYXDIR=/root/.lyx bash sofp-src/scripts/make_all.sh" + args: "LYXDIR=/root/.lyx bash sofp-src/make_sofp_pdf.sh" - name: Upload built PDF id: upload-pdf diff --git a/sofp-src/lyx/sofp-free-type.lyx b/sofp-src/lyx/sofp-free-type.lyx index 82ec9f05a..c46778689 100644 --- a/sofp-src/lyx/sofp-free-type.lyx +++ b/sofp-src/lyx/sofp-free-type.lyx @@ -34778,15 +34778,7 @@ recursive status open \begin_layout Plain Layout -This -\begin_inset Quotes eld -\end_inset - -Church encoding -\begin_inset Quotes erd -\end_inset - - is known more precisely as +The \begin_inset Quotes eld \end_inset @@ -34794,9 +34786,7 @@ Boehm-Berarducci encoding \begin_inset Quotes erd \end_inset -. - For the purposes of this book, they are the same. - See + discussed in \family typewriter \begin_inset CommandInset href @@ -34808,7 +34798,7 @@ literal "false" \family default - for discussion. + can be seen as a curried form of the Church encoding. \end_layout \end_inset @@ -34910,18 +34900,10 @@ noprefix "false" \begin_layout Standard The following statement \begin_inset Foot -status collapsed +status open \begin_layout Plain Layout See also the papers -\begin_inset Quotes eld -\end_inset - -A note on strong dinaturality -\begin_inset Quotes erd -\end_inset - - ( \family typewriter \begin_inset CommandInset href @@ -34934,15 +34916,7 @@ literal "false" \family default -) and -\begin_inset Quotes eld -\end_inset - -Build, augment, and destroy universally -\begin_inset Quotes erd -\end_inset - - ( + and \family typewriter \begin_inset CommandInset href @@ -34954,7 +34928,7 @@ literal "false" \family default -). +. \end_layout \end_inset @@ -35241,6 +35215,26 @@ fix \end_inset +Omitting type annotations, we may write +\begin_inset listings +inline true +status open + +\begin_layout Plain Layout + +fix +\end_layout + +\end_inset + + as: +\begin_inset Formula +\[ +\text{fix}\triangleq f\rightarrow\,^{Y}\rightarrow q\rightarrow f\triangleright(p\rightarrow q\triangleright p^{Y})^{\uparrow F}\bef q\quad. +\] + +\end_inset + \end_layout @@ -35537,7 +35531,8 @@ It remains to verify that the last line holds. \begin_inset Formula \begin{align*} & \text{fix}^{\uparrow F}\bef f\overset{?}{=}f^{\uparrow F}\bef q\quad,\\ -\text{or equivalently}:\quad & \text{fix}^{\uparrow F}\bef\big(p^{:\forall X.\,(F^{X}\rightarrow X)\rightarrow X}\rightarrow q\triangleright p^{Y}\big)^{\uparrow F}\bef q\overset{?}{=}\big(p^{:\forall X.\,(F^{X}\rightarrow X)\rightarrow X}\rightarrow q\triangleright p^{Y}\big)^{\uparrow F\uparrow F}\bef q^{\uparrow F}\bef q\quad. +\text{or equivalently}:\quad & \text{fix}^{\uparrow F}\bef\big(p^{:\forall X.\,(F^{X}\rightarrow X)\rightarrow X}\rightarrow q\triangleright p^{Y}\big)^{\uparrow F}\bef q\\ + & \quad\overset{?}{=}\big(p^{:\forall X.\,(F^{X}\rightarrow X)\rightarrow X}\rightarrow q\triangleright p^{Y}\big)^{\uparrow F\uparrow F}\bef q^{\uparrow F}\bef q\quad. \end{align*} \end_inset @@ -35656,27 +35651,75 @@ noprefix "false" \begin_inset Formula $f$ \end_inset - by + by: \begin_inset Formula \[ -r\triangleq\text{fix}^{\uparrow F}\quad,\quad\quad f\triangleq u^{:F^{T}}\rightarrow s\triangleright(u\triangleright\text{fix})\quad. +r\triangleq\text{fix}^{\uparrow F}\quad,\quad\quad f\triangleq u^{:F^{T}}\rightarrow s\triangleright(u\triangleright\text{fix})^{B}\quad. \] \end_inset +Substituting the definition of +\begin_inset listings +inline true +status open + +\begin_layout Plain Layout + +fix +\end_layout + +\end_inset + +, we get a simplified formula for +\begin_inset Formula $f$ +\end_inset + +: +\begin_inset Formula +\begin{align*} + & f=u^{:F^{T}}\rightarrow s\triangleright(u\triangleright\text{fix})^{B}\\ + & =u^{:F^{T}}\rightarrow u\triangleright(q^{:\forall X.\,(F^{X}\rightarrow X)\rightarrow X}\rightarrow s\triangleright q^{B})^{\uparrow F}\bef s\\ + & =(q^{:\forall X.\,(F^{X}\rightarrow X)\rightarrow X}\rightarrow s\triangleright q^{B})^{\uparrow F}\bef s\quad. +\end{align*} + +\end_inset + It remains to verify that the assumption of the strong dinaturality law holds: \begin_inset Formula \begin{align*} & r\bef f\overset{?}{=}f^{\uparrow F}\bef s\quad,\\ -\text{or equivalently}:\quad & \text{fix}^{\uparrow F}\bef(u\rightarrow s\triangleright(u\triangleright\text{fix}))\overset{?}{=}\big(u^{:F^{T}}\rightarrow s\triangleright(u\triangleright\text{fix})\big)^{\uparrow F}\bef s\quad. +\text{or equivalently}:\quad & \text{fix}^{\uparrow F}\bef(q\rightarrow s\triangleright q^{B})^{\uparrow F}\bef s\overset{?}{=}f^{\uparrow F}\bef s\quad. \end{align*} \end_inset +To prove the last equation, it is sufficient to prove that: +\begin_inset Formula +\[ +\text{fix}\bef(q\rightarrow s\triangleright q^{B})=f\quad. +\] + +\end_inset + Rewrite the left-hand side above until it becomes equal to the right-hand side: \begin_inset Formula +\begin{align*} + & \text{fix}\bef(q\rightarrow s\triangleright q^{B})\\ + & =(u^{:F^{T}}\rightarrow u\triangleright\text{fix})\bef(q\rightarrow s\triangleright q^{B})\\ + & =u^{:F^{T}}\rightarrow s\triangleright(u\triangleright\text{fix})^{B}=f. +\end{align*} + +\end_inset + + +\begin_inset Note Note +status collapsed + +\begin_layout Plain Layout +\begin_inset Formula \begin{align*} & \text{fix}^{\uparrow F}\bef(u\rightarrow s\triangleright(u\triangleright\text{fix}))=(u^{:F^{F^{T}}}\rightarrow u\triangleright\text{fix}^{\uparrow F})\bef(u\rightarrow s\triangleright(u\triangleright\text{fix}))\\ \text{compute composition}:\quad & =u\rightarrow s\triangleright(u\triangleright\text{fix}^{\uparrow F}\triangleright\gunderline{\text{fix}})=\gunderline{u\rightarrow u\,\triangleright}\,\text{fix}^{\uparrow F}\triangleright(q\rightarrow s\triangleright q)^{\uparrow F}\bef s\\ @@ -35686,6 +35729,11 @@ Rewrite the left-hand side above until it becomes equal to the right-hand \end_inset + +\end_layout + +\end_inset + The two sides are now equal. \begin_inset Formula $\square$ diff --git a/sofp-src/lyx/sofp-transformers.lyx b/sofp-src/lyx/sofp-transformers.lyx index 7b597ce7b..1195c40be 100644 --- a/sofp-src/lyx/sofp-transformers.lyx +++ b/sofp-src/lyx/sofp-transformers.lyx @@ -586,9 +586,8 @@ n[Int]] everywhere. \end_inset -The type constructor forces us to use pattern matching with nested functor - blocks, since that is the only way of getting access to values of type - +We are forced to use pattern matching with nested functor blocks, since + that is the only way of getting access to values of type \begin_inset listings inline true status open @@ -2474,31 +2473,31 @@ Solution \end_layout \begin_layout Standard -There is no lawful +The type constructor \begin_inset listings inline true status open \begin_layout Plain Layout -flatMap +Option[State[S, A]] \end_layout \end_inset - function for the type constructor + has no lawful \begin_inset listings inline true status open \begin_layout Plain Layout -Option[State[S, A]] +flatMap \end_layout \end_inset -: + function: \begin_inset listings inline false status open @@ -4561,7 +4560,7 @@ noprefix "false" \end_layout \begin_layout Standard -The type constructors for monad transformers are conventionally named +The type constructors for monad transformers are usually named as \begin_inset listings inline true status open @@ -4733,8 +4732,8 @@ implicit class ReaderTBaseLift[M[_]: Monad : Functor, R, A](t: R => A) { The lifts are written in the code notation as: \begin_inset Formula \begin{align*} -\text{foreign lift}:\quad & \text{flift}:M^{A}\rightarrow T_{\text{Reader}}^{M,A}\quad, & \text{flift}\,(m^{:M^{A}})\triangleq\_^{:R}\rightarrow m=\text{pu}_{\text{Reader}}(m)\quad,\quad~\\ -\text{base lift}:\quad & \text{blift}:(R\rightarrow A)\rightarrow T_{\text{Reader}}^{M,A}\quad, & \text{blift}\,(t^{:R\rightarrow A})\triangleq r^{:R}\rightarrow\text{pu}_{M}(t(r))=t\bef\text{pu}_{M}\quad. +\text{foreign lift}:\quad & \text{flift}:M^{A}\rightarrow T_{\text{Reader}}^{M,A}\quad,\quad\quad\text{flift}\,(m^{:M^{A}})\triangleq\_^{:R}\rightarrow m=\text{pu}_{\text{Reader}}(m)\quad,\\ +\text{base lift}:\quad & \text{blift}:(R\rightarrow A)\rightarrow T_{\text{Reader}}^{M,A}\quad,\quad\quad\text{blift}\,(t^{:R\rightarrow A})\triangleq t\bef\text{pu}_{M}\quad. \end{align*} \end_inset @@ -5154,10 +5153,11 @@ Writer 's flatten methods: \begin_inset Formula \begin{align*} -\text{ftn}_{T}\big(t^{:M^{M^{A\times W}\times W}}\big) & =t\triangleright(m^{:M^{A\times W}}\times w^{:W}\rightarrow m\triangleright(p^{:A\times W}\rightarrow p\times w)^{\uparrow M})^{\uparrow M}\triangleright\text{ftn}_{M}\triangleright(\text{ftn}_{\text{Writer}})^{\uparrow M}\quad,\\ -\text{ftn}_{T} & =(m^{:M^{A\times W}}\times w^{:W}\rightarrow m\triangleright(p^{:A\times W}\rightarrow p\times w)^{\uparrow M})^{\uparrow M}\bef\text{ftn}_{M}\bef(\text{ftn}_{\text{Writer}})^{\uparrow M}\\ - & =\text{flm}_{M}(m\times w\rightarrow m\triangleright(p\rightarrow p\times w)^{\uparrow M}\bef\text{ftn}_{\text{Writer}}^{\uparrow M})\\ - & =\text{flm}_{M}(m\times w\rightarrow m\triangleright(a\times w_{2}\rightarrow a\times(w\oplus w_{2})))\quad. + & \text{ftn}_{T}\big(t^{:M^{M^{A\times W}\times W}}\big)\\ + & \quad=t\triangleright(m^{:M^{A\times W}}\times w^{:W}\rightarrow m\triangleright(p^{:A\times W}\rightarrow p\times w)^{\uparrow M})^{\uparrow M}\triangleright\text{ftn}_{M}\triangleright(\text{ftn}_{\text{Writer}})^{\uparrow M}\quad,\\ + & \text{ftn}_{T}=(m^{:M^{A\times W}}\times w^{:W}\rightarrow m\triangleright(p^{:A\times W}\rightarrow p\times w)^{\uparrow M})^{\uparrow M}\bef\text{ftn}_{M}\bef(\text{ftn}_{\text{Writer}})^{\uparrow M}\\ + & \quad=\text{flm}_{M}(m\times w\rightarrow m\triangleright(p\rightarrow p\times w)^{\uparrow M}\bef\text{ftn}_{\text{Writer}}^{\uparrow M})\\ + & \quad=\text{flm}_{M}(m\times w\rightarrow m\triangleright(a\times w_{2}\rightarrow a\times(w\oplus w_{2})))\quad. \end{align*} \end_inset diff --git a/sofp-src/tex/chapter3-picture.pdf b/sofp-src/tex/chapter3-picture.pdf index 706c13201..b12eb0bcc 100644 Binary files a/sofp-src/tex/chapter3-picture.pdf and b/sofp-src/tex/chapter3-picture.pdf differ diff --git a/sofp-src/tex/sofp.tex b/sofp-src/tex/sofp.tex index 0aa67999b..4e4988e23 100644 --- a/sofp-src/tex/sofp.tex +++ b/sofp-src/tex/sofp.tex @@ -321,8 +321,8 @@ {\footnotesize{}ISBN: 978-0-359-76877-6}\\ \\ {\scriptsize{}Source hash (sha256): cbd327cf5baeac2e9d58471a6d010dc2c542ea70d4d5c5a4c4c8ce793c5a5b43}\\ -{\scriptsize{}Git commit: 195c1f1251605e0eba92ac033f93ee2d0acaf5ef}\\ -{\scriptsize{}PDF file built on Sat, 04 May 2024 21:11:14 +0200 by pdfTeX 3.141592653-2.6-1.40.25 (TeX Live 2023) on Darwin}\\ +{\scriptsize{}Git commit: 35ba0d9120711fb25927dc04d722f92824b93408}\\ +{\scriptsize{}PDF file built on Sat, 04 May 2024 21:18:10 +0200 by pdfTeX 3.141592653-2.6-1.40.25 (TeX Live 2023) on Darwin}\\ ~\\ {\scriptsize{}Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License,