Skip to content

Commit

Permalink
finish solved examples for chapter 7
Browse files Browse the repository at this point in the history
  • Loading branch information
winitzki committed Sep 20, 2019
1 parent 1d02a3b commit 0942c63
Showing 1 changed file with 39 additions and 2 deletions.
41 changes: 39 additions & 2 deletions sofp-src/sofp-typeclasses.lyx
Original file line number Diff line number Diff line change
Expand Up @@ -22344,12 +22344,49 @@ Can we recognize a pointed contrafunctor
by looking at its type expression, e.g.
\begin_inset Formula
\[
C^{A,B}\triangleq\left(\bbnum 1+A\Rightarrow\text{Int}\right)+(\text{String}\times A\times A\Rightarrow\text{String})\quad?
C^{A}\triangleq\left(\bbnum 1+A\Rightarrow\text{Int}\right)+(\text{String}\times A\times A\Rightarrow\text{String})\quad?
\]

\end_inset

We ***
We need to set the type parameter to
\begin_inset Formula $\bbnum 1$
\end_inset

and try to create a value of type
\begin_inset Formula $C^{\bbnum 1}$
\end_inset

.
For this example:
\begin_inset Formula
\[
C^{\bbnum 1}=\left(\bbnum 1+\bbnum 1\Rightarrow\text{Int}\right)+(\text{String}\times\bbnum 1\times\bbnum 1\Rightarrow\text{String})\quad.
\]

\end_inset

We can certainly create values of this type, e.g.
\begin_inset space ~
\end_inset

a constant function returning an integer
\begin_inset Formula $123$
\end_inset

:
\begin_inset Formula
\[
\text{wu}_{C}\triangleq(\_^{:\bbnum 1+\bbnum 1}\Rightarrow123)+\bbnum 0\quad.
\]

\end_inset

So, the contrafunctor
\begin_inset Formula $C$
\end_inset

is pointed.
\end_layout

\begin_layout Section
Expand Down

0 comments on commit 0942c63

Please sign in to comment.