mirror of
https://github.com/hmemcpy/milewski-ctfp-pdf.git
synced 2024-11-23 04:15:23 +03:00
Adding \Hask command
This commit is contained in:
parent
080eaa44d3
commit
e86e4b4dc9
@ -13,4 +13,5 @@
|
||||
\newcommand{\id}{\mathbf{id}}
|
||||
\newcommand{\Ran}{\mathbf{Ran}}
|
||||
\newcommand{\Lan}{\mathbf{Lan}}
|
||||
\newcommand{\Fop}{\cat{F}^{op}}
|
||||
\newcommand{\Hask}{\mathbf{Hask}}
|
||||
\newcommand{\Fop}{\cat{F}^{op}}
|
||||
|
@ -408,7 +408,7 @@ We can write a polymorphic function from, say, \code{Op Bool} to
|
||||
predToStr (Op f) = Op (\x -> if f x then "T" else "F")
|
||||
\end{Verbatim}
|
||||
But since the two functors are not covariant, this is not a natural
|
||||
transformation in \textbf{Hask}. However, because they are both
|
||||
transformation in $\Hask$. However, because they are both
|
||||
contravariant, they satisfy the ``opposite'' naturality condition:
|
||||
|
||||
\begin{Verbatim}
|
||||
|
@ -184,7 +184,7 @@ the theoretical point of view, this is the source of never-ending
|
||||
complications, so at this point I will use my butcher's knife and
|
||||
terminate this line of reasoning. From the pragmatic point of view, it's
|
||||
okay to ignore non-terminating functions and bottoms, and treat
|
||||
\textbf{Hask} as bona fide $\Set$.\footnote{Nils Anders Danielsson,
|
||||
$\Hask$ as bona fide $\Set$.\footnote{Nils Anders Danielsson,
|
||||
John Hughes, Patrik Jansson, Jeremy Gibbons, \href{http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf}{
|
||||
Fast and Loose Reasoning is Morally Correct}. This paper provides justification for ignoring bottoms in most contexts.}
|
||||
|
||||
|
@ -170,7 +170,7 @@ produced by functions, as in:
|
||||
mappend s1 s2 = (++) s1 s2
|
||||
\end{Verbatim}
|
||||
The former translates into equality of morphisms in the category
|
||||
\textbf{Hask} (or $\Set$, if we ignore bottoms, which is the name
|
||||
$\Hask$ (or $\Set$, if we ignore bottoms, which is the name
|
||||
for never-ending calculations). Such equations are not only more
|
||||
succinct, but can often be generalized to other categories. The latter
|
||||
is called \newterm{extensional} equality, and states the fact that for any
|
||||
|
@ -209,7 +209,7 @@ pair of adjoint functors --- this factorization is not unique, though.
|
||||
|
||||
In Haskell, we use monads a lot, but only rarely factorize them into
|
||||
pairs of adjoint functors, primarily because those functors would
|
||||
normally take us out of $\cat{Hask}$.
|
||||
normally take us out of $\Hask$.
|
||||
|
||||
We can however define adjunctions of \newterm{endofunctors} in Haskell.
|
||||
Here's part of the definition taken from
|
||||
@ -423,7 +423,7 @@ We have a mapping that takes a pair of morphisms \code{p} and
|
||||
|
||||
How can we translate this into a mapping between two hom-sets that we
|
||||
need to define an adjunction? The trick is to go outside of
|
||||
\textbf{Hask} and treat the pair of morphisms as a single morphism in
|
||||
$\Hask$ and treat the pair of morphisms as a single morphism in
|
||||
the product category.
|
||||
|
||||
Let me remind you what a product category is. Take two arbitrary
|
||||
|
@ -95,9 +95,9 @@ this value is not explicitly needed (for instance, to be pattern
|
||||
matched, or produced as output), it may be passed around without
|
||||
stalling the execution of the program. Because every Haskell function
|
||||
may be potentially non-terminating, all types in Haskell are assumed to
|
||||
be lifted. This is why we often talk about the category $\cat{Hask}$ of
|
||||
be lifted. This is why we often talk about the category $\Hask$ of
|
||||
Haskell (lifted) types and functions rather than the simpler
|
||||
$\Set$. It is not clear, though, that $\cat{Hask}$ is a real
|
||||
$\Set$. It is not clear, though, that $\Hask$ is a real
|
||||
category (see this
|
||||
\urlref{http://math.andrej.com/2016/08/06/hask-is-not-a-category/}{Andrej
|
||||
Bauer post}).
|
||||
|
@ -56,7 +56,7 @@ endofunctors).
|
||||
The component of this natural transformation at an object $a$ is
|
||||
the morphism:
|
||||
\[\mu_a \Colon T (T a) \to T a\]
|
||||
which, in $\cat{Hask}$, translates directly to our definition of
|
||||
which, in $\Hask$, translates directly to our definition of
|
||||
\code{join}.
|
||||
|
||||
$\eta$ is a natural transformation between the identity functor $I$
|
||||
|
Loading…
Reference in New Issue
Block a user