All1 Haskell types can be written in terms of 1≅Unit, 0≅Void, +≅Either, ×≅Pair, (−)(−)≅(→), and fixpoint (ie, self-reference, recursion)
Ignoring GADTs, smart constructors, etc
Examples: Bool≅1+1, Maybe(a)≅1+a, String≅1+String≅‘‘ℵ0′′, List(a)≅1+a×List(a) (why?), BinTree(a)≅a×(1+2×BinTree(a)) (omg just like in Kishan’s lecture)
Hask
Can assemble a categoryHask with Ob=Type and Mor(a,b)={Haskell functions f:a→b}
Yes, generally! Go through examples: Maybe(−), List(−), Pair(a,−), a→(−), Predicate(−) (contravariant), Endo(−) (invariant)
Because our action on morphisms itself has to be a Haskell function, and due to restrictions2 on Haskell functions, every arity-1 Haskell extends to at most one functor!
Consider the family of values eg {lengtha:List(a)→Int}a∈Type. This length family in fact forms a natural transformation (cocone) length:List(−)⇒Int. Naturality is
and says that lengthb(List(f)(x))=lengtha(x). Knowing that List(f) maps the elements of the list, this says that length is insensitive to changes in content of the input list. It “observes only structure”.
More examples (what do each of these do? draw out naturality squares and re-interpret naturality with fresh eyes):
hush:Either(e,−)⇒Maybe(−)
count:List(−)⇒Map(−,Int)3
Technically this should have domain Eq(−)×List(−) since the algorithm needs equality on the input type. We’ll be ignoring this
filter:Predicate(−)×List(−)⇒List(−)4
nb. due to variance, have to treat both functors as having domain something like Haskiso. Actually I think we can use just Hask< (from uniformity.z), but I’m not sure
[]:Const(1)(−)⇒List(−). That is, []:List(−)
All5 polymorphic values in Haskell are natural transformations. Very neat. Also, this means we’re “forced to write good code”; specifically, a polymorphic value is not allowed to observe its type variables. (This doesn’t mean we can’t get information about the type variables, we just have to ask for it as a parameter)
For any monad (M,pure,join) can define a natural transformation with components>>=a,b:M(a)×(a→M(b))→M(b)
given by
m>>=a,bf=joinb(M(f)(m))=joinb(M(f)(m))=joinb(M(f)(m))=joinb(M(f)(m))=joinb(M(f)(m)):M(a)→M(M(b)):M(a):M(M(b)):M(b)
Examples:
Here’s what I’m thinking. Go through one example at a time. Give the monad definition and the sample usage. Have someone explain what’s happening in the example. Only then do we discuss the monad abstractly, giving it a meaning.After 1-2 monads offer the concept that a value of typeM(A) is an “action in M producing an A"
Maybe monad (errors)
Given by
Maybe(A)pure(a)join(m:Maybe(Maybe(A)))={Just(a):a∈A}∪{Nothing}=Just(a)=⎩⎨⎧NothingNothingJust(a)m=Nothingm=Just(Nothing)m=Just(Just(a))
And used with
dbFetchgetAddressgetCountrygetCapital:UserId→Maybe(User):User→Maybe(Address):Address→Country:Country→Maybe(City)idmaynotbeindatabaseusermaynothaveanaddressregisterednotallcountrieshave a singlecapital
like eg
userIddbFetch(userId)dbFetch(userId)>>=getAddressdbFetch(userId)>>=getAddress>>=(pure∘getCountry)dbFetch(userId)>>=getAddress>>=(pure∘getCountry)>>=getCapital:UserId:Maybe(User):Maybe(Address):Maybe(Country):Maybe(City)
compare to writing as something like the following, which is effectively how you have to do it in a language like Python
mCapital:Maybe(City)mCapital=⎩⎨⎧Nthg⎝⎛⎩⎨⎧Nthg({NthgJust(c)gtCptl(gtCnty(a))=NthggtCptl(gtCnty(a))=Just(c))gtAdrs(u)=NthggtAdrs(u)=Just(a)⎠⎞dbFetch(userUid)=NthgdbFetch(userUid)=Just(u)
Either monad (errors)
Given by
Either(E,−)(A)pure(a)join(m:Either(Either(A)))={Left(e):e∈E}∪{Right(a):a∈A}=Right(a)=⎩⎨⎧Left(e)Left(e)Right(a)m=Left(e)m=Right(Left(e))m=Right(Right(a))
Powerset monad given by
P(A)pure(a)join(p:PP(A))=P(A)={a}=⋃p=‘‘{e∈a∈p}′′={e∣(∃a∈p)(e∈a)}or
P′(A)pure(a0)join(f:(A→2)→2)=A→2=a↦{10a=a0else=a↦g:A→2∑f(g)⋅g(a)
Multiset monad given by
MS(A)pure(a0)join(f:(A→N)→N)=A→N=a↦{10a=a0else=a↦g:A→N∑f(g)⋅g(a)
Used for instance by
aoc:P(Int)×P(Int)→P(Int)aoc(x,y)=x>>=x↦{∅y>>=y↦pure(x+y)2∤xelse
this function is equivalent to
aoc(x,y)={x+y∣x∈x∧y∈y∧(2∣x)}
Reader monad
Given by
RdR(A)pure(a)join(f:R→(R→A))=R→A=r↦a=r↦f(r)(r)
Writer monad
Given by
Wr(W,⋅,e)(A)pure(a)join(((x,w1),w2):(A×W)×W)=A×W=(a,e)=(x,w1⋅w2)
State monad
Given by
StS(A)pure(a)join(f:S→S×(S→S×A))=S→S×A=s↦(s,a)=s↦(f′(s′)where(s′,f′)=f(s))
Used like e.g.
putSputS(s1)getSgetS:S→StS(Unit)=s0↦(s1,unit):StS(S)=s↦(s,s)f:List(Player)→Int×List(Player)f(p)=⎩⎨⎧pure([])({s↦(s+1,unit)pure(unit)p1∈winnersp1∈/winners)>>=u↦f(p2,…,pk)>>=p′↦pure([p1,p′])p=[]p=[p1,p2,…,pk],k≥1
and says that . Knowing that maps the elements of the list, this says that is insensitive to changes in content of the input list. It “observes only structure”.
Written pointwise, this says:
