Code snippets refactoring (#148)

* Tweaking relative paths + spaces in filenames
* Extracting code snippets to external files
* Adding a missing package to nix script
This commit is contained in:
Igal Tabachnik 2018-10-01 00:03:52 +03:00 committed by GitHub
parent 2d058ce702
commit 2a4b681cf5
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
511 changed files with 1463 additions and 1843 deletions

View File

@ -30,11 +30,15 @@ mkShell {
subfiles
lettrine
upquote
libertine
mweights
fontaxes
mdframed
needspace
xifthen
currfile
noindentafter
ifmtarg
scheme-medium
listings
minted

View File

@ -48,6 +48,6 @@ copy:
clean:
rm -f *~ *.aux {ctfp-*}.{out,log,pdf,dvi,fls,fdb_latexmk,aux,brf,bbl,idx,ilg,ind,toc,sed}
rm -rf _minted-ctfp
rm -rf _minted-*
if which latexmk > /dev/null 2>&1 ; then latexmk -CA; fi
rm -rf ../out

View File

@ -1,3 +1,5 @@
% !TEX root = ../../ctfp-reader.tex
\lettrine[lhang=0.17]{A}{category} is an embarrassingly simple concept.
A category consists of \newterm{objects} and \newterm{arrows} that go between them. That's
why categories are so easy to represent pictorially. An object can be
@ -66,19 +68,13 @@ Library that takes two functions and returns their composition, but
there isn't one. So let's try some Haskell for a change. Here's the
declaration of a function from A to B:
\begin{Verbatim}
f :: A -> B
\end{Verbatim}
\src{code/haskell/snippet01.hs}
Similarly:
\begin{Verbatim}
g :: B -> C
\end{Verbatim}
\src{code/haskell/snippet02.hs}
Their composition is:
\begin{Verbatim}
g . f
\end{Verbatim}
\src{code/haskell/snippet03.hs}
Once you see how simple things are in Haskell, the inability to express
straightforward functional concepts in C++ is a little embarrassing. In
fact, Haskell will let you use Unicode characters so you can write
@ -111,12 +107,7 @@ expressed as:
\[h \circ (g \circ f) = (h \circ g) \circ f = h \circ g \circ f\]
In (pseudo) Haskell:
\begin{Verbatim}
f :: A -> B
g :: B -> C
h :: C -> D
h . (g . f) == (h . g) . f == h . g . f
\end{Verbatim}
\src{code/haskell/snippet04.hs}
(I said ``pseudo,'' because equality is not defined for functions.)
Associativity is pretty obvious when dealing with functions, but it may
@ -148,10 +139,7 @@ reference, by const reference, by move, and so on).
In Haskell, the identity function is part of the standard library
(called Prelude). Here's its declaration and definition:
\begin{Verbatim}
id :: a -> a
id x = x
\end{Verbatim}
\src{code/haskell/snippet05.hs}
As you can see, polymorphic functions in Haskell are a piece of cake. In
the declaration, you just replace the type with a type variable. Here's
the trick: names of concrete types always start with a capital letter,
@ -176,10 +164,7 @@ This concludes our second Haskell lesson.
The identity conditions can be written (again, in pseudo-Haskell) as:
\begin{Verbatim}
f . id == f
id . f == f
\end{Verbatim}
\src{code/haskell/snippet06.hs}
You might be asking yourself the question: Why would anyone bother with
the identity function --- a function that does nothing? Then again, why
do we bother with the number zero? Zero is a symbol for nothing. Ancient

View File

@ -0,0 +1 @@
f :: A -> B

View File

@ -0,0 +1 @@
g :: B -> C

View File

@ -0,0 +1 @@
g . f

View File

@ -0,0 +1,4 @@
f :: A -> B
g :: B -> C
h :: C -> D
h . (g . f) == (h . g) . f == h . g . f

View File

@ -0,0 +1,2 @@
id :: a -> a
id x = x

View File

@ -0,0 +1,2 @@
f . id == f
id . f == f

View File

@ -1,3 +1,5 @@
% !TEX root = ../../ctfp-reader.tex
\lettrine[lhang=0.17]{W}{e talked about} functors as mappings between categories that preserve
their structure.
@ -150,16 +152,12 @@ alpha\textsubscript{a} :: F a -> G a
A natural transformation is a polymorphic function that is defined for
all types \code{a}:
\begin{Verbatim}
alpha :: forall a . F a -> G a
\end{Verbatim}
\src{code/haskell/snippet01.hs}
The \code{forall a} is optional in Haskell (and in fact requires
turning on the language extension \code{ExplicitForAll}). Normally,
you would write it like this:
\begin{Verbatim}
alpha :: F a -> G a
\end{Verbatim}
\src{code/haskell/snippet02.hs}
Keep in mind that it's really a family of functions parameterized by
\code{a}. This is another example of the terseness of the Haskell
syntax. A similar construct in C++ would be slightly more verbose:
@ -188,9 +186,7 @@ classes and type families.
Haskell's parametric polymorphism has an unexpected consequence: any
polymorphic function of the type:
\begin{Verbatim}
alpha :: F a -> G a
\end{Verbatim}
\src{code/haskell/snippet03.hs}
where \code{F} and \code{G} are functors, automatically satisfies
the naturality condition. Here it is in categorical notation ($f$
is a function $f \Colon a \to b$):
@ -243,49 +239,30 @@ Let's see a few examples of natural transformations in Haskell. The
first is between the list functor, and the \code{Maybe} functor. It
returns the head of the list, but only if the list is non-empty:
\begin{Verbatim}
safeHead :: [a] -> Maybe a
safeHead [] = Nothing
safeHead (x:xs) = Just x
\end{Verbatim}
\src{code/haskell/snippet04.hs}
It's a function polymorphic in \code{a}. It works for any type
\code{a}, with no limitations, so it is an example of parametric
polymorphism. Therefore it is a natural transformation between the two
functors. But just to convince ourselves, let's verify the naturality
condition.
\begin{Verbatim}
fmap f . safeHead = safeHead . fmap f
\end{Verbatim}
\src{code/haskell/snippet05.hs}
We have two cases to consider; an empty list:
\begin{Verbatim}
fmap f (safeHead []) = fmap f Nothing = Nothing
\end{Verbatim}
\src{code/haskell/snippet06.hs}
\begin{Verbatim}
safeHead (fmap f []) = safeHead [] = Nothing
\end{Verbatim}
\src{code/haskell/snippet07.hs}
and a non-empty list:
\begin{Verbatim}
fmap f (safeHead (x:xs)) = fmap f (Just x) = Just (f x)
\end{Verbatim}
\begin{Verbatim}
safeHead (fmap f (x:xs)) = safeHead (f x : fmap f xs) = Just (f x)
\end{Verbatim}
\src{code/haskell/snippet08.hs}
\src{code/haskell/snippet09.hs}
I used the implementation of \code{fmap} for lists:
\begin{Verbatim}
fmap f [] = []
fmap f (x:xs) = f x : fmap f xs
\end{Verbatim}
\src{code/haskell/snippet10.hs}
and for \code{Maybe}:
\begin{Verbatim}
fmap f Nothing = Nothing
fmap f (Just x) = Just (f x)
\end{Verbatim}
\src{code/haskell/snippet11.hs}
An interesting case is when one of the functors is the trivial
\code{Const} functor. A natural transformation from or to a
\code{Const} functor looks just like a function that's either
@ -294,47 +271,30 @@ polymorphic in its return type or in its argument type.
For instance, \code{length} can be thought of as a natural
transformation from the list functor to the \code{Const Int} functor:
\begin{Verbatim}
length :: [a] -> Const Int a
length [] = Const 0
length (x:xs) = Const (1 + unConst (length xs))
\end{Verbatim}
\src{code/haskell/snippet12.hs}
Here, \code{unConst} is used to peel off the \code{Const}
constructor:
\begin{Verbatim}
unConst :: Const c a -> c
unConst (Const x) = x
\end{Verbatim}
\src{code/haskell/snippet13.hs}
Of course, in practice \code{length} is defined as:
\begin{Verbatim}
length :: [a] -> Int
\end{Verbatim}
\src{code/haskell/snippet14.hs}
which effectively hides the fact that it's a natural transformation.
Finding a parametrically polymorphic function \emph{from} a
\code{Const} functor is a little harder, since it would require the
creation of a value from nothing. The best we can do is:
\begin{Verbatim}
scam :: Const Int a -> Maybe a
scam (Const x) = Nothing
\end{Verbatim}
\src{code/haskell/snippet15.hs}
Another common functor that we've seen already, and which will play an
important role in the Yoneda lemma, is the \code{Reader} functor. I
will rewrite its definition as a \code{newtype}:
\begin{Verbatim}
newtype Reader e a = Reader (e -> a)
\end{Verbatim}
\src{code/haskell/snippet16.hs}
It is parameterized by two types, but is (covariantly) functorial only
in the second one:
\begin{Verbatim}
instance Functor (Reader e) where
fmap f (Reader g) = Reader (\x -> f (g x))
\end{Verbatim}
\src{code/haskell/snippet17.hs}
For every type \code{e}, you can define a family of natural
transformations from \code{Reader e} to any other functor \code{f}.
We'll see later that the members of this family are always in one to one
@ -349,19 +309,13 @@ These are just all the functions that pick a single element from the set
\code{a}. Now let's consider natural transformations from this functor
to the \code{Maybe} functor:
\begin{Verbatim}
alpha :: Reader () a -> Maybe a
\end{Verbatim}
\src{code/haskell/snippet18.hs}
There are only two of these, \code{dumb} and \code{obvious}:
\begin{Verbatim}
dumb (Reader _) = Nothing
\end{Verbatim}
\src{code/haskell/snippet19.hs}
and
\begin{Verbatim}
obvious (Reader g) = Just (g ())
\end{Verbatim}
\src{code/haskell/snippet20.hs}
(The only thing you can do with \code{g} is to apply it to the unit
value \code{()}.)
@ -392,49 +346,34 @@ opposite category to Haskell types.
You might remember the example of a contravariant functor we've looked
at before:
\begin{Verbatim}
newtype Op r a = Op (a -> r)
\end{Verbatim}
\src{code/haskell/snippet21.hs}
This functor is contravariant in \code{a}:
\begin{Verbatim}
instance Contravariant (Op r) where
contramap f (Op g) = Op (g . f)
\end{Verbatim}
\src{code/haskell/snippet22.hs}
We can write a polymorphic function from, say, \code{Op Bool} to
\code{Op String}:
\begin{Verbatim}
predToStr (Op f) = Op (\x -> if f x then "T" else "F")
\end{Verbatim}
\src{code/haskell/snippet23.hs}
But since the two functors are not covariant, this is not a natural
transformation in $\Hask$. However, because they are both
contravariant, they satisfy the ``opposite'' naturality condition:
\begin{Verbatim}
contramap f . predToStr = predToStr . contramap f
\end{Verbatim}
\src{code/haskell/snippet24.hs}
Notice that the function \code{f} must go in the opposite direction
than what you'd use with \code{fmap}, because of the signature of
\code{contramap}:
\begin{Verbatim}
contramap :: (b -> a) -> (Op Bool a -> Op Bool b)
\end{Verbatim}
\src{code/haskell/snippet25.hs}
Are there any type constructors that are not functors, whether covariant
or contravariant? Here's one example:
\begin{Verbatim}
a -> a
\end{Verbatim}
\src{code/haskell/snippet26.hs}
This is not a functor because the same type \code{a} is used both in
the negative (contravariant) and positive (covariant) position. You
can't implement \code{fmap} or \code{contramap} for this type.
Therefore a function of the signature:
\begin{Verbatim}
(a -> a) -> f a
\end{Verbatim}
\src{code/haskell/snippet27.hs}
where \code{f} is an arbitrary functor, cannot be a natural
transformation. Interestingly, there is a generalization of natural
transformations, called dinatural transformations, that deals with such

View File

@ -0,0 +1 @@
alpha :: forall a . F a -> G a

View File

@ -0,0 +1 @@
alpha :: F a -> G a

View File

@ -0,0 +1 @@
alpha :: F a -> G a

View File

@ -0,0 +1,3 @@
safeHead :: [a] -> Maybe a
safeHead [] = Nothing
safeHead (x:xs) = Just x

View File

@ -0,0 +1 @@
fmap f . safeHead = safeHead . fmap f

View File

@ -0,0 +1 @@
fmap f (safeHead []) = fmap f Nothing = Nothing

View File

@ -0,0 +1 @@
safeHead (fmap f []) = safeHead [] = Nothing

View File

@ -0,0 +1 @@
fmap f (safeHead (x:xs)) = fmap f (Just x) = Just (f x)

View File

@ -0,0 +1 @@
safeHead (fmap f (x:xs)) = safeHead (f x : fmap f xs) = Just (f x)

View File

@ -0,0 +1,2 @@
fmap f [] = []
fmap f (x:xs) = f x : fmap f xs

View File

@ -0,0 +1,2 @@
fmap f Nothing = Nothing
fmap f (Just x) = Just (f x)

View File

@ -0,0 +1,3 @@
length :: [a] -> Const Int a
length [] = Const 0
length (x:xs) = Const (1 + unConst (length xs))

View File

@ -0,0 +1,2 @@
unConst :: Const c a -> c
unConst (Const x) = x

View File

@ -0,0 +1 @@
length :: [a] -> Int

View File

@ -0,0 +1,2 @@
scam :: Const Int a -> Maybe a
scam (Const x) = Nothing

View File

@ -0,0 +1 @@
newtype Reader e a = Reader (e -> a)

View File

@ -0,0 +1,2 @@
instance Functor (Reader e) where
fmap f (Reader g) = Reader (\x -> f (g x))

View File

@ -0,0 +1 @@
alpha :: Reader () a -> Maybe a

View File

@ -0,0 +1 @@
dumb (Reader _) = Nothing

View File

@ -0,0 +1 @@
obvious (Reader g) = Just (g ())

View File

@ -0,0 +1 @@
newtype Op r a = Op (a -> r)

View File

@ -0,0 +1,2 @@
instance Contravariant (Op r) where
contramap f (Op g) = Op (g . f)

View File

@ -0,0 +1 @@
predToStr (Op f) = Op (\x -> if f x then "T" else "F")

View File

@ -0,0 +1 @@
contramap f . predToStr = predToStr . contramap f

View File

@ -0,0 +1 @@
contramap :: (b -> a) -> (Op Bool a -> Op Bool b)

View File

@ -0,0 +1 @@
a -> a

View File

@ -0,0 +1 @@
(a -> a) -> f a

View File

@ -1,3 +1,5 @@
% !TEX root = ../../ctfp-reader.tex
\lettrine[lhang=0.17]{T}{he category of types and functions} plays an important role in
programming, so let's talk about what types are and why we need them.
@ -107,9 +109,7 @@ synonym for a list of \code{Char}, is an example of an infinite set.
When we declare \code{x} to be an \code{Integer}:
\begin{Verbatim}
x :: Integer
\end{Verbatim}
\src{code/haskell/snippet01.hs}
we are saying that it's an element of the set of integers.
\code{Integer} in Haskell is an infinite set, and it can be used to do
arbitrary precision arithmetic. There is also a finite-set \code{Int}
@ -149,9 +149,7 @@ called the \newterm{bottom} and denoted by \code{\_|\_}, or
Unicode $\bot$. This ``value'' corresponds to a non-terminating computation.
So a function declared as:
\begin{Verbatim}
f :: Bool -> Bool
\end{Verbatim}
\src{code/haskell/snippet02.hs}
may return \code{True}, \code{False}, or \code{\_|\_};
the latter meaning that it would never terminate.
@ -160,18 +158,12 @@ is convenient to treat every runtime error as a bottom, and even allow
functions to return the bottom explicitly. The latter is usually done
using the expression \code{undefined}, as in:
\begin{Verbatim}
f :: Bool -> Bool
f x = undefined
\end{Verbatim}
\src{code/haskell/snippet03.hs}
This definition type checks because \code{undefined} evaluates to
bottom, which is a member of any type, including \code{Bool}. You can
even write:
\begin{Verbatim}
f :: Bool -> Bool
f = undefined
\end{Verbatim}
\src{code/haskell/snippet04.hs}
(without the \code{x}) because the bottom is also a member of the type\\
\code{Bool -> Bool}.
@ -179,7 +171,7 @@ Functions that may return bottom are called partial, as opposed to total
functions, which return valid results for every possible argument.
Because of the bottom, you'll see the category of Haskell types and
functions referred to as $\cat{Hask}$ rather than $\Set$. From
functions referred to as $\Hask$ rather than $\Set$. From
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
@ -237,9 +229,7 @@ usually quite simple, if not trivial.
Consider the definition of a factorial function in Haskell, which is a
language quite amenable to denotational semantics:
\begin{Verbatim}
fact n = product [1..n]
\end{Verbatim}
\src{code/haskell/snippet05.hs}
The expression \code{{[}1..n{]}} is a list of integers from \code{1} to \code{n}.
The function \code{product} multiplies all elements of a list. That's
just like a definition of factorial taken from a math text. Compare this
@ -323,9 +313,7 @@ return, there are no restrictions whatsoever. It can return any type
it's a function that's polymorphic in the return type. Haskellers have a
name for it:
\begin{Verbatim}
absurd :: Void -> a
\end{Verbatim}
\src{code/haskell/snippet06.hs}
(Remember, \code{a} is a type variable that can stand for any type.)
The name is not coincidental. There is deeper interpretation of types
and functions in terms of logic called the Curry-Howard isomorphism. The
@ -355,10 +343,7 @@ because of the Haskell's love of terseness, the same symbol \code{()}
is used for the type, the constructor, and the only value corresponding
to a singleton set. So here's this function in Haskell:
\begin{Verbatim}
f44 :: () -> Integer
f44 () = 44
\end{Verbatim}
\src{code/haskell/snippet07.hs}
The first line declares that \code{f44} takes the type \code{()},
pronounced ``unit,'' into the type \code{Integer}. The second line
defines \code{f44} by pattern matching the only constructor for unit,
@ -387,19 +372,13 @@ element of $A$ to the single element of that singleton set. For every $A$
there is exactly one such function. Here's this function for
\code{Integer}:
\begin{Verbatim}
fInt :: Integer -> ()
fInt x = ()
\end{Verbatim}
\src{code/haskell/snippet08.hs}
You give it any integer, and it gives you back a unit. In the spirit of
terseness, Haskell lets you use the wildcard pattern, the underscore,
for an argument that is discarded. This way you don't have to invent a
name for it. So the above can be rewritten as:
\begin{Verbatim}
fInt :: Integer -> ()
fInt _ = ()
\end{Verbatim}
\src{code/haskell/snippet09.hs}
Notice that the implementation of this function not only doesn't depend
on the value passed to it, but it doesn't even depend on the type of the
argument.
@ -410,10 +389,7 @@ such functions with one equation using a type parameter instead of a
concrete type. What should we call a polymorphic function from any type
to unit type? Of course we'll call it \code{unit}:
\begin{Verbatim}
unit :: a -> ()
unit _ = ()
\end{Verbatim}
\src{code/haskell/snippet10.hs}
In C++ you would write this function as:
\begin{Verbatim}
@ -425,9 +401,7 @@ Next in the typology of types is a two-element set. In C++ it's called
is that in C++ \code{bool} is a built-in type, whereas in Haskell it
can be defined as follows:
\begin{Verbatim}
data Bool = True | False
\end{Verbatim}
\src{code/haskell/snippet11.hs}
(The way to read this definition is that \code{Bool} is either
\code{True} or \code{False}.) In principle, one should also be able
to define a Boolean type in C++ as an enumeration:

View File

@ -0,0 +1 @@
x :: Integer

View File

@ -0,0 +1 @@
f :: Bool -> Bool

View File

@ -0,0 +1,2 @@
f :: Bool -> Bool
f x = undefined

View File

@ -0,0 +1,2 @@
f :: Bool -> Bool
f = undefined

View File

@ -0,0 +1 @@
fact n = product [1..n]

View File

@ -0,0 +1 @@
absurd :: Void -> a

View File

@ -0,0 +1,2 @@
f44 :: () -> Integer
f44 () = 44

View File

@ -0,0 +1,2 @@
fInt :: Integer -> ()
fInt x = ()

View File

@ -0,0 +1,2 @@
fInt :: Integer -> ()
fInt _ = ()

View File

@ -0,0 +1,2 @@
unit :: a -> ()
unit _ = ()

View File

@ -0,0 +1 @@
data Bool = True | False

View File

@ -1,3 +1,5 @@
% !TEX root = ../../ctfp-reader.tex
\lettrine[lhang=0.17]{Y}{ou can get} real appreciation for categories by studying a variety of
examples. Categories come in all shapes and sizes and often pop up in
unexpected places. We'll start with something really simple.
@ -103,11 +105,7 @@ In Haskell we can define a type class for monoids --- a type for which
there is a neutral element called \code{mempty} and a binary operation
called \code{mappend}:
\begin{Verbatim}
class Monoid m where
mempty :: m
mappend :: m -> m -> m
\end{Verbatim}
\src{code/haskell/snippet01.hs}
The type signature for a two-argument function,
\code{m -> m -> m}, might look strange at first,
but it will make perfect sense after we talk about currying. You may
@ -133,11 +131,7 @@ be a monoid by providing the implementation of \code{mempty} and
\code{mappend} (this is, in fact, done for you in the standard
Prelude):
\begin{Verbatim}
instance Monoid String where
mempty = ""
mappend = (++)
\end{Verbatim}
\src{code/haskell/snippet02.hs}
Here, we have reused the list concatenation operator \code{(++)},
because a \code{String} is just a list of characters.

View File

@ -0,0 +1,3 @@
class Monoid m where
mempty :: m
mappend :: m -> m -> m

View File

@ -0,0 +1,3 @@
instance Monoid String where
mempty = ""
mappend = (++)

View File

@ -1,3 +1,5 @@
% !TEX root = ../../ctfp-reader.tex
\lettrine[lhang=0.17]{Y}{ou've seen how to model} types and pure functions as a category. I also
mentioned that there is a way to model side effects, or non-pure
functions, in category theory. Let's have a look at one such example:
@ -307,9 +309,7 @@ The same thing in Haskell is a little more terse, and we also get a lot
more help from the compiler. Let's start by defining the \code{Writer}
type:
\begin{Verbatim}
type Writer a = (a, String)
\end{Verbatim}
\src{code/haskell/snippet01.hs}
Here I'm just defining a type alias, an equivalent of a \code{typedef}
(or \code{using}) in C++. The type \code{Writer} is parameterized by
a type variable \code{a} and is equivalent to a pair of \code{a} and
@ -319,15 +319,11 @@ parentheses, separated by a comma.
Our morphisms are functions from an arbitrary type to some
\code{Writer} type:
\begin{Verbatim}
a -> Writer b
\end{Verbatim}
\src{code/haskell/snippet02.hs}
We'll declare the composition as a funny infix operator, sometimes
called the ``fish'':
\begin{Verbatim}
(>=>) :: (a -> Writer b) -> (b -> Writer c) -> (a -> Writer c)
\end{Verbatim}
\src{code/haskell/snippet03.hs}
It's a function of two arguments, each being a function on its own, and
returning a function. The first argument is of the type
\code{(a -> Writer b)}, the second is
@ -338,12 +334,7 @@ Here's the definition of this infix operator --- the two arguments
\code{m1} and \code{m2} appearing on either side of the fishy
symbol:
\begin{Verbatim}
m1 >=> m2 = \x ->
let (y, s1) = m1 x
(z, s2) = m2 y
in (z, s1 ++ s2)
\end{Verbatim}
\src{code/haskell/snippet04.hs}
The result is a lambda function of one argument \code{x}. The lambda
is written as a backslash --- think of it as the Greek letter λ with an
amputated leg.
@ -367,22 +358,13 @@ I will also define the identity morphism for our category, but for
reasons that will become clear much later, I will call it
\code{return}.
\begin{Verbatim}
return :: a -> Writer a
return x = (x, "")
\end{Verbatim}
\src{code/haskell/snippet05.hs}
For completeness, let's have the Haskell versions of the embellished
functions \code{upCase} and \code{toWords}:
\begin{Verbatim}
upCase :: String -> Writer String
upCase s = (map toUpper s, "upCase ")
\end{Verbatim}
\src{code/haskell/snippet06.hs}
\begin{Verbatim}
toWords :: String -> Writer [String]
toWords s = (words s, "toWords ")
\end{Verbatim}
\src{code/haskell/snippet07.hs}
The function \code{map} corresponds to the C++ \code{transform}. It
applies the character function \code{toUpper} to the string
\code{s}. The auxiliary function \code{words} is defined in the
@ -391,10 +373,7 @@ standard Prelude library.
Finally, the composition of the two functions is accomplished with the
help of the fish operator:
\begin{Verbatim}
process :: String -> Writer [String]
process = upCase >=> toWords
\end{Verbatim}
\src{code/haskell/snippet08.hs}
\section{Kleisli Categories}

View File

@ -0,0 +1 @@
type Writer a = (a, String)

View File

@ -0,0 +1 @@
a -> Writer b

View File

@ -0,0 +1 @@
(>=>) :: (a -> Writer b) -> (b -> Writer c) -> (a -> Writer c)

View File

@ -0,0 +1,4 @@
m1 >=> m2 = \x ->
let (y, s1) = m1 x
(z, s2) = m2 y
in (z, s1 ++ s2)

View File

@ -0,0 +1,2 @@
return :: a -> Writer a
return x = (x, "")

View File

@ -0,0 +1,2 @@
upCase :: String -> Writer String
upCase s = (map toUpper s, "upCase ")

View File

@ -0,0 +1,2 @@
toWords :: String -> Writer [String]
toWords s = (words s, "toWords ")

View File

@ -0,0 +1,2 @@
process :: String -> Writer [String]
process = upCase >=> toWords

View File

@ -1,3 +1,5 @@
% !TEX root = ../../ctfp-reader.tex
\lettrine[lhang=0.17]{T}{he Ancient Greek} playwright Euripides once said: ``Every man is like
the company he is wont to keep.'' We are defined by our relationships.
Nowhere is this more true than in category theory. If we want to single
@ -71,9 +73,7 @@ set. Remember, an empty set corresponds to the Haskell type
polymorphic function from \code{Void} to any other type is called
\code{absurd}:
\begin{Verbatim}
absurd :: Void -> a
\end{Verbatim}
\src{code/haskell/snippet01.hs}
It's this family of morphisms that makes \code{Void} the initial
object in the category of types.
@ -107,10 +107,7 @@ one value --- implicit in C++ and explicit in Haskell, denoted by
\code{()}. We've also established that there is one and only one pure
function from any type to the unit type:
\begin{Verbatim}
unit :: a -> ()
unit _ = ()
\end{Verbatim}
\src{code/haskell/snippet02.hs}
so all the conditions for the terminal object are satisfied.
Notice that in this example the uniqueness condition is crucial, because
@ -118,17 +115,11 @@ there are other sets (actually, all of them, except for the empty set)
that have incoming morphisms from every set. For instance, there is a
Boolean-valued function (a predicate) defined for every type:
\begin{Verbatim}
yes :: a -> Bool
yes _ = True
\end{Verbatim}
\src{code/haskell/snippet03.hs}
But \code{Bool} is not a terminal object. There is at least one more
\code{Bool}-valued function from every type:
\begin{Verbatim}
no :: a -> Bool
no _ = False
\end{Verbatim}
\src{code/haskell/snippet04.hs}
Insisting on uniqueness gives us just the right precision to narrow down
the definition of the terminal object to just one type.
@ -189,10 +180,7 @@ $g$ is the inverse of morphism $f$ if their composition is the
identity morphism. These are actually two equations because there are
two ways of composing two morphisms:
\begin{Verbatim}
f . g = id
g . f = id
\end{Verbatim}
\src{code/haskell/snippet05.hs}
When I said that the initial (terminal) object was unique up to
isomorphism, I meant that any two initial (terminal) objects are
isomorphic. That's actually easy to see. Let's suppose that we have two
@ -242,15 +230,9 @@ the product to each of the constituents. In Haskell, these two functions
are called \code{fst} and \code{snd} and they pick, respectively,
the first and the second component of a pair:
\begin{Verbatim}
fst :: (a, b) -> a
fst (x, y) = x
\end{Verbatim}
\src{code/haskell/snippet06.hs}
\begin{Verbatim}
snd :: (a, b) -> b
snd (x, y) = y
\end{Verbatim}
\src{code/haskell/snippet07.hs}
Here, the functions are defined by pattern matching their arguments: the
pattern that matches any pair is \code{(x, y)}, and it extracts its
components into variables \code{x} and \code{y}.
@ -258,10 +240,7 @@ components into variables \code{x} and \code{y}.
These definitions can be simplified even further with the use of
wildcards:
\begin{Verbatim}
fst (x, _) = x
snd (_, y) = y
\end{Verbatim}
\src{code/haskell/snippet08.hs}
In C++, we would use template functions, for instance:
\begin{Verbatim}
@ -277,10 +256,7 @@ $b$. This pattern consists of an object $c$ and two morphisms
$p$ and $q$ connecting it to $a$ and $b$,
respectively:
\begin{Verbatim}
p :: c -> a
q :: c -> b
\end{Verbatim}
\src{code/haskell/snippet09.hs}
\begin{figure}[H]
\centering
@ -305,26 +281,14 @@ Here's one: \code{Int}. Can \code{Int} be considered a candidate for
the product of \code{Int} and \code{Bool}? Yes, it can --- and here
are its projections:
\begin{Verbatim}
p :: Int -> Int
p x = x
q :: Int -> Bool
q _ = True
\end{Verbatim}
\src{code/haskell/snippet10.hs}
That's pretty lame, but it matches the criteria.
Here's another one: \code{(Int, Int, Bool)}. It's a tuple of three
elements, or a triple. Here are two morphisms that make it a legitimate
candidate (we are using pattern matching on triples):
\begin{Verbatim}
p :: (Int, Int, Bool) -> Int
p (x, _, _) = x
q :: (Int, Int, Bool) -> Bool
q (_, _, b) = b
\end{Verbatim}
\src{code/haskell/snippet11.hs}
You may have noticed that while our first candidate was too small --- it
only covered the \code{Int} dimension of the product; the second was
too big --- it spuriously duplicated the \code{Int} dimension.
@ -341,10 +305,7 @@ projections of $c'$. What it means is that the projections
\emph{p'} and \emph{q'} can be reconstructed from \emph{p} and \emph{q}
using $m$:
\begin{Verbatim}
p' = p . m
q' = q . m
\end{Verbatim}
\src{code/haskell/snippet12.hs}
\begin{figure}[H]
\centering
@ -370,31 +331,20 @@ presented before.
\noindent
The mapping \code{m} for the first candidate is:
\begin{Verbatim}
m :: Int -> (Int, Bool)
m x = (x, True)
\end{Verbatim}
\src{code/haskell/snippet13.hs}
Indeed, the two projections, \code{p} and \code{q} can be
reconstructed as:
\begin{Verbatim}
p x = fst (m x) = x
q x = snd (m x) = True
\end{Verbatim}
\src{code/haskell/snippet14.hs}
The \code{m} for the second example is similarly uniquely determined:
\begin{Verbatim}
m (x, _, b) = (x, b)
\end{Verbatim}
\src{code/haskell/snippet15.hs}
We were able to show that \code{(Int, Bool)} is better than either of
the two candidates. Let's see why the opposite is not true. Could we
find some \code{m'} that would help us reconstruct \code{fst}
and \code{snd} from \code{p} and \code{q}?
\begin{Verbatim}
fst = p . m'
snd = q . m'
\end{Verbatim}
\src{code/haskell/snippet16.hs}
In our first example, \code{q} always returned \code{True} and we
know that there are pairs whose second component is \code{False}. We
can't reconstruct \code{snd} from \code{q}.
@ -405,14 +355,10 @@ to factorize \code{fst} and \code{snd}. Because both \code{p} and
\code{q} ignore the second component of the triple, our \code{m'}
can put anything in it. We can have:
\begin{Verbatim}
m' (x, b) = (x, x, b)
\end{Verbatim}
or
\src{code/haskell/snippet17.hs}
\begin{Verbatim}
m' (x, b) = (x, 42, b)
\end{Verbatim}
or
\src{code/haskell/snippet18.hs}
and so on.
Putting it all together, given any type \code{c} with two projections
@ -420,10 +366,7 @@ Putting it all together, given any type \code{c} with two projections
to the Cartesian product \code{(a, b)} that factorizes them. In fact,
it just combines \code{p} and \code{q} into a pair.
\begin{Verbatim}
m :: c -> (a, b)
m x = (p x, q x)
\end{Verbatim}
\src{code/haskell/snippet19.hs}
That makes the Cartesian product \code{(a, b)} our best match, which
means that this universal construction works in the category of sets. It
picks the product of any two sets.
@ -444,10 +387,7 @@ A (higher order) function that produces the factorizing function
\code{m} from two candidates is sometimes called the
\newterm{factorizer}. In our case, it would be the function:
\begin{Verbatim}
factorizer :: (c -> a) -> (c -> b) -> (c -> (a, b))
factorizer p q = \x -> (p x, q x)
\end{Verbatim}
\src{code/haskell/snippet20.hs}
\section{Coproduct}
@ -457,10 +397,7 @@ pattern, we end up with an object $c$ equipped with two
\emph{injections}, \code{i} and \code{j}: morphisms from $a$
and $b$ to $c$.
\begin{Verbatim}
i :: a -> c
j :: b -> c
\end{Verbatim}
\src{code/haskell/snippet21.hs}
\begin{figure}[H]
\centering
@ -473,10 +410,7 @@ $c'$ that is equipped with the injections $i'$ and $j'$
if there is a morphism $m$ from $c$ to $c'$ that
factorizes the injections:
\begin{Verbatim}
i' = m . i
j' = m . j
\end{Verbatim}
\src{code/haskell/snippet22.hs}
\begin{figure}[H]
\centering
@ -539,26 +473,19 @@ In Haskell, you can combine any data types into a tagged union by
separating data constructors with a vertical bar. The \code{Contact}
example translates into the declaration:
\begin{Verbatim}
data Contact = PhoneNum Int | EmailAddr String
\end{Verbatim}
\src{code/haskell/snippet23.hs}
Here, \code{PhoneNum} and \code{EmailAddr} serve both as
constructors (injections), and as tags for pattern matching (more about
this later). For instance, this is how you would construct a contact
using a phone number:
\begin{Verbatim}
helpdesk :: Contact
helpdesk = PhoneNum 2222222
\end{Verbatim}
\src{code/haskell/snippet24.hs}
Unlike the canonical implementation of the product that is built into
Haskell as the primitive pair, the canonical implementation of the
coproduct is a data type called \code{Either}, which is defined in the
standard Prelude as:
\begin{Verbatim}
data Either a b = Left a | Right b
\end{Verbatim}
\src{code/haskell/snippet25.hs}
It is parameterized by two types, \code{a} and \code{b} and has two
constructors: \code{Left} that takes a value of type \code{a}, and
\code{Right} that takes a value of type \code{b}.
@ -568,11 +495,7 @@ for the coproduct. Given a candidate type \code{c} and two candidate
injections \code{i} and \code{j}, the factorizer for \code{Either}
produces the factoring function:
\begin{Verbatim}
factorizer :: (a -> c) -> (b -> c) -> Either a b -> c
factorizer i j (Left a) = i a
factorizer i j (Right b) = j b
\end{Verbatim}
\src{code/haskell/snippet26.hs}
\section{Asymmetry}
@ -610,17 +533,11 @@ Because the product is universal, there is also a (unique) morphism
morphism selects an element from the product set --- it selects a
concrete pair. It also factorizes the two projections:
\begin{Verbatim}
p = fst . m
q = snd . m
\end{Verbatim}
\src{code/haskell/snippet27.hs}
When acting on the singleton value \code{()}, the only element of the
singleton set, these two equations become:
\begin{Verbatim}
p () = fst (m ())
q () = snd (m ())
\end{Verbatim}
\src{code/haskell/snippet28.hs}
Since \code{m ()} is the element of the product picked by \code{m},
these equations tell us that the element picked by \code{p} from the
first set, \code{p ()}, is the first component of the pair picked by

View File

@ -0,0 +1 @@
absurd :: Void -> a

View File

@ -0,0 +1,2 @@
unit :: a -> ()
unit _ = ()

View File

@ -0,0 +1,2 @@
yes :: a -> Bool
yes _ = True

View File

@ -0,0 +1,2 @@
no :: a -> Bool
no _ = False

View File

@ -0,0 +1,2 @@
f . g = id
g . f = id

View File

@ -0,0 +1,2 @@
fst :: (a, b) -> a
fst (x, y) = x

View File

@ -0,0 +1,2 @@
snd :: (a, b) -> b
snd (x, y) = y

View File

@ -0,0 +1,2 @@
fst (x, _) = x
snd (_, y) = y

View File

@ -0,0 +1,2 @@
p :: c -> a
q :: c -> b

View File

@ -0,0 +1,5 @@
p :: Int -> Int
p x = x
q :: Int -> Bool
q _ = True

View File

@ -0,0 +1,5 @@
p :: (Int, Int, Bool) -> Int
p (x, _, _) = x
q :: (Int, Int, Bool) -> Bool
q (_, _, b) = b

View File

@ -0,0 +1,2 @@
p' = p . m
q' = q . m

View File

@ -0,0 +1,2 @@
m :: Int -> (Int, Bool)
m x = (x, True)

View File

@ -0,0 +1,2 @@
p x = fst (m x) = x
q x = snd (m x) = True

View File

@ -0,0 +1 @@
m (x, _, b) = (x, b)

View File

@ -0,0 +1,2 @@
fst = p . m'
snd = q . m'

View File

@ -0,0 +1 @@
m' (x, b) = (x, x, b)

View File

@ -0,0 +1 @@
m' (x, b) = (x, 42, b)

View File

@ -0,0 +1,2 @@
m :: c -> (a, b)
m x = (p x, q x)

View File

@ -0,0 +1,2 @@
factorizer :: (c -> a) -> (c -> b) -> (c -> (a, b))
factorizer p q = \x -> (p x, q x)

View File

@ -0,0 +1,2 @@
i :: a -> c
j :: b -> c

View File

@ -0,0 +1,2 @@
i' = m . i
j' = m . j

View File

@ -0,0 +1 @@
data Contact = PhoneNum Int | EmailAddr String

View File

@ -0,0 +1,2 @@
helpdesk :: Contact
helpdesk = PhoneNum 2222222

View File

@ -0,0 +1 @@
data Either a b = Left a | Right b

View File

@ -0,0 +1,3 @@
factorizer :: (a -> c) -> (b -> c) -> Either a b -> c
factorizer i j (Left a) = i a
factorizer i j (Right b) = j b

View File

@ -0,0 +1,2 @@
p = fst . m
q = snd . m

View File

@ -0,0 +1,2 @@
p () = fst (m ())
q () = snd (m ())

View File

@ -1,3 +1,5 @@
% !TEX root = ../../ctfp-reader.tex
\lettrine[lhang=0.17]{W}{e've seen two basic} ways of combining types: using a product and a
coproduct. It turns out that a lot of data structures in everyday
programming can be built using just these two mechanisms. This fact has
@ -31,10 +33,7 @@ the same information. They are, however, commutative up to isomorphism
--- the isomorphism being given by the \code{swap} function (which is
its own inverse):
\begin{Verbatim}
swap :: (a, b) -> (b, a)
swap (x, y) = (y, x)
\end{Verbatim}
\src{code/haskell/snippet01.hs}
You can think of the two pairs as simply using a different format for
storing the same data. It's just like big endian vs. little endian.
@ -45,28 +44,18 @@ ways of nesting pairs are isomorphic. If you want to combine three types
in a product, \code{a}, \code{b}, and \code{c}, in this order, you
can do it in two ways:
\begin{Verbatim}
((a, b), c)
\end{Verbatim}
or
\src{code/haskell/snippet02.hs}
\begin{Verbatim}
(a, (b, c))
\end{Verbatim}
or
\src{code/haskell/snippet03.hs}
These types are different --- you can't pass one to a function that
expects the other --- but their elements are in one-to-one
correspondence. There is a function that maps one to another:
\begin{Verbatim}
alpha :: ((a, b), c) -> (a, (b, c))
alpha ((x, y), z) = (x, (y, z))
\end{Verbatim}
\src{code/haskell/snippet04.hs}
and this function is invertible:
\begin{Verbatim}
alpha_inv :: (a, (b, c)) -> ((a, b), c)
alpha_inv (x, (y, z)) = ((x, y), z)
\end{Verbatim}
\src{code/haskell/snippet05.hs}
so it's an isomorphism. These are just different ways of repackaging the
same data.
@ -83,20 +72,12 @@ unit of the product the same way 1 is the unit of multiplication.
Indeed, the pairing of a value of some type \code{a} with a unit
doesn't add any information. The type:
\begin{Verbatim}
(a, ())
\end{Verbatim}
\src{code/haskell/snippet06.hs}
is isomorphic to \code{a}. Here's the isomorphism:
\begin{Verbatim}
rho :: (a, ()) -> a
rho (x, ()) = x
\end{Verbatim}
\src{code/haskell/snippet07.hs}
\begin{Verbatim}
rho_inv :: a -> (a, ())
rho_inv x = (x, ())
\end{Verbatim}
\src{code/haskell/snippet08.hs}
These observations can be formalized by saying that $\Set$ (the
category of sets) is a \newterm{monoidal category}. It's a category that's
also a monoid, in the sense that you can multiply objects (here, take
@ -108,9 +89,7 @@ especially, as we'll see soon, when they are combined with sum types. It
uses named constructors with multiple arguments. A pair, for instance,
can be defined alternatively as:
\begin{Verbatim}
data Pair a b = P a b
\end{Verbatim}
\src{code/haskell/snippet09.hs}
Here, \code{Pair a b} is the name of the type parameterized by two
other types, \code{a} and \code{b}; and \code{P} is the name of
the data constructor. You define a pair type by passing two types to the
@ -119,10 +98,7 @@ two values of appropriate types to the constructor \code{P}. For
instance, let's define a value \code{stmt} as a pair of
\code{String} and \code{Bool}:
\begin{Verbatim}
stmt :: Pair String Bool
stmt = P "This statements is" False
\end{Verbatim}
\src{code/haskell/snippet10.hs}
The first line is the type declaration. It uses the type constructor
\code{Pair}, with \code{String} and \code{Bool} replacing
\code{a} and the \code{b} in the generic definition of
@ -134,26 +110,20 @@ constructors, to construct values.
Since the name spaces for type and data constructors are separate in
Haskell, you will often see the same name used for both, as in:
\begin{Verbatim}
data Pair a b = Pair a b
\end{Verbatim}
\src{code/haskell/snippet11.hs}
And if you squint hard enough, you may even view the built-in pair type
as a variation on this kind of declaration, where the name \code{Pair}
is replaced with the binary operator \code{(,)}. In fact you can use
\code{(,)} just like any other named constructor and create pairs
using prefix notation:
\begin{Verbatim}
stmt = (,) "This statement is" False
\end{Verbatim}
\src{code/haskell/snippet12.hs}
Similarly, you can use \code{(,,)} to create triples, and so on.
Instead of using generic pairs or tuples, you can also define specific
named product types, as in:
\begin{Verbatim}
data Stmt = Stmt String Bool
\end{Verbatim}
\src{code/haskell/snippet13.hs}
which is just a product of \code{String} and \code{Bool}, but it's
given its own name and constructor. The advantage of this style of
declaration is that you may define many types that have the same content
@ -175,54 +145,32 @@ what. We would extract components by pattern matching, as in this
function that checks if the symbol of the element is the prefix of its
name (as in \textbf{He} being the prefix of \textbf{Helium}):
\begin{Verbatim}
startsWithSymbol :: (String, String, Int) -> Bool
startsWithSymbol (name, symbol, _) = isPrefixOf symbol name
\end{Verbatim}
\src{code/haskell/snippet14.hs}
This code is error prone, and is hard to read and maintain. It's much
better to define a record:
\begin{Verbatim}
data Element = Element { name :: String
, symbol :: String
, atomicNumber :: Int }
\end{Verbatim}
\src{code/haskell/snippet15.hs}
The two representations are isomorphic, as witnessed by these two
conversion functions, which are the inverse of each other:
\begin{Verbatim}
tupleToElem :: (String, String, Int) -> Element
tupleToElem (n, s, a) = Element { name = n
, symbol = s
, atomicNumber = a }
\end{Verbatim}
\src{code/haskell/snippet16.hs}
\begin{Verbatim}
elemToTuple :: Element -> (String, String, Int)
elemToTuple e = (name e, symbol e, atomicNumber e)
\end{Verbatim}
\src{code/haskell/snippet17.hs}
Notice that the names of record fields also serve as functions to access
these fields. For instance, \code{atomicNumber e} retrieves the
\code{atomicNumber} field from \code{e}. We use
\code{atomicNumber} as a function of the type:
\begin{Verbatim}
atomicNumber :: Element -> Int
\end{Verbatim}
\src{code/haskell/snippet18.hs}
With the record syntax for \code{Element}, our function
\code{startsWithSymbol} becomes more readable:
\begin{Verbatim}
startsWithSymbol :: Element -> Bool
startsWithSymbol e = isPrefixOf (symbol e) (name e)
\end{Verbatim}
\src{code/haskell/snippet19.hs}
We could even use the Haskell trick of turning the function
\code{isPrefixOf} into an infix operator by surrounding it with
backquotes, and make it read almost like a sentence:
\begin{Verbatim}
startsWithSymbol e = symbol e `isPrefixOf` name e
\end{Verbatim}
\src{code/haskell/snippet20.hs}
The parentheses could be omitted in this case, because an infix operator
has lower precedence than a function call.
@ -232,16 +180,12 @@ Just as the product in the category of sets gives rise to product types,
the coproduct gives rise to sum types. The canonical implementation of a
sum type in Haskell is:
\begin{Verbatim}
data Either a b = Left a | Right b
\end{Verbatim}
\src{code/haskell/snippet21.hs}
And like pairs, \code{Either}s are commutative (up to isomorphism),
can be nested, and the nesting order is irrelevant (up to isomorphism).
So we can, for instance, define a sum equivalent of a triple:
\begin{Verbatim}
data OneOfThree a b c = Sinistral a | Medial b | Dextral c
\end{Verbatim}
\src{code/haskell/snippet22.hs}
and so on.
It turns out that $\Set$ is also a (symmetric) monoidal category
@ -253,9 +197,7 @@ neutral element. You can think of \code{Either} as plus, and
\code{Void} as zero. Indeed, adding \code{Void} to a sum type
doesn't change its content. For instance:
\begin{Verbatim}
Either a Void
\end{Verbatim}
\src{code/haskell/snippet23.hs}
is isomorphic to \code{a}. That's because there is no way to construct
a \code{Right} version of this type --- there isn't a value of type
\code{Void}. The only inhabitants of \code{Either a Void} are
@ -270,9 +212,7 @@ First of all, the simplest sum types are just enumerations and are
implemented using \code{enum} in C++. The equivalent of the Haskell
sum type:
\begin{Verbatim}
data Color = Red | Green | Blue
\end{Verbatim}
\src{code/haskell/snippet24.hs}
is the C++:
\begin{Verbatim}
@ -280,9 +220,7 @@ enum { Red, Green, Blue };
\end{Verbatim}
An even simpler sum type:
\begin{Verbatim}
data Bool = True | False
\end{Verbatim}
\src{code/haskell/snippet25.hs}
is the primitive \code{bool} in C++.
Simple sum types that encode the presence or absence of a value are
@ -291,36 +229,26 @@ values, like empty strings, negative numbers, null pointers, etc. This
kind of optionality, if deliberate, is expressed in Haskell using the
\code{Maybe} type:
\begin{Verbatim}
data Maybe a = Nothing | Just a
\end{Verbatim}
\src{code/haskell/snippet26.hs}
The \code{Maybe} type is a sum of two types. You can see this if you
separate the two constructors into individual types. The first one would
look like this:
\begin{Verbatim}
data NothingType = Nothing
\end{Verbatim}
\src{code/haskell/snippet27.hs}
It's an enumeration with one value called \code{Nothing}. In other
words, it's a singleton, which is equivalent to the unit type
\code{()}. The second part:
\begin{Verbatim}
data JustType a = Just a
\end{Verbatim}
\src{code/haskell/snippet28.hs}
is just an encapsulation of the type \code{a}. We could have encoded
\code{Maybe} as:
\begin{Verbatim}
data Maybe a = Either () a
\end{Verbatim}
\src{code/haskell/snippet29.hs}
More complex sum types are often faked in C++ using pointers. A pointer
can be either null, or point to a value of specific type. For instance,
a Haskell list type, which can be defined as a (recursive) sum type:
\begin{Verbatim}
data List a = Nil | Cons a (List a)
\end{Verbatim}
\src{code/haskell/snippet30.hs}
can be translated to C++ using the null pointer trick to implement the
empty list:
@ -364,11 +292,7 @@ constructors. One matches the empty \code{Nil} list, and the other a
\code{Cons}-constructed list. For instance, here's the definition of a
simple function on \code{List}s:
\begin{Verbatim}
maybeTail :: List a -> Maybe (List a)
maybeTail Nil = Nothing
maybeTail (Cons _ t) = Just t
\end{Verbatim}
\src{code/haskell/snippet31.hs}
The first part of the definition of \code{maybeTail} uses the
\code{Nil} constructor as pattern and returns \code{Nothing}. The
second part uses the \code{Cons} constructor as pattern. It replaces
@ -423,41 +347,22 @@ property:
Does it also hold for product and sum types? Yes, it does --- up to
isomorphisms, as usual. The left hand side corresponds to the type:
\begin{Verbatim}
(a, Either b c)
\end{Verbatim}
\src{code/haskell/snippet32.hs}
and the right hand side corresponds to the type:
\begin{Verbatim}
Either (a, b) (a, c)
\end{Verbatim}
\src{code/haskell/snippet33.hs}
Here's the function that converts them one way:
\begin{Verbatim}
prodToSum :: (a, Either b c) -> Either (a, b) (a, c)
prodToSum (x, e) =
case e of
Left y -> Left (x, y)
Right z -> Right (x, z)
\end{Verbatim}
\src{code/haskell/snippet34.hs}
and here's one that goes the other way:
\begin{Verbatim}
sumToProd :: Either (a, b) (a, c) -> (a, Either b c)
sumToProd e =
case e of
Left (x, y) -> (x, Left y)
Right (x, z) -> (x, Right z)
\end{Verbatim}
\src{code/haskell/snippet35.hs}
The \code{case of} statement is used for pattern matching inside
functions. Each pattern is followed by an arrow and the expression to be
evaluated when the pattern matches. For instance, if you call
\code{prodToSum} with the value:
\begin{Verbatim}
prod1 :: (Int, Either String Float)
prod1 = (2, Left "Hi!")
\end{Verbatim}
\src{code/haskell/snippet36.hs}
the \code{e} in \code{case e of} will be equal to
\code{Left "Hi!"}. It will match the pattern \code{Left y},
substituting \code{"Hi!"} for \code{y}. Since the \code{x} has
@ -497,9 +402,7 @@ The list type is quite interesting, because it's defined as a solution
to an equation. The type we are defining appears on both sides of the
equation:
\begin{Verbatim}
data List a = Nil | Cons a (List a)
\end{Verbatim}
\src{code/haskell/snippet37.hs}
If we do our usual substitutions, and also replace \code{List a} with
\code{x}, we get the equation:

View File

@ -0,0 +1,2 @@
swap :: (a, b) -> (b, a)
swap (x, y) = (y, x)

View File

@ -0,0 +1 @@
((a, b), c)

View File

@ -0,0 +1 @@
(a, (b, c))

View File

@ -0,0 +1,2 @@
alpha :: ((a, b), c) -> (a, (b, c))
alpha ((x, y), z) = (x, (y, z))

View File

@ -0,0 +1,2 @@
alpha_inv :: (a, (b, c)) -> ((a, b), c)
alpha_inv (x, (y, z)) = ((x, y), z)

View File

@ -0,0 +1 @@
(a, ())

View File

@ -0,0 +1,2 @@
rho :: (a, ()) -> a
rho (x, ()) = x

View File

@ -0,0 +1,2 @@
rho_inv :: a -> (a, ())
rho_inv x = (x, ())

View File

@ -0,0 +1 @@
data Pair a b = P a b

Some files were not shown because too many files have changed in this diff Show More