123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420 |
- % Copyright (C) 2017 Koz Ross <koz.ross@retro-freedom.nz>
- % This work is licensed under the Creative Commons Attribution-ShareAlike 4.0
- % International License. To view a copy of this license, visit
- % http://creativecommons.org/licenses/by-sa/4.0/ or send a letter to Creative
- % Commons, PO Box 1866, Mountain View, CA 94042, USA.
- \documentclass{beamer}
- \usepackage[utf8]{inputenc}
- \usecolortheme{seahorse}
- \usefonttheme{professionalfonts}
- \usepackage{fontspec}
- \setmainfont{DejaVu Sans}
- \setbeamertemplate{navigation symbols}{}
- \usepackage{caption}
- \usepackage[font=itshape, begintext=``, endtext='']{quoting}
- \usepackage{fancyvrb}
- \usepackage{color}
- \title{Functors}
- \subtitle{Or: why your abstractions are weak}
- \titlegraphic{\includegraphics[scale=0.8]{img/logo.pdf}}
- \author{Koz Ross}
- \date{18th May, 2017}
- \begin{document}
- \begin{frame}[c]
- \titlepage{}
- \end{frame}
- \begin{frame}[c]
- \frametitle{Outline}
- \tableofcontents
- \end{frame}
- \section{Introduction}
- \begin{frame}
- \frametitle{Things we want to have when programming}
-
- When we write code, all the following are pretty vital:\pause{}
- \bigskip
- \begin{itemize}
- \item Error handling (unlabelled and labelled)\pause{}
- \item Nondeterminism (multiple answers)\pause{}
- \item Side effects (file handling, GUIs, database operations,\ldots)\pause{}
- \item Metadata handling (information about data)\pause{}
- \item Containers (lists, dictionaries, trees,\ldots)\pause{}
- \end{itemize}
-
- \bigskip
- These things are very different, aren't they?\pause{} Your programming
- languages sure seem to think so\ldots
- \end{frame}
- \begin{frame}[c,fragile]
- \frametitle{The truth}
- \begin{center}
- \includegraphics[scale=0.65]{img/morpheus.pdf}
- \pause{}
- \bigskip
- Yes, your languages have been \alert{{\em lying\/}} to you.
- \end{center}
- \end{frame}
- \begin{frame}
- \frametitle{The fantastic functor}
- The {\em functor\/} is an abstraction which unifies {\em all\/} of the above:
- we can code to functors, and that code will {\em provably\/} work
- \alert{for every single one of those cases}.\pause{} Well, and plenty more
- besides\ldots\pause{}
- \bigskip
- Functors have been known about for {\em over forty years},
- and have been implemented in programming languages {\em since 1990}.\pause{}
- They are easy to understand, easy to use, and generally awesome.\pause{}
- \bigskip
- \alert{If your `high-level' language doesn't have them, your language is {\em weak}.}\pause{}
- If you haven't been {\em taught\/} them, \alert{your {\em instructors\/}
- are weak} (pointing no fingers, of course).\pause{}
- \bigskip
- \begin{center}
- \Large Let's fix this, shall we?
- \end{center}
- \end{frame}
- \section{Some formalisms}
- \begin{frame}[fragile]
- \frametitle{Types}
- A {\em type\/} is a set of rules.\pause{} {\em Values\/} can have types (which
- indicate what we can do with them), but {\em variables\/} can have them too
- (and that tells us what values they can hold).\pause{}
- \bigskip
- \begin{Verbatim}[commandchars=\\\{\}]
- \color{gray}-- I'm a comment!
- 1 :: Int \color{gray}-- we're asserting that 1 is an Int
- 1 :: Real \color{gray}-- same look, different meaning
- (3, 2.5) :: (Int, Real) \color{gray}-- a pair
- ["foo", "bar", "baz"] :: [String] \color{gray}--a list\pause{}
- x :: Int \color{gray}-- the variable x holds ints (declaration)
- x = 10 \color{gray}-- specifically this one (definition)\pause{}
- plus :: Int -> Int -> Int \color{gray}-- functions have types too!
- plus x y = x + y \color{gray}-- and definitions
- \end{Verbatim}
- \end{frame}
- \begin{frame}[fragile]
- \frametitle{Type parameterization}
- Instead of giving a type, we can use a {\em type parameter\/}:\pause{}
- \bigskip
- \begin{Verbatim}[commandchars=\\\{\}]
- \color{gray}-- take a value of any type, return one of the same
- id :: a -> a
- id x = x \color{gray}-- we're gonna see this one too!\pause{}
- \color{gray}-- we can have as many type parameters as we want!
- swap :: (a, b) -> (b, a)
- swap (x,y) = (y,x) \color{gray}-- just like you expected
- \end{Verbatim}
- \pause{}
-
- \bigskip
- We will typically use \verb+a,b+ for type parameters.
- \end{frame}
- \begin{frame}[fragile]
- \frametitle{Our own types}
- We can define our own types by putting together descriptions of what they
- contain, based on existing types:\pause{}
- \bigskip
- \begin{Verbatim}[commandchars=\\\{\}]
- \color{gray}-- similar to a struct
- \color{gray}-- type name on left, constructor name on right
- data Name = Name \{ first :: String, last :: String \}\pause{}
-
- \color{gray}-- similar to an enum
- data Colour = Red | Green | Blue\pause{}
- \color{gray}-- we can mix these two forms
- \color{gray}-- can be parametrized by type(s) if we wish
- data Maybe a = Nothing | Just a
- data Either a b = Left a | Right b\pause{}
- \end{Verbatim}
- \end{frame}
- \begin{frame}[fragile]
- \frametitle{Type classes}
- Similar to interfaces or protocols --- define some operations which might
- exist on different types, but should behave similarly.\pause{} Like
- interfaces, also tend to have additional rules about what they should do which
- the compiler cannot check:\pause{}
- \bigskip
- \begin{Verbatim}[commandchars=\\\{\}]
- \color{gray}-- a type class for things which can be compared
- class Eq a where
- \color{gray}-- instances must have these defined for them
- == :: a -> a -> Bool
- /= :: a -> a -> Bool\pause{}
- instance Eq Int where
- == x y = \color{gray}-- fill in whatever
- /= x y = \color{gray}-- same here\pause{}
- \end{Verbatim}
- \end{frame}
- \begin{frame}[fragile]
- \frametitle{Pure and impure code}
- Code is {\em pure\/} if it {\em always\/} returns the same result when given
- the same arguments, {\em and\/} has no side effects.\pause{} For example, the
- {\tt +} function is pure, but something like {\tt print} or {\tt random} aren't.
- \pause{} Code which is not pure is {\em impure\/} (or {\em
- side-effecting\/}).\pause{}
- \bigskip
- Most languages default to {\em everything\/} being as impure as possible ---
- any line of code can do anything at all, and it's up to {\em us\/} to make
- sure they all behave.\pause{} This is a huge pain:\pause{}
-
- \begin{itemize}
- \item We have to keep it straight in our heads\pause{}
- \item No telling what an arbitrary function will do\pause{}
- \item No guarantees that our impurity is limited in any way!\pause{}
- \end{itemize}
-
- This seems rather strange --- why not have {\em pure\/} code be the default,
- and then use the type system to {\em state\/} what other behaviour we want to
- have?
- \end{frame}
- \begin{frame}[fragile]
- \frametitle{Marking impurity using the type system}
- \pause{}
- \begin{Verbatim}[commandchars=\\\{\}]
- \color{gray}-- unlabelled error (divide by zero)
- divide :: Real -> Real -> Maybe Real\pause{}
- \color{gray}-- labelled error (lots can go wrong)
- parseInt :: String -> Either ParseError Int\pause{}
- \color{gray}-- nondeterminism (from zero to two roots)
- sqrt :: Real -> [Real]\pause{}
- \color{gray}-- or whatever the hell (probably web-based here...)
- getMeme :: URL -> MemeType -> IO Meme\pause{}
- \color{gray}-- we know these functions' side effects\pause{}
- \color{gray}-- and we *didn't even have to read them*!
- \end{Verbatim}
- \end{frame}
- \begin{frame}[fragile]
- \frametitle{A problem}
-
- \pause{}
- \begin{Verbatim}[commandchars=\\\{\}]
- \color{gray}-- suppose we have this eminently-sensible function
- square :: Real -> Real
- square x = x * x\pause{}
- \color{gray}-- we want to do this, but it won't work
- lifeTheUniverseAndEverything = square(sqrt(42))\pause{}
- \color{gray}-- this is because sqrt gives us a [Real]
- \color{gray}-- but square wants a plain Real\pause{}
- \end{Verbatim}
- \bigskip
- It seems all we can do is re-write every single thing to handle every single
- condition possible, which is ridiculous and impossible.\pause{} We
- \alert{deserve} better from our languages!
- \end{frame}
- \begin{frame}[fragile, c]
- \frametitle{What you're probably thinking now}
- \includegraphics[scale=0.125]{img/get-on-with-it.pdf}
- \end{frame}
- \section{The functor revealed}
- \begin{frame}[fragile]
- \frametitle{What a functor really is}
- \pause{}
- \begin{Verbatim}[commandchars=\\\{\}]
- class Functor f where
- map :: a -> b -> f a -> f b
- \end{Verbatim}
- \pause{}
- \bigskip
- Furthermore, we require that the following hold for any functor:\pause{}
- \begin{Verbatim}[commandchars=\\\{\}]
- \color{gray}--compiler can't check this, sadly, so we must
- map id == id
- \end{Verbatim}
- \pause{}
- \bigskip
- We call this the {\em functor law}.
- \end{frame}
- \begin{frame}[fragile]
- \frametitle{Wait, what?}
- \pause{}
- Maybe this will help (it's the same thing really):
- \bigskip
- \begin{Verbatim}[commandchars=\\\{\}]
- class Functor f where
- map :: (a -> b) -> (f a -> f b)
- \end{Verbatim}
- \pause{}
- \bigskip
- \verb+map+ transforms a pure function into a function with a side effect
- described by the type of the functor.\pause{} So as long as our type has a
- functor definition, we can use {\em any\/} pure function with it.\pause{}
- \bigskip
- We can define (correct) functor instances for \verb+Maybe+,\pause{}
- \verb+Either+,\pause{} \verb+[]+,\pause{} \verb+(,)+,\pause{}
- \verb+IO+,\pause{} most container types,\ldots
- \end{frame}
- \begin{frame}[fragile]
- \frametitle{Solving both our problems}
- Because of \verb+map+, our original problems of `type incompatibility' no
- longer exist:\pause{}
- \bigskip
- \begin{Verbatim}[commandchars=\\\{\}]
- \color{gray}-- this now works!
- lifeTheUniverseAndEverything = map square (sqrt 42)
- \color{gray}-- what do you think its type would be?\pause{}
- lifeTheUniverseAndEverything :: [Real]
- \end{Verbatim}
- \pause{}
- \bigskip
- Furthermore, we can define (correct) functors for {\em all\/} the types which
- describe all the effects we mentioned earlier. Now, we can treat them all the
- same, just by writing functions against \verb+Functor+ instead.\pause{} What's
- more, this requires {\em no special support from the language\/} --- if we can
- define the functor, we can do this!
- \end{frame}
- \begin{frame}[fragile]
- \frametitle{An example functor: Maybe}
- \pause{}
- \begin{Verbatim}[commandchars=\\\{\}]
- instance Functor Maybe where\pause{}
- map :: (a -> b) -> (Maybe a -> Maybe b)\pause{}
- map g Nothing = \pause{}Nothing \color{gray}-- no other choice\pause{}
- map g (Just x) = \pause{}Just (g x) \color{gray}-- apply and rewrap\pause{}
- \end{Verbatim}
- \bigskip
- Of course, we now need to check that the functor law is obeyed.\pause{} We can {\em
- prove\/} that this is the case (and pretty easily too).
- \end{frame}
- \begin{frame}[fragile]
- \frametitle{Proving the functor law for Maybe}
- \begin{lemma}
- Our definition of \verb+Maybe+ follows the functor law.
- \end{lemma}\pause{}
- \bigskip
- \begin{proof}
- We must show that, for our definition of \verb+Maybe+, we have:
- \begin{Verbatim}[commandchars=\\\{\}]
- map id == id
- \end{Verbatim}
- \pause{}
- If \verb+Maybe a == Nothing+, we have:\pause{}
- \begin{Verbatim}[commandchars=\\\{\}]
- map id Nothing == id Nothing\pause{}
- => Nothing == Nothing\pause{}
- \end{Verbatim}
- Otherwise, \verb+Maybe a == Just x+, and we have:\pause{}
- \begin{Verbatim}[commandchars=\\\{\}]
- map id (Just x) == id (Just x)\pause{}
- => Just (id x) == Just x\pause{}
- => Just x == Just x\pause{}
- \end{Verbatim}
- Thus, our definition of \verb+Maybe+ follows the functor law.
- \end{proof}
- \end{frame}
- \section{Limitations of functors}
- \begin{frame}[fragile]
- \frametitle{What functors {\em can't\/} do}
- \pause{}
- \begin{itemize}
- \item Can't apply functions with side-effect markers. If we want to apply a
- \verb+Maybe (Int -> Int)+ to a \verb+Maybe Int+, functors are of no
- help.\pause{}
- \item `Chaining together' functors stacks markers instead of collapsing
- them. If we tried do \verb+map sqrt (sqrt 42)+, we probably want a
- \verb+[Real]+, but what we actually get is \verb+[[Real]]+.\pause{}
- \end{itemize}
- \bigskip
- Luckily for us, there are other, more powerful abstractions built on the
- functor which solve {\em both\/} of these problems.
- \end{frame}
- \section{Questions}
- \begin{frame}[fragile, c]
- \frametitle{Questions?}
- \begin{center}
- \includegraphics[scale=0.27]{img/questions.pdf}
- \end{center}
- \end{frame}
- \end{document}
|