Created 2020-04-04 Sat 22:32

#+OPTIONS: toc:nil d:nil #+OPTIONS: toc:nil d:nil #+TITLE: Haskell CheatSheet #+AUTHOR: [[https://alhassy.github.io/][Musa Al-hassy]] #+export_file_name: README.org

A reference sheet for the basics of the mind-expanding Haskell language (•̀ᴗ•́)و

#+begin_quote The listing sheet, as PDF, can be found [[https://alhassy.github.io/HaskellCheatSheet/CheatSheet.pdf][here]], or as a [[https://alhassy.github.io/HaskellCheatSheet/CheatSheet_Portrait.pdf][single column portrait]], while below is an unruly html rendition. #+end_quote

This reference sheet is built from a [[https://github.com/alhassy/CheatSheet][CheatSheets with Org-mode]] system.

#+html:

#+toc: headlines 2 #+macro: blurb A reference sheet for the basics of the mind-expanding Haskell language (•̀ᴗ•́)و

#+latex_header: \usepackage{titling,parskip} #+latex_header: \usepackage{eufrak} % for mathfrak fonts #+latex_header: \usepackage{multicol,xparse,newunicodechar}

#+latex_header: \usepackage{etoolbox}

#+latex_header: \newif\iflandscape #+latex_header: \landscapetrue

#+latex_header_extra: \iflandscape \usepackage[landscape, margin=0.5in]{geometry} \else \usepackage[margin=0.5in]{geometry} \fi

#+latex_header: \def\cheatsheetcols{2} #+latex_header: \AfterEndPreamble{\begin{multicols}{\cheatsheetcols}} #+latex_header: \AtEndDocument{ \end{multicols} }

#+latex_header: \let\multicolmulticols\multicols #+latex_header: \let\endmulticolmulticols\endmulticols #+latex_header: \RenewDocumentEnvironment{multicols}{mO{}}{\ifnum#1=1 #2 \def\columnbreak{} \else \multicolmulticols{#1}[#2] \fi}{\ifnum#1=1 \else \endmulticolmulticols\fi}

#+latex_header: \def\maketitle{} #+latex: \fontsize{9}{10}\selectfont

#+latex_header: \def\cheatsheeturl{}

#+latex_header: \usepackage[dvipsnames]{xcolor} % named colours #+latex: \definecolor{grey}{rgb}{0.5,0.5,0.5}

#+latex_header: \usepackage{color} #+latex_header: \definecolor{darkgreen}{rgb}{0.0, 0.3, 0.1} #+latex_header: \definecolor{darkblue}{rgb}{0.0, 0.1, 0.3} #+latex_header: \hypersetup{colorlinks,linkcolor=darkblue,citecolor=darkblue,urlcolor=darkgreen}

#+latex_header: \setlength{\parindent}{0pt}

#+latex_header: \def\cheatsheetitemsep{-0.5em} #+latex_header: \let\olditem\item #+latex_header_extra: \def\item{\vspace{\cheatsheetitemsep}\olditem}

#+latex_header: \usepackage{CheatSheet/UnicodeSymbols}

#+latex_header: \makeatletter #+latex_header: \AtBeginEnvironment{minted}{\dontdofcolorbox} #+latex_header: \def\dontdofcolorbox{\renewcommand\fcolorbox[4][]{##4}} #+latex_header: \makeatother

#+latex_header: \RequirePackage{fancyvrb} #+latex_header: \DefineVerbatimEnvironment{verbatim}{Verbatim}{fontsize=\scriptsize}

#+macro: newline @@latex: \newline@@

#+latex_header: \def\cheatsheeturl{https://github.com/alhassy/HaskellCheatSheet}

#+latex_header: \def\cheatsheetcols{2} #+latex_header: \landscapetrue #+latex_header: \def\cheatsheetitemsep{-0.5em}

#+latex_header: \newunicodechar{𝑻}{\ensuremath{T}} #+latex_header: \newunicodechar{⊕}{\ensuremath{\oplus}} #+latex_header: \newunicodechar{≈}{\ensuremath{\approx}} #+latex_header: \newunicodechar{𝓍}{\ensuremath{x}} #+latex_header: \newunicodechar{α}{\ensuremath{\alpha}} #+latex_header: \newunicodechar{β}{\ensuremath{\beta}} #+latex_header: \newunicodechar{ε}{\ensuremath{\epsilon}} #+latex_header: \newunicodechar{∂}{\ensuremath{\partial}} #+latex_header: \newunicodechar{⊝}{\ensuremath{\ominus}} #+latex_header: \newunicodechar{₋}{\ensuremath{_-}} #+latex_header: \newunicodechar{⟶}{\ensuremath{\rightarrow}} #+latex_header: \newunicodechar{∉}{\ensuremath{\not\in}} #+latex_header: \newunicodechar{ }{\ensuremath{;;}}

#+begin_quote

• [[#hello-home][Hello, Home!]]
• [[#pattern-matching][Pattern Matching]]
• [[#local-bindings][Local Bindings]]
• [[#operators][Operators]]
• [[#types][Types]]
• [[#tuples][Tuples]]
• [[#lists][Lists]]
  • [[#pattern-matching-on-lists][Pattern Matching on Lists]]
  • [[#common-methods-on-lists][Common Methods on Lists]]
• [[#list-design-patterns][List ‘Design Patterns’]]
  • [[#map][Map]]
  • [[#filter][Filter]]
  • [[#fold][Fold]]
• [[#algebraic-data-types][Algebraic data types]]
• [[#typeclasses-and-overloading][Typeclasses and overloading]]
• [[#functor][Functor]]
  • [[#identity-axiom][Identity Axiom]]
  • [[#fusion-axiom][Fusion Axiom]]
  • [[#functors-do-not-necessarily-contain-anything][Functors do not necessarily ‘contain’ anything]]
  • [[#misc-results-about-functors][Misc results about Functors]]
• [[#functor-examples][Functor Examples]]
• [[#applicative][Applicative]]
  • [[#axioms][Axioms]]
  • [[#canonical-form----liftn][Canonical Form -- =liftN=]]
  • [[#monoidal-presentation][Monoidal Presentation]]
• [[#applicative-examples][Applicative Examples]]
• [[#do-notation----subtle-difference-between-applicatives-and-monads][~Do~-Notation ---Subtle difference between applicatives and monads]]
  • [[#do-notation-with-tuples-and-functions][Do-notation with tuples and functions]]
• [[#formal-definition-of-do-notation][Formal Definition of ~Do~-Notation]]
• [[#monad-laws][Monad Laws]]
• [[#monad-examples][Monad Examples]]
• [[#running-example----a-simple-arithmetic-language][Running Example ---A Simple Arithmetic Language]]
• [[#maybe----possibly-failing-computations][Maybe ---Possibly Failing Computations]]
• [[#writer----logging-information-as-we-compute][Writer ---Logging Information as we Compute]]
• [[#reader----accessing-global-read-only-data][Reader ---Accessing ‘Global, read-only, data’]]
• [[#state----read-and-write-to-local-storage][State ---Read and write to local storage]]
• [[#reads][Reads]] #+end_quote

• Hello, Home!

#+begin_src haskell :tangle home.hs main = do putStr "What's your name? " name <- getLine putStrLn ("It's 2020, " ++ name ++ "! Stay home, stay safe!") #+end_src

• Pattern Matching

Functions can be defined using the usual ~if_then_else_~ construct, or as expressions /guarded/ by Boolean expressions as in mathematics, or by /pattern matching/ ---a form of ‘syntactic comparision’.

#+begin_src haskell fact n = if n == 0 then 1 else n * fact (n - 1)

fact' n | n == 0 = 1 | n != 0 = n * fact' (n - 1)

fact'' 0 = 1 fact'' n = n * fact'' (n - 1) #+end_src

The above definitions of the factorial function are all equal.

Guards, as in the second version, are a form of ‘multi-branching conditional’.

In the final version, when a call, say, ~fact 5~ happens we compare /syntactically/ whether ~5~ and the first pattern ~0~ are the same. They are not, so we consider the second case with the understanding that an identifier appearing in a pattern matches /any/ argument, so the second clause is used.

Hence, when pattern matching is used, order of equations matters: If we declared the ~n~-pattern first, then the call ~fact 0~ would match it and we end up with ~0 * fact (-1)~, which is not what we want!

If we simply defined the final ~fact~ using /only/ the first clause, then ~fact 1~ would crash with the error /Non-exhaustive patterns in function fact/. That is, we may define /partial functions/ by not considering all possible shapes of inputs.

See also [[https://gitlab.haskell.org/ghc/ghc/-/wikis/view-patterns][“view patterns”]].

• Local Bindings

An equation can be qualified by a ~where~ or ~let~ clause for defining values or functions used only within an expression.

#+begin_src haskell …e…e…e where e = ℯ𝓍𝓅𝓇 ≈ let e = ℯ𝓍𝓅𝓇 in …ℯ𝓍𝓅𝓇…ℯ𝓍𝓅𝓇…ℯ𝓍𝓅𝓇 #+end_src

It sometimes happens in functional programs that one clause of a function needs /part of/ an argument, while another operators on the /whole/ argument. It it tedious (and inefficient) to write out the structure of the complete argument again when referring to it. Use the “as operator” ~@~ to label all or part of an argument, as in

#+begin_src haskell f label@(x:y:ys) = ⋯ #+end_src

• Operators Infix operators in Haskell must consist entiry of ‘symbols’ such as ~&, ^, !, …~ rather than alphanumeric characters. Hence, while addition, ~+~, is written infix, integer division is written prefix with ~div~.

We can always use whatever fixity we like:

• If ~f~ is any /prefix/ binary function, then ~x f y~ is a valid /infix/ call.
• If ~⊕~ is any /infix/ binary operator, then ~(⊕) x y~ is a valid /prefix/ call.

It is common to fix one argument ahead of time, e.g., ~λ x → x + 1~ is the successor operation and is written more tersely as ~(+1)~. More generally, ~(⊕r) = λ x → x ⊕ r~.

The usual arithmeic operations are ~+, /, *, -~ but ~%~ is used to make fractions.

The Boolean operations are ~==, /=, &&, ||~ for equality, discrepancy, conjunction, and disjunction.

• Types

Type are inferred, but it is better to write them explicitly so that /you communicate your intentions to the machine/. If you /think/ that expression ~e~ has type ~τ~ then write ~e :: τ~ to /communicate/ that to the machine, which will silently accept your claim or reject it loudly.

| Type | Name | Example Value | |--------------------+-------------+-----------------------| | Small integers | ~Int~ | ~42~ | | Unlimited integers | ~Integer~ | ~7376541234~ | | Reals | ~Float~ | ~3.14~ and ~2 % 5~ | | Booleans | ~Boolean~ | ~True~ and ~False~ | | Characters | ~Char~ | ~'a'~ and ~'3'~ | | Strings | ~String~ | ~"salam"~ | | Lists | ~[α]~ | ~[]~ or ~[x₁, …, xₙ]~ | | Tuples | ~(α, β, γ)~ | ~(x₁, x₂, x₃)~ | | Functions | ~α → β~ | ~λ x → ⋯~ |

/Polymorphism/ is the concept that allows one function to operate on different types.

• A function whose type contains /variables/ is called a /polymorphic function/.
• The simplest polymorphic function is ~id ∷ a -> a~, defined by ~id x = x~.

• Tuples

Tuples ~(α₁, …, αₙ)~ are types with values written ~(x₁, …, xₙ)~ where each ~xᵢ :: αᵢ~. The are a form of ‘record’ or ‘product’ type.

E.g., ~(True, 3, 'a') :: (Boolean, Int, Char)~.

Tuples are used to “return multiple values” from a function.

Two useful functions on tuples of length 2 are: #+begin_src haskell fst :: (α, β) → α fst (x, y) = x

snd :: (α, β) → β snd (x, y) = β #+end_src

If in addition you ~import Control.Arrow~ then you may use: #+begin_src haskell first :: (α → τ) → (α, β) → (τ, β) first f (x, y) = (f x, y)

second :: (β → τ) → (α, β) → (α, τ) second g (x, y) = (x, g y)

(***) :: (α → α′) → (β → β) → (α, β) → (α′, β′) (f *** g) (x, y) = (f x, g y)

(&&&) :: (τ → α) → (τ → β) → τ → (α, β) (f &&& g) x = (f x, g x) #+end_src

• Lists

Lists are sequences of items of the same type.

If each ~xᵢ ∷ α~ then ~[x₁, …, xₙ] ∷ [α]~.

Lists are useful for functions that want to ‘non-deterministicly’ return a value: They return a list of all possible values.

• The /empty list/ is ~[]~
• We “cons”truct nonempty lists using ~(:) ∷ α → [α] → [α]~
• Abbreviation: ~[x₁, …, xₙ] = x₁ ∶ (x₂ ∶ (⋯ (xₙ ∶ [])))~
• /List comprehensions/: ~[f x | x <- xs, p x]~ is the list of elements ~f x~ where ~x~ is an element from list ~xs~ and ~x~ satisfies the property ~p~
  • E.g., ~[2 * x | x <- [2, 3, 4], x < 4] ≈ [2 * 2, 2 * 3] ≈ [4, 6]~
• Shorthand notation for segments: ~u~ may be ommitted to yield /infinite lists/
  • ~[l .. u] = [l, l + 1, l + 2, …, u]~.
  • ~[a, b, .., u] = [a + i * step | i <- [0 .. u - a] ] where step = b - a~

Strings are just lists of characters: ~"c₀c₁…cₙ" ≈ ['c₀', …, 'cₙ']~.

• Hence, all list methods work for strings.

** Pattern Matching on Lists Pattern matching on lists #+begin_src haskell prod [] = 1 prod (x:xs) = x * prod xs

fact n = prod [1 .. n] #+end_src

If your function needs a case with a list of say, length 3, then you can match directly on that /shape/ via ~[x, y, z]~ ---which is just an abbreviation for the shape ~x:y:z:[]~. Likewise, if we want to consider lists of length /at least 3/ then we match on the shape ~x:y:z:zs~. E.g., define the function that produces the maximum of a non-empty list, or the function that removes adjacent duplicates ---both require the use of guards.

** Common Methods on Lists #+begin_src haskell [x₀, …, xₙ] !! i = xᵢ [x₀, …, xₙ] ++ [y₀, …, yₘ] = [x₀, …, xₙ, y₀, …, yₘ] concat [xs₀, …, xsₙ] = xs₀ ++ ⋯ ++ xsₙ

{- Partial functions -} head [x₀, …, xₙ] = x₀ tail [x₀, …, xₙ] = [x₁, …, xₙ] init [x₀, …, xₙ] = [x₀, …, xₙ₋₁] last [x₀, …, xₙ] = xₙ

take k [x₀, …, xₙ] = [x₀, …, xₖ₋₁] drop k [x₀, …, xₙ] = [xₖ, …, xₙ]

sum [x₀, …, xₙ] = x₀ + ⋯ + xₙ prod [x₀, …, xₙ] = x₀ * ⋯ * xₙ reverse [x₀, …, xₙ] = [xₙ, …, x₀] elem x [x₀, …, xₙ] = x == x₀ || ⋯ || x == xₙ

zip [x₀, …, xₙ] [y₀, …, yₘ] = [(x₀, y₀), …, (xₖ, yₖ)] where k = n min m unzip [(x₀, y₀), …, (xₖ, yₖ)] = ([x₀, …, xₖ], [y₀, …, yₖ]) #+end_src

[[https://en.wikipedia.org/wiki/Conjugacy_class][Duality]]: Let ~∂f = reverse . f . reverse~, then ~init = ∂ tail~ and ~take k = ∂ (drop k)~; even ~pure . head = ∂ (pure . last)~ where ~pure x = [x]~.

• List ‘Design Patterns’

Many functions have the same ‘form’ or ‘design pattern’, a fact which is taken advantage of by defining /higher-order functions/ to factor out the structural similarity of the individual functions.

** Map

~map f xs = [f x | x <- xs]~

• Transform all elements of a list according to the function ~f~.

** Filter ~filter p xs = [x | x <- xs, p x]~

• Keep only the elements of the list that satisfy the predicate ~p~.
• ~takeWhile p xs~ ≈ Take elements of ~xs~ that satisfy ~p~, but stop stop at the first element that does not satisfy ~p~.
• ~dropWhile p xs~ ≈ Drop all elements until you see one that does not satisfy the predicate.
• ~xs = takeWhile p xs ++ dropWhile p xs~.

** Fold Right-folds let us ‘sum’ up the elements of the list, associating to the right. #+begin_src haskell foldr (⊕) e ≈ λ (x₀ : (x₁ : (… : (xₙ : [])))) → (x₀ ⊕ (x₁ ⊕ (… ⊕ (xₙ ⊕ e)))) #+end_src

This function just replaces cons ~“∶”~ and ~[]~ with ~⊕~ and ~e~. That's all.

• E.g., replacing ~:,[]~ with themselves does nothing: ~foldr (:) [] = id~.

#+latex: \newpage /All functions on lists can be written as folds!/ #+begin_src haskell h [] = e ∧ h (x:xs) = x ⊕ h xs ≡ h = foldr (λ x rec_call → x ⊕ rec_call) e #+end_src

• Look at the two cases of a function and move them to the two first arguments of the fold.
  • ~map f = foldr (λ x ys → f x : ys) []~
  • ~filter p = foldr (λ x ys → if (p x) then (x:ys) else ys) []~
  • ~takeWhile p = foldr (λ x ys → if (p x) then (x:ys) else []) []~

You can also fold leftward, i.e., by associating to the left: #+begin_src haskell foldl (⊕) e ≈ λ (x₀ : (x₁ : (… : (xₙ : [])))) → (((e ⊕ x₀) ⊕ x₁) ⊕ … ) ⊕ xₙ #+end_src Unless the operation ~⊕~ is associative, the folds are generally different.

• E.g., ~foldl (/) 1 [1..n] ≈ 1 / n!~ where ~n ! = product [1..n]~.
• E.g., ~-55 = foldl (-) 0 [1..10] ≠ foldr (-) 0 [1..10] = -5~.

If ~h~ swaps arguments ---~h(x ⊕ y) = h y ⊕ h x~--- then ~h~ swaps folds:

~h . foldr (⊕) e = foldl (⊝) e′~ where ~e′ = h e~ and ~x ⊝ y = x ⊕ h y~.

E.g., ~foldl (-) 0 xs = - (foldr (+) 0 xs) = - (sum xs)~ and ~n ! = foldr (*) 1 [1..n] = 1 / foldl (/) 1 [1..n]~.

| /( Floating points are a leaky abstraction! )/ |

• Algebraic data types

When we have ‘possible scenarios’, we can make a type to consider each option. E.g., ~data Door = Open | Closed~ makes a new datatype with two different values. Under the hood, ~Door~ could be implemented as integers and ~Open~ is 0 and ~Closed~ is 1; or any other implementation ---/all that matters/ is that we have a new type, ~Door~, with two different values, ~Open~ and ~Closed~.

Usually, our scenarios contain a ‘payload’ of additional information; e.g., ~data Door2 = Open | Ajar Int | Closed~. Here, we have a new way to construct ~Door~ values, such as ~Ajar 10~ and ~Ajar 30~, that we could interpret as denoting how far the door is open/. Under the hood, ~Door2~ could be implemented as pairs of integers, with ~Open~ being ~(0,0)~, ~Ajar n~ being ~(1, n)~, and ~Closed~ being ~(2, 0)~ ---i.e., as the pairs “(value position, payload data)”. Unlike functions, a value construction such as ~Ajar 10~ cannot be simplified any further; just as the list value ~1:2:3:[]~ cannot be simplified any further. Remember, the representation under the hood does not matter, what matters is that we have three possible /construction forms/ of ~Door2~ values.

Languages, such as C, which do not support such an “algebraic” approach, force you, the user, to actually choose a particular representation ---even though, it does not matter, since we only want /a way to speak of/ “different cases, with additional information”.

In general, we declare the following to get an “enumerated type with payloads”. #+begin_src haskell data D = C₀ τ₁ τ₂ … τₘ | C₁ ⋯ | Cₙ ⋯ deriving Show #+end_src There are =n= constructors ~Cᵢ~ that make /different/ values of type ~D~; e.g., ~C₀ x₁ x₂ … xₘ~ is a ~D~-value whenever each ~xᵢ~ is a ~τᵢ~-value. The ~“deriving Show”~ at the end of the definition is necessary for user-defined types to make sure that values of these types can be printed in a standard form.

We may now define functions on ~D~ by pattern matching on the possible ways to /construct/ values for it; i.e., by considering the cases ~Cᵢ~.

In-fact, we could have written ~data D α₁ α₂ … αₖ = ⋯~, so that we speak of “D values /parameterised/ by types αᵢ”. E.g., “lists whose elements are of type α” is defined by ~data List α = Nil | Cons α (List α)~ and, for example, ~Cons 1 (Cons 2 Nil)~ is a value of ~List Int~, whereas ~Cons 'a' Nil~ is of type ~List Char~. ---The ~List~ type is missing the ~“deriving Show”~, see below for how to /mixin/ such a feature.

For example, suppose we want to distinguish whether we have an α-value or a β-value, we use ~Either~. Let's then define an example /infix/ function using pattern matching. #+begin_src haskell data Either α β = Left α | Right β

(+++) :: (α → α′) → (β → β′) → Either α β → Either α′ β′ (f +++ g) (Left x) = Left $ f x (f +++ g) (Right x) = Right $ g x

right :: (β → τ) → Either α β → Either α τ right f = id +++ f #+end_src The above ~(+++)~ can be found in ~Control.Arrow~ and is also known as ~either~ in the standard library.

• Typeclasses and overloading

/Overloading/ is using the same name to designate operations “of the same nature” on values of different types.

E.g., the ~show~ function converts its argument into a string; however, it is not polymorphic: We cannot define ~show :: α → String~ with one definition since some items, like functions or infinite datatypes, cannot be printed and so this is not a valid type for the function ~show~.

Haskell solves this by having ~Show~ /typeclass/ whose /instance types/ ~α~ each implement a definition of the /class method/ ~show~. The type of ~show~ is written ~Show α => α -> String~: /Given an argument of type ~α~, look in the global listing of ~Show~ instances, find the one for ~α~, and use that;/ if ~α~ has no ~Show~ instance, then we have a type error. One says “the type variable ~α~ has is /restricted/ to be a ~Show~ instance” ---as indicated on the left side of the ~“=>”~ symbol.

E.g., for the ~List~ datatype we defined, we may declare it to be ‘showable’ like so: #+begin_quote #+begin_src haskell -n 1 instance Show a => Show (List a) where show Nil = "Nope, nothing here" show (Cons x xs) = "Saw " ++ show x ++ ", then " ++ show xs #+end_src #+end_quote That is:

1. /If ~a~ is showable, then ~List a~ is also showable./
2. /Here's how to show ~Nil~ directly./
3. /We show ~Cons x xs~ by using the ~show~ of ~a~ on ~x~, then recursively showing ~xs~./

| | Common Typeclasses | |---------------+----------------------------------------------------| | ~Show~ | Show elements as strings, ~show~ | | ~Read~ | How to read element values from strings, ~read~ | | ~Eq~ | Compare elements for equality, ~==~ | | ~Num~ | Use literals ~0, 20, …,~ and arithmetic ~+, *, -~ | | ~Ord~ | Use comparison relations ~>, <, >=, <=~ | | ~Enum~ | Types that can be listed, ~[start .. end]~ | | ~Monoid~ | Types that model ‘(untyped) composition’ | | ~Functor~ | /Type formers/ that model effectful computation | | ~Applicative~ | Type formers that can sequence effects | | ~Monad~ | Type formers that let effects depend on each other |

The ~Ord~ typeclass is declared ~class Eq a => Ord a where ⋯~, so that all ordered types are necessarily also types with equality. One says ~Ord~ is a /subclass/ of ~Eq~; and since subclasses /inherit/ all functions of a class, we may always replace ~(Eq a, Ord a) => ⋯~ by ~Ord a => ⋯~.

You can of-course define your own typeclasses; e.g., the ~Monoid~ class in Haskell could be defined as follows. #+begin_src haskell class Semigroup a where (<>) :: a -> a -> a {- A way to “compose” elements together -} {- Axiom: (x <> y) <> z = x <> (y <> z) -}

class Semigroup a => Monoid a where mempty :: a {- Axiom: This is a ‘no-op’, identity, for composition <> -} #+end_src Example monoids ~(α, <>, mempty)~ include ~(Int, +, 0)~, ~([α], ++, [])~, and (Program statements, sequence “;”, the empty statement) ---this last example is approximated as ~Term~ with ‘let-in’ clauses at the end of this cheatsheet. /Typeclasses are interfaces, possibly with axioms specifying their behaviour./

As shown earlier, Haskell provides a the ~deriving~ mechanism for making it easier to define instances of typeclasses, such as ~Show, Read, Eq, Ord, Enum~. How? Constructor names are printed and read as written as written in the ~data~ declaration, two values are equal if they are formed by the same construction, one value is less than another if the constructor of the first is declared in the ~data~ definition before the constructor of the second, and similarly for listing elements out.

• Functor

/Functors are type formers that “behave” like collections: We can alter their/ /“elements” without messing with the ‘collection structure’ or ‘element positions’./ The well-behavedness constraints are called /the functor axioms/. #+begin_src haskell class Functor f where fmap :: (α → β) → f α → f β

(<$>) = fmap {- An infix alias -} #+end_src

The axioms cannot be checked by Haskell, so we can form instances that fail to meet the implicit specifications ---two examples are below.

** Identity Axiom

Identity Law: ~fmap id = id~

/Doing no alteration to the contents of a collection does nothing to the collection./

This ensures that “alterations don't needlessly mess with element values” e.g., the following is not a functor since it does. #+begin_src haskell :tangle probably.hs {- I probably have an item -} data Probably a = Chance a Int

instance Functor Probably where fmap f (Chance x n) = Chance (f x) (n div 2) #+end_src

** Fusion Axiom Fusion Law: ~fmap f . fmap g = fmap (f . g)~

/Reaching into a collection and altering twice is the same as reaching in and altering once./

This ensures that “alterations don't needlessly mess with collection structure”; e.g., the following is not a functor since it does.

#+begin_src haskell :tangle pocket.hs import Prelude hiding (Left, Right)

{- I have an item in my left or my right pocket -} data Pocket a = Left a | Right a

instance Functor Pocket where fmap f (Left x) = Right (f x) fmap f (Right x) = Left (f x) #+end_src

** Functors do not necessarily ‘contain’ anything

It is important to note that functors model well-behaved container-like types, but of-course the types do not actually need to contain anything at all! E.g., the following is a valid functor. #+begin_src haskell :tangle Liar.hs {- “I totally have an α-value, it's either here or there.” Lies! -} data Liar α = OverHere Int | OverThere Int

instance Functor Liar where fmap f (OverHere n) = OverHere n fmap f (OverThere n) = OverThere n #+end_src Notice that if we altered ~n~, say by dividing it by two, then we break the identity law; and if we swap the constructors, then we break the fusion law. Super neat stuff!

In general, functors take something boring and generally furnish it with ‘coherent’ structure, but there is not necessarily an α ‘inside’ f α. E.g., ~f α = (ε → α)~ has as values “recipes for forming an α-value”, but unless executed, there is no ~α~-value.

** Misc results about Functors

#+latex: \vspace{0.5em}

• ~fmap f xs~ ≈ /for each/ element ~x~ in the ‘collection’ ~xs~, yield ~f x~.
• Haskell can usually ~derive~ functor instances since they are [[http://archive.fo/U8xIY][unique]]: Only one possible definition of ~fmap~ will work.
• Reading the functor axioms left-to-right, they can be seen as /optimisation laws/ that make a program faster by reducing work.
• The two laws together say /fmap distributes over composition/: ~fmap (f₁ . f₂ . ⋯ . fₙ)  =  fmap f₁ . ⋯ . fmap fₙ~ for ~n ≥ 0~.

Naturality Theorems: If ~p ∷ f a → g a~ for some /functors/ ~f~ and ~g~, then ~fmap f . p  =  p . fmap f~ for any /function/ ~f~.

Hence, any generic property ~p ∷ f α → ε~ is invariant over fmaps: ~p(fmap f xs) = p xs~. E.g., the length of a list does not change even when an fmap is applied.

• Functor Examples

Let ~f₁, f₂~ be functors and ~ε~ be a given type.

| Type Former | ~f α~ | ~f <$> x~ | |-------------------------------------------------------------------------------------------------------------+------------------------+---------------------------------------| | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Functor-Identity.html#t:Identity][Identity]] | ~α~ | ~f <$> x = f x~ | | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Control-Applicative.html#t:Const][Constant]] | ~ε~ | ~f <$> x = x~ | | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/GHC-List.html][List]] | ~[α]~ | ~f <$> [x₀, …, xₙ] = [f x₀, …, f xₙ]~ | | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Either.html#t:Either][Either]] | ~Either ε α~ | ~f <$> x = right f~ | |-------------------------------------------------------------------------------------------------------------+------------------------+---------------------------------------| | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Functor-Product.html#t:Product][Product]] | ~(f₁ α, f₂ α)~ | ~f <$> (x, y) = (f <$> x, f <$> y)~ | | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Functor-Compose.html#t:Compose][Composition]] | ~f₁ (f₂ α)~ | ~f <$> x = (fmap f) <$> x~ | | [[http://comonad.com/reader/2012/abstracting-with-applicatives/][Sum]] | ~Either (f₁ α) (f₂ α)~ | ~f <$> ea = f +++ f~ | |-------------------------------------------------------------------------------------------------------------+------------------------+---------------------------------------| | [[http://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Writer-Lazy.html#g:2][Writer]] | ~(ε, α)~ | ~f <$> (e, x) = (e, f x)~ | | [[https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Reader.html][Reader]] | ~ε → α~ | ~f <$> g = f . g~ | | [[https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-State-Lazy.html#g:2][State]] | ~ε → (ε, α)~ | ~f <$> g = second f . g~ |

Notice that writer is the product of the constant and the identity functors.

Unlike reader, the type former ~f α = α → ε~ is /not/ a functor since there is no way to implement ~fmap~. In contrast, ~f α = (α → ε, α)~ /does/ have an implementation of ~fmap~, but it is not lawful.

• Applicative /Applicatives are collection-like types that can apply collections of functions to collections of elements./

In particular, /applicatives can fmap over multiple arguments/; e.g., if we try to add ~Just 2~ and ~Just 3~, we find =(+) <$> Just 2 :: Maybe (Int → Int)= and this is not a function and so cannot be applied further to ~Just 3~ to get ~Just 5~. We have both the function and the value wrapped up, so we need a way to apply the former to the latter. The answer is ~(+) <$> Just 2 <*> Just 3~.

#+begin_src haskell class Functor f => Applicative f where pure :: a -> f a (<*>) :: f (a -> b) -> f a -> f b {- “apply” -}

{- Apply associates to the left: p <> q <> r = (p <> q) <> r) -} #+end_src

The method ~pure~ lets us inject values, to make ‘singleton collections’.

• /Functors transform values inside collections; applicatives can additionally combine values inside collections./
• Exercise: If ~α~ is a monoid, then so too is ~f α~ for any applicative ~f~.

** Axioms The applicative axioms ensure that apply behaves like usual functional application:

• Identity: ~pure id <*> x = x~ ---c.f., ~id x = x~

• Homomorphism: ~pure f <*> pure x = pure (f x)~ ---it really is function application on pure values!

  • Applying a non-effectful function to a non-effectful argument in an effectful context is the same as just applying the function to the argument and then injecting the result into the content.

• Interchange: ~p <> pure x = pure ($ x) <> p~ ---c.f., ~f x = ($ x) f~

  • Functions ~f~ take ~x~ as input ≈ Values ~x~ project functions ~f~ to particular values
  • When there is only one effectful component, then it does not matter whether we evaluate the function first or the argument first, there will still only be one effect.
  • Indeed, this is equivalent to the law: ~pure f <> q = pure (flip ($)) <> q <*> pure f~.

• Composition: ~pure (.) <> p <> q <> r = p <> (q <*> r)~ ---c.f., ~(f . g) . h = f . (g . h)~.

If we view ~f α~ as an “effectful computation on α”, then the above laws ensure ~pure~ creates an “effect free” context. E.g., if ~f α = [α]~ is considered “nondeterminstic α-values”, then ~pure~ just treats usual α-values as nondeterminstic but with no ambiguity, and ~fs <> xs~ reads “if we nondeterminsticly have a choice ~f~ from ~fs~, and we nondeterminsticly an ~x~ from ~xs~, then we nondeterminsticly obtain ~f x~.” More concretely, if I'm given randomly addition or multiplication along with the argument 3 and another argument that could be 2, 4, or 6, then the result would be obtained by considering all possible combinations: ~[(+), ()] <> pure 3 <> [2, 4, 6] = [5,7,9,6,12,18]~. The name ~“<*>”~ is suggestive of this ‘cartesian product’ nature.

Given a definition of apply, the definition of ~pure~ may be obtained by unfolding the identity axiom.

Using these laws, we regain the original ~fmap~ ---since ~fmap~'s are [[http://archive.fo/U8xIY][unique]] in Haskell--- thereby further cementing that applicatives model “collections that can be functionally applied”: ~f <$> x = pure f <*> x~. ( Hence, every applicative is a functor whether we like it or not. )

• The identity applicative law is then just the identity law of functor: ~id <$> x = x~.

• The homomorphism law now becomes: ~pure . f = fmap f . pure~.

  • This is the “naturality law” for ~pure~.

** Canonical Form -- =liftN=

[[http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf][The laws]] may be interpreted as left-to-right rewrite rules and so are a procedure for transforming any applicative expression into the canonical form of “a pure function applied to effectful arguments”: ~pure f <> x₁ <> ⋯ <*> xₙ~. In this way, one can compute in-parallel the, necessarily independent, ~xᵢ~ then combine them together.

Notice that the canonical form generalises ~fmap~ to ~n~-arguments: Given ~f ∷ α₁ → ⋯ → αₙ → β~ and ~xᵢ ∷ f αᵢ~, we obtain an ~(f β)~-value. The case of ~n = 2~ is called ~liftA2~, ~n = 1~ is just ~fmap~, and for ~n = 0~ we have ~pure~! ** Monoidal Presentation

Notice that ~lift2A~ is essentially the cartesian product in the setting of lists, or ~(<&>)~ below ---c.f., ~sequenceA :: Applicative f ⇒ [f a] → f [a]~.

#+begin_src haskell (<&>) :: f a → f b → f (a, b) {- Not a standard name! -} (<&>) = liftA2 (,) -- i.e., p <&> q = (,) <$> p <*> q #+end_src This is a pairing operation with properties of ~(,)~ mirrored at the applicative level: #+begin_src haskell {- Pure Pairing -} pure x <&> pure y = pure (x, y) {- Naturality -} (f &&& g) <$> (u <&> v) = (f <$> u) <&> (g <&> v)

{- Left Projection -} fst <$> (u <&> pure ()) = u {- Right Projection -} snd <$> (pure () <&> v) = v {- Associtivity -} assocl <$> (u <&> (v <&> w)) = (u <&> v) <&> w #+end_src The final three laws above suffice to prove the original applicative axioms, and so we may define ~p <*> q = uncurry ($) <$> (p <&> q)~.

• Applicative Examples

Let ~f₁, f₂~ be functors and let ~ε~ a type.

| Functor | ~f α~ | ~f <> x~ | |-------------------------------------------------------------------------------------------------------------+------------------------+---------------------------------------------| | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Functor-Identity.html#t:Identity][Identity]] | ~α~ | ~f <> x = f x~ | | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Control-Applicative.html#t:Const][Constant]] | ~ε~ | ~e <> d = e <> d~ | | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/GHC-List.html][List]] | ~[α]~ | =fs <> xs = [f x ∣ f <- fs, x <- xs]= | | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Either.html#t:Either][Either]] | ~Either ε α~ | ~ef <> ea = right (λ f → right f ea) ef~ | |-------------------------------------------------------------------------------------------------------------+------------------------+---------------------------------------------| | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Functor-Compose.html#t:Compose][Composition]] | ~f₁ (f₂ α)~ | ~f <> x = (<>) <$> f <> x~ | | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Functor-Product.html#t:Product][Product]] | ~(f₁ α, f₂ α)~ | ~(f, g) <> (x, y) = (f <> x, g <> y)~ | | [[http://comonad.com/reader/2012/abstracting-with-applicatives/][Sum]] | ~Either (f₁ α) (f₂ α)~ | Challenge: Assume ~η ∷ f₁ a → f₂ a~ | |-------------------------------------------------------------------------------------------------------------+------------------------+---------------------------------------------| | [[http://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Writer-Lazy.html#g:2][Writer]] | ~(ε, α)~ | ~(a , f) <> (b, x) = (a <> b, f x)~ | | [[https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Reader.html][Reader]] | ~ε → α~ | ~f <> g = λ e → f e (g e)~ ---c.f., ~SKI~ | | [[https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-State-Lazy.html#g:2][State]] | ~ε → (ε, α)~ | ~sf <> sa = λ e → let (e′, f) = sf e~ | | | |                   ~in second f (sa e′)~ |

In the writer and constant cases, we need ~ε~ to also be a monoid. When ε is /not/ a monoid, then those two constructions give examples of functors that are /not/ applicatives ---since there is no way to define ~pure~. In contrast, ~f α = (α → ε) → Maybe ε~ is not an applicative since no definition of apply is lawful.

Since readers ~((->) r)~ are applicatives, we may, for example, write ~(⊕) <$> f <*> g~ as a terse alternative to the “pointwise ⊕” method ~λ x → f x ⊕ g x~. E.g., using ~(&&)~ gives a simple way to chain predicates.

• ~Do~-Notation ---Subtle difference between applicatives and monads Recall the ~map~ operation on lists, we could define it ourselves: #+begin_src haskell :tangle delme.hs map' :: (α -> β) -> [α] -> [β] map' f [] = [] map' f (x:xs) = let y = f x ys = map' f xs in (y:ys) #+end_src If instead the altering function ~f~ returned effectful results, then we could gather the results along with the effect: #+begin_src haskell :tangle delme1.hs {-# LANGUAGE ApplicativeDo #-}

mapA :: Applicative f => (a -> f b) -> [a] -> f [b] mapA f [] = pure [] mapA f (x:xs) = do y <- f x ys <- mapA f xs pure (y:ys) {- ≈ (:) <$> f x <*> mapA f xs -} #+end_src

Applicative syntax can be a bit hard to write, whereas ~do~-notation is more natural and reminiscent of the imperative style used in defining ~map'~ above. For instance, the intuition that ~fs <> ps~ is a cartesian product is clearer in do-notation: ~fs <> ps ≈ do {f ← fs; x ← ps; pure (f x)}~ where the right side is read /“for-each f in fs, and each x in ps, compute f x”/.

#+latex: \columnbreak

[[https://dl.acm.org/doi/pdf/10.1145/3241625.2976007][In-general]], ~do {x₁ ← p₁; …; xₙ ← pₙ; pure e} ≈ pure (λ x₁ … xₙ → e) <> p₁ <> ⋯ <*> pₙ~ provided ~pᵢ~ does not mention ~xⱼ~ for ~j < i~; but =e= may refer to all ~xᵢ~. If any ~pᵢ~ mentions an earlier ~xⱼ~, then we could not translate the ~do~-notation into an applicative expression.

If ~do {x ← p; y ← qx; pure e}~ has ~qx~ being an expression depending on ~x~, then we could say this is an abbreviation for ~(λ x → (λ y → e) <$> qx) <$> p~ but this is of type ~f (f β))~. Hence, to allow later computations to depend on earlier computations, we need a method ~join :: f (f α) → f α~ with which we define ~do {x ← p; y ← qx; pure e} ≈ join $ ~(λ x -> (λ y → e) <$> qx) <$> p~.

Applicatives with a ~join~ are called monads and they give us a “programmable semicolon”. Since later items may depend on earlier ones, ~do {x ← p; y ← q; pure e}~ could be read /“let x be the value of computation p, let y be the value of computation q, then combine the values via expression e”/. Depending on how ~<*>~ is implemented, such ‘let declarations’ could short-circuit (~Maybe~) or be nondeterministic (~List~) or have other effects such as altering state.

As the ~do~-notation clearly shows, the primary difference between =Monad= and =Applicative= is that =Monad= allows dependencies on previous results, whereas =Applicative= does not.

** Do-notation with tuples and functions

Do-syntax also works with tuples and functions --c.f., reader monad below--- since they are monadic; e.g., every clause ~x <- f~ in a functional do-expression denotes the resulting of applying ~f~ to the (implicit) input. More concretely: #+begin_src haskell go :: (Show a, Num a) => a -> (a, String) go = do {x <- (1+); y <- show; return (x, y)}

-- go 3 = (4, "3") #+end_src

Likewise, tuples, lists, etc.

• Formal Definition of ~Do~-Notation

For a general applicative ~f~, a ~do~ expression has the form ~do {C; r}~, where ~C~ is a (possibly empty) list of commands separated by semicolons, and ~r~ is an expression of type ~f β~, which is also the type of the entire ~do~ expression. Each command takes the form ~x ← p~, where ~x~ is a variable, or possibly a pattern; if ~p :: f α~ then ~x :: α~. In the particular case of the anonymous variable, ~_ ← p~ may be abbreviated to ~p~.

The translation of a ~do~ expression into ~<>/join~ operations and ~where~ clauses is governed by three rules ---the last one only applies in the setting of a monad. #+begin_src haskell (1) do {r} = r (2A) do {x ← p; C; r} = q <> p where q x = do {C; r} --Provided x ∉ C (2M) do {x ← p; C; r} = join $ map q p where q x = do {C; r}

{- Fact: When x ∉ C, (2A) = (2M). -} #+end_src

By definition chasing and induction on the number of commands ~C~, we have: #+begin_src haskell [CollapseLaw] do {C; do {D; r}} = do {C; D; r} #+end_src Likewise: #+begin_src haskell [Map ] fmap f p = do {x ← p; pure (f x)} -- By applicative laws [Join] join ps = do {p ← ps; p} -- By functor laws #+end_src

Do-Notation Laws: Here are some desirable usability properties of ~do~-notation. #+begin_src haskell [RightIdentity] do {B; x ← p; pure x} = do {B; p} [LeftIdentity ] do {B; x ← pure e; C; r} = do {B; C[x ≔ e]; r[x ≔ e]} [Associtivity ] do {B; x ← do {C; p}; D; r} = do {B; C; x ← p; D; r} #+end_src

Here, ~B, C, D~ range over sequences of commands and ~C[x ≔ e]~ means the sequence ~C~ with all free occruences of ~x~ replaced by ~e~.

• Associtivity gives us a nice way to ‘inline’ other calls.

• The LeftIdentity law, read right-to-left, lets us “locally give a name” to the possibly complex expression ~e~.

  If ~pure~ forms a singleton collection, then LeftIdentity is a “one-point rule”: We consider /all/ ~x ← pure e~, but there is only /one/ such ~x~, namely ~e~!

In the applicative case, where the clauses are independent, we can prove, say, ~RightIdentity~ using the identity law for applicatives ---which says essentially

~do {x <- p; pure x} = p~--- then apply induction on the length of ~B~.

What axioms are needed for the monad case to prove the ~do~-notation laws?

• Monad Laws Here is the definition of the monad typeclass. #+begin_src haskell :tangle del_4.hs class Applicative m => Monad (m :: * -> *) where (>>=) :: m a -> (a -> m b) -> m b

(<=<) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c f <=< g = join . fmap f . g #+end_src

Where's ~join~!? Historically, monads entered Haskell first with interface ~(>>=), return~; later it was realised that ~return = pure~ and the relationship with applicative was cemented.

‘Bind’ ~(>>=)~ is definable from ~join~ by ~ma >>= f = join (fmap f ma)~, and, for this reason, bind is known as “flat map” or “concat map” in particular instances. For instance, the second definition of ~do~-notation could be expressed: #+begin_src haskell (2M′) do {x ← p; C; r} = p >>= q where q x = do {C; r} #+end_src Conversely, ~join ps = do {p ← ps; p} = ps >>= id~. Likewise, with (2M′), note how ~(<*>)~ can be defined directly in-terms of ~(>>=)~

---c.f., ~mf <*> mx = do {f ← mf; x ← mx; return (f x)}~.

Since ~fmap f p = do {x ← p; return (f x)} = p >>= return . f~, in the past monad did not even have functor as a superclass ---c.f., [[http://hackage.haskell.org/package/base-4.12.0.0/docs/Control-Monad.html#v:liftM][liftM]].

The properties of ~>>=, return~ that prove the desired ~do~-notation laws are: #+begin_src haskell [LeftIdentity ] return a >>= f ≡ f a [RightIdentity] m >>= return ≡ m [Associtivity ] (m >>= f) >>= g ≡ m >>= (\x -> f x >>= g) i.e., (m >>= (\x -> f x)) >>= g = m >>= (\x -> f x >>= g) #+end_src

Equivalently, show the ‘fish’ ~(<=<)~ is associative with identity being ~pure~ ---c.f., monoids!

It is pretty awesome that ~(>>=), return~ give us a functor, an applicative, and (dependent) do-notation! Why? Because bind does both the work of ~fmap~ and ~join~. Thus, ~pure, fmap, join~ suffice to characterise a monad.

| /Join determines how a monad behaves!/ |

The monad laws can be expressed in terms of ~join~ [[https://en.wikibooks.org/wiki/Haskell/Category_theory#The_monad_laws_and_their_importance][directly]]: #+begin_src haskell [Associativity] join . fmap join = join . join {- The only two ways to get from “m (m (m α))” to “m α” are the same. -}

[Identity Laws] join. fmap pure = join . pure = id {- Wrapping up “m α” gives an “m (m α)” which flattens to the original element. -} #+end_src

Then, notice that the (free) naturality of join is: #+begin_src haskell join . fmap (fmap f) = fmap f . join ∷ m (m α) → m β #+end_src

Again, note that ~join~ doesn't merely flatten a monad value, but rather performs the necessary logic that determines /how the monad behaves/.

E.g., suppose ~m α = ε → (ε, α)~ is the type of ~α~-values that can be configured according to a fixed environment type ~ε~, along with the possibly updated configuration ---i.e., functions ~ε → (ε, α)~. Then any ~a ∶ ε → (ε, ε → (ε, α))~ in ~m (m α)~ can be considered an element of ~m α~ if we /propagate the environment configuration/ through the outer layer to obtain a new configuration for the inner layer: ~λ e → let (e′, a′) = a e in a′ e′~. The join dictates how a configuration is /modified then passed along/: We have two actions, ~a~ and ~a′~, and join has /sequenced/ them by pushing the environment through the first thereby modifying it then pushing it through the second.

• Monad Examples

Let ~f₁, f₂~ be functors and let ~ε~ a type.

| Applicative | ~m α~ | ~join :: m (m α) → m α~ | |-------------------------------------------------------------------------------------------------------------+----------------+---------------------------------------------------------------------| | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Functor-Identity.html#t:Identity][Identity]] | ~α~ | ~λ x → x~ | | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Control-Applicative.html#t:Const][Constant]] | ~ε~ | ~λ x → x~ ---Shucks! | | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/GHC-List.html][List]] | ~[α]~ | ~λ xss → foldr (++) [] xss~ | | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Either.html#t:Either][Either]] | ~Either ε α~ | Exercise ^_^ | |-------------------------------------------------------------------------------------------------------------+----------------+---------------------------------------------------------------------| | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Functor-Compose.html#t:Compose][Composition]] | ~f₁ (f₂ α)~ | [[https://stackoverflow.com/q/7040844/3550444][Nope! Not a monad!]] | | [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Functor-Product.html#t:Product][Product]] | ~(f₁ α, f₂ α)~ | ~λ p → (fst <$> p, snd <$> p)~ | |-------------------------------------------------------------------------------------------------------------+----------------+---------------------------------------------------------------------| | [[http://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Writer-Lazy.html#g:2][Writer]] | ~(ε, α)~ | ~λ (e, (e′, a)) → (e <> e′, a)~ | | [[https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Reader.html][Reader]] | ~ε → α~ | ~λ ra → λ e → ra e e~ | | [[https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-State-Lazy.html#g:2][State]] | ~ε → (ε, α)~ | ~λ ra → λ e → let (e′, a) = ra e in a e′~ |

In writer, we need ~ε~ to be a monoid.

• Notice how, in writer, join merges the outer context with the inner context: /Sequential writes are mappended together!/
• If ~pure~ forms ‘singleton containers’ then ~join~ flattens containers of containers into a single container.

Excluding the trivial monoid, the constant functor is /not/ a monad: It fails the monad identity laws for join. Similarly, ~f α = Maybe (α, α)~ is an applicative but /not/ a monad ---since there is no lawful definition of ~join~. Hence, applicatives are strictly more generally than monads.

• Running Example ---A Simple Arithmetic Language

Let's start with a weak language: #+begin_src haskell :tangle simple_terms.hs data Term = Int Int | Div Term Term deriving Show

thirteen = Int 1729 Div (Int 133 Div Int 1) boom = Int 1729 Div (Int 12 Div Int 0)

eval₀ :: Term -> Int eval₀ (Int n) = n eval₀ (n Div d) = let top = eval₀ n bottom = eval₀ d in top div bottom #+end_src

How do we accomodate safe division by zero? Print to the user what's happening at each step of the calcuation? Have terms that access ‘global’ variables? Have terms that can store named expressions then access them later?

We'll make such languages and their ~eval~'s will be nearly just as simple as this one (!) but accomodate these other issues.

• [[http://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Maybe.html][Maybe]] ---Possibly Failing Computations Safe evaluator: No division errors. #+begin_src haskell :tangle simple_terms.hs eval₁ :: Term -> Maybe Int eval₁ (Int n) = pure n eval₁ (n Div d) = do t <- eval₁ n b <- eval₁ d if b == 0 then Nothing else pure (t div b) #+end_src Exercise: Rewrite ~evalᵢ~ without ~do~-notation and you'll end-up with nested case analysis leading into a straicase of code that runs right off the page.

• Applicative is enough for ~eval₁, eval₂, eval₃~, but ~eval₄~ needs ~Monad~.

• [[https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Writer-Lazy.html#g:2][Writer]] ---Logging Information as we Compute

Use a pair type ~W ε α~ to keep track of an environment ~ε~ and a value ~α~. #+begin_src haskell :tangle simple_terms.hs data Writer ε α = W ε α deriving Show

write :: ε -> Writer ε () write e = W e ()

instance Functor (Writer ε) where fmap f (W e a) = W e (f a) #+end_src Aggregate, merge, environments using their monoidal operation. #+begin_src haskell :tangle simple_terms.hs instance Monoid ε => Applicative (Writer ε) where pure a = W mempty a (W e f) <*> (W d a) = W (e <> d) (f a)

instance Monoid ε => Monad (Writer ε) where (>>=) = \ ma f -> join (pure f <*> ma) where join (W e (W d a)) = W (e <> d) a #+end_src

An evaluator that prints to the user what's going on. #+begin_src haskell :tangle simple_terms.hs eval₂ :: Term -> Writer String Int eval₂ it@(Int n) = W ("\n Evaluating: " ++ show it) n eval₂ it@(n Div d) = do write $ "\n Evaluating: " ++ show it t <- eval₂ n b <- eval₂ d pure $ (t div b)

-- Try this! With “boom”, we get to see up to the boint of the error ^_^ -- let W e x = eval₂ thirteen in putStrLn e #+end_src

#+latex: \vspace{-1em}

• [[https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Reader.html#g:2][Reader]] ---Accessing ‘Global, read-only, data’ #+latex: \hspace{-1.5em} Use a function type ~ε → α~ to get ~α~-values that ‘reads’ from a configuration environment ε. #+begin_src haskell :tangle terms_with_vars.hs data Reader ε α = R {run :: ε -> α}

instance Functor (Reader ε) where fmap f (R g) = R $ f . g

instance Applicative (Reader ε) where pure a = R $ const a (R f) <*> (R g) = R $ \e -> f e (g e) {- “S” combinator -}

instance Monad (Reader ε) where ma >>= f = join (pure f <*> ma) where join (R rf) = R $ \e -> run (rf e) e #+end_src

A language with access to global variables; uninitialised variables are 0 by default. #+begin_src haskell :tangle terms_with_vars.hs data Term = Int Int | Div Term Term | Var String deriving Show

type GlobalVars = [(String, Int)]

valuefrom :: String -> GlobalVars -> Int valuefrom x gvs = maybe 0 id $ lookup x gvs

eval₃ :: Term -> Reader GlobalVars Int eval₃ (Int x) = pure x eval₃ (Var x) = R $ \e -> x valuefrom e eval₃ (n Div d) = do t <- eval₃ n b <- eval₃ d pure (t div b)

state = [("x", 1729), ("y", 133)] :: GlobalVars thirteen = Var "x" Div (Var "y" Div Int 1) -- run (eval₃ thirteen) state #+end_src

• [[https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-State-Lazy.html#g:2][State]] ---Read and write to local storage

Let's combine writer and reader to get state: We can both read and write to data by using functions ~ε → (ε, α)~ that read from an environment ε and result in a new environment as well as a value.

• ~IO α ≅ State TheRealWorld α~ ;-) #+begin_src haskell :tangle terms_with_storage.hs data State ε α = S {run :: ε -> (ε, α)}

push :: Monoid ε => ε -> State ε () push d = S $ \e -> (d <> e, ())

instance Functor (State ε) where fmap f (S g) = S $ \ e -> let (e', a) = g e in (e', f a)

instance Applicative (State ε) where pure a = S $ \e -> (e, a) (S sf) <*> (S g) = S $ \e -> let (e', a) = g e (e'', f) = sf e' in (e'', f a)

instance Monad (State ε) where ma >>= f = join (pure f <*> ma) where join (S sf) = S $ \e -> let (e', S f) = sf e in f e' #+end_src

A simple language with storage; a program's value is the value of its final store. #+begin_src haskell :tangle terms_with_storage.hs data Expr = Let String Expr Expr | Var String | Int Int | Div Expr Expr deriving Show

eval₄ :: Expr -> State GlobalVars Int eval₄ (Var x) = S $ \e -> let r = x valuefrom e in ((x,r):e, r) eval₄ (Int x) = pure x eval₄ (Let x t body) = do n <- eval₄ t push [(x, n)] -- Applicative is NOT enough here! eval₄ body eval₄ (n Div d) = do t <- eval₄ n; b <- eval₄ d; pure (t div b)

thirteen = Let "x" (Int 1729) $ Let "y" (Int 133 Div Int 1) $ Var "x" Div Var "y"

-- run (eval₄ thirteen) [] #+end_src

Exercise: Add to the oringal =Term= type a constructor =Rndm [Term]=, where =Rndm [t₁, …, tₙ]= denotes non-deterministicly choosing one of the terms ~tᵢ~. Then write an evaluator that considers all possible branches of a computation: ~eval₅ : Term → [Int]~.

If we want to mixin any of the features for our evaluators, we need to use ‘monad transformers’ since monads do not compose in general.

#+latex: \columnbreak

• Reads

• /Introduction to Functional Programming/ by Richard Bird

  • Assuming no programming, this book end by showing how to write a theorem prover powerful enough to prove many of laws scattered throughout the book.

• [[http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf][Monads for functional programming]] by Philip Wadler

  • This covers the ~evalᵢ~ and more ^_^

• [[https://docs.racket-lang.org/heresy/monad-do.html][Comprehending Monads]] by Philip Wadler

• [[http://dev.stephendiehl.com/hask/][What I Wish I Knew When Learning Haskell]]

• [[https://wiki.haskell.org/Typeclassopedia][Typeclassopedia]] ---/The essentials of each type class are introduced, with examples, commentary, and extensive references for further reading./

• [[http://blog.sigfpe.com/2006/08/you-could-have-invented-monads-and.html][You Could Have Invented Monads! (And Maybe You Already Have.)]]

• [[http://learnyouahaskell.com/chapters][Learn You a Haskell for Great Good]] ---An accessible read with many examples, and drawings

• [[https://en.wikibooks.org/wiki/Haskell][The Haskell WikiBook]] ---Has four beginner's tracks and four advanced tracks

• [[https://alhassy.github.io/CatsCheatSheet/CheatSheet.pdf][Category Theory Cheat Sheet]] ---The “theory of typed composition”: Products, Sums, Functors, Natural Transformations ^_^

• [[https://alhassy.github.io/AgdaCheatSheet/CheatSheet.pdf][Agda Cheat Sheet]] ---Agda is Haskell on steroids in that it you can invoke Haskell code and write proofs for it.

• LINQ for [[http://tomasp.net/blog/idioms-in-linq.aspx/#csidiomsl][applicatives]] and [[https://livebook.manning.com/book/real-world-functional-programming/chapter-12/28][monads]].

  • Monads ≈ SQL/Linq ≈ Comprehensions/Generators

#+latex: \ifnum\cheatsheetcols=1 \newpage \else \columnbreak \fi