347 lines
18 KiB
Markdown
347 lines
18 KiB
Markdown
---
|
||
title: Haskell
|
||
---
|
||
|
||
# Haskell
|
||
|
||
## Semirings
|
||
|
||
- https://doisinkidney.com/posts/2016-11-17-semirings-lhs.html
|
||
|
||
- https://doisinkidney.com/posts/2017-10-13-convolutions-and-semirings.html
|
||
|
||
- https://r6.ca/blog/20110808T035622Z.html
|
||
|
||
## Monoids
|
||
|
||
- http://blog.sigfpe.com/2009/01/haskell-monoids-and-their-uses.html
|
||
|
||
- https://www.haskellforall.com/2014/07/equational-reasoning-at-scale.html
|
||
|
||
- https://apfelmus.nfshost.com/articles/monoid-fingertree.html
|
||
|
||
- https://gist.github.com/cscalfani/b0a263cf1d33d5d75ca746d81dac95c5
|
||
|
||
## Continuation passing style
|
||
|
||
- https://stackoverflow.com/questions/45334985/when-to-use-cps-vs-codensity-vs-reflection-without-remorse-in-haskell
|
||
|
||
- https://deque.blog/2017/01/13/beautiful-code-control-fold/
|
||
|
||
- https://free.cofree.io/2020/01/02/cps/
|
||
|
||
- https://neilmitchell.blogspot.com/2014/06/optimisation-with-continuations.html
|
||
|
||
- https://jtobin.io/page2/
|
||
|
||
## How to read sequential calculus notation
|
||
|
||
|
||
|
||
- http://logitext.mit.edu/tutorial
|
||
|
||
- https://langdev.stackexchange.com/questions/2692/how-should-i-read-type-system-notation
|
||
|
||
## Folds
|
||
|
||
Alexis King's excellent explanation on folds
|
||
|
||
- https://twitter.com/lexi_lambda/status/1198676516445589509
|
||
|
||
- https://github.com/hasura/graphql-engine/pull/2933#discussion_r328821960
|
||
|
||
|
||
## Principles of Programming Languages
|
||
|
||
- http://kmicinski.com//cis352-s20/
|
||
|
||
- https://www.youtube.com/user/krismicinski/videos
|
||
|
||
# Category Theory
|
||
|
||
## Resources
|
||
|
||
- https://pages.cs.wisc.edu/~jcyphert/categoryTheoryNotes/
|
||
- http://brendanfong.com/programmingcats.html
|
||
- https://www.johndcook.com/blog/2018/08/06/hom-functors/
|
||
- https://www.cs.cornell.edu/courses/cs6117/2022fa/
|
||
|
||
## Chapter 1
|
||
|
||
- A category consists of objects and arrows that go between them.
|
||
- The essence of a category is composition or the essence of composition is a category.
|
||
|
||
### Arrows as functions
|
||
|
||
- Arrows are also called morphisms
|
||
- In a category, if there is an arrow going from **A** to **B** and an arrow going from **B** to **C** then there must also be a direct arrow from **A** to **C** that is their composition. Note that this is not a full category because it's missing identity morphisms.
|
||
- **In Mathematics and in Haskell, functions compose right to left**.
|
||
|
||
### Properties of Composition
|
||
|
||
- Composition is associative.
|
||
- For every object, there is identity morphism.
|
||
|
||
### Notes from video lecture "1.2 What's a category?"
|
||
|
||
Major tools in arsenal
|
||
|
||
- Abstraction
|
||
- Composition
|
||
- Identity
|
||
|
||
*Composition and Identity define category theory*.
|
||
|
||
Category is just a bunch of objects. One analogy is thinking of category as a graph.
|
||
|
||
Composable "end of one is beginning of other". And remember that end or beginnings are objects. Thinking in terms of types, the objects should be types?. If the *end* type does match *beginning* type, we cannot compose right?
|
||
|
||
When we are defining a category, the category is defined by giving objects, what the objects are, defining arrows and then defining composition. Composition is like a big multiplication table for arrows. For every arrow, one has to define their composition.
|
||
|
||
Different composition tables give different category.
|
||
|
||
We also have laws:
|
||
|
||
1. Left Identity
|
||
2. Right Identity
|
||
3. Associativity *h* ∘ (*g*∘*f*) = (*h*∘*g*) ∘ *f*
|
||
|
||
Objects don't form a set in general. If they form a set, then this category is called *small*. Morphisms between any two objects form a set. There is a category theory in which they don't form a set and that
|
||
is a higher order categories.
|
||
|
||
A group is an monoid that also has an inverse. A groupoid is a category in which every arrow has an inverse.
|
||
|
||
Objects are types and arrows are functions. A function is a morphism between two types.
|
||
|
||
Question:
|
||
|
||
1. hom-sets map pairs to sets. And sets are objects in the category set. How does it follow we have a mapping between categories.
|
||
|
||
## Chapter 2
|
||
|
||
### Types are about composability
|
||
|
||
### What are types?
|
||
|
||
- Types are sets of values.
|
||
- In the ideal world, Haskell types are sets and Haskell functions are mathematical functions between sets.
|
||
- Functions that return bottom are called partial, as opposed to total functions, which return valid results for every possible argument.
|
||
- Because of bottom, the category of Haskell types and functions are referred to as **Hask** rather than **Set**.
|
||
|
||
### Why do we need a mathematical model?
|
||
|
||
- Operational semantics describes the mechanics of program execution.
|
||
- In denotational semantics, every programming construct is given it's mathematical interpretation.
|
||
|
||
### Examples of types
|
||
|
||
- What's the type corresponding to an empty set? This type is called **Void** in Haskell.
|
||
- Functions that can be implemented with the same formula for any type are called parametrically polymorphic.
|
||
|
||
### Notes from video lecture "2.1 Functions, Epimorphisms"
|
||
|
||
- Category **Set** which contains sets and functions between sets.
|
||
- The set of all paris forms a Cartesian Product. A subset of the Cartesian Product is a **relation**.
|
||
- If a function does not collapse things, it is *injective*.
|
||
- If the function covers the whole co-domain, then it is *surjective*.
|
||
- Both *injective* and *surjective*, then it is an isomorphism.
|
||
- Think of Epimorphism as a way of considering surjection in Category theory. Since we do not care about elements, but, need to think in terms of morphisms, this is where Epimorphism comes in. Epimorphisms are categorical analogues of surjective functions.
|
||
- Surjective => Epic, Injective => Monic
|
||
|
||
### Notes from video lecture "2.2 Monomorphisms, simple types"
|
||
|
||
Equality of composition leads to Equality of functions.
|
||
|
||
*Void* in logic corresponds to *False*.
|
||
|
||
## Chapter 3
|
||
|
||
### Simple Graphs
|
||
|
||
Creating a category, which has an object for every node in the graph, and all possible chains of composable graph edges as morphisms. One may even consider identity morphisms as special cases of chains of length zero.
|
||
|
||
Such a category is called *free category* generated by a given graph. It's an example of free construction, a process of completing a given structure by extending it with a minimum number of items to satisfy it's laws (here, the laws of a category).
|
||
|
||
### Orders
|
||
|
||
Consider the category where a morphism is a relation between objects: the relation of being less than or equal. We have identity morphisms as every object is less than or equal to itself. If `a <= b` and `b <= c` then `a <= c`. Composition is also associative. A set with a relation like this is called *preorder*, so a preorder is indeed a category.
|
||
|
||
For a stronger relation:
|
||
|
||
- An additional condition that, if `a <= b` and `b <= a`, then *a* miust be the same as *b*. That's called a *partial order*.
|
||
- If any two objects are in relation with one each other, one way or another, that gives a *linear order* or *total order*.
|
||
|
||
A preorder is a category where there is at most one morphism going from any object *a* to any object *b*. Another name for such a category is "thin". A preorder is a thin category.
|
||
|
||
A set of morphisms from object *a* to object *b* in a category **C** is called a *hom-set* and is written as **C**(*a*,*b*) or sometimes **Hom**<sub>*C*</sub>(*a*,*b*). *Hom* stands for homomorphism, the usual name for structure preserving functions in algebra.
|
||
|
||
Sorting algorithms can only work on total orders. Partial orders can be sorted using topological sort.
|
||
|
||
### Monoid as Set
|
||
|
||
A monoid is defined as a set with binary operation. The operation should be associative and should have one special element that behaves likes a unit with respect to it.
|
||
|
||
``` haskell
|
||
class Monoid m where
|
||
mempty :: m
|
||
mappend :: m -> m -> m
|
||
```
|
||
|
||
Interpretation of the type signature of *mappend* as *m* → (*m*→*m*) tells us that *mappend* maps an element of a monoid set to a function acting on that set.
|
||
|
||
There is the adders example and then this follows. What does this mean? As in I haven't digested it!
|
||
|
||
One might ask the question whether every categorical monoid - a one object category - defines a unique set-with-binary-operator monoid. It turns out we can always extract a set from a single-object category. This is set of morphisms - the adders in our example. In other words, we have the *hom-set*, **M**(*m*,*m*) of the single object *m* in the category **M**.
|
||
|
||
The monoidal product of two set-elements is the element corresponding to the composition of the corresponding morphisms. Given two elements of **M**(*m*,*m*) corresponding to *f* and *g*, their product will correspond to the composition of *f* ∘ *g*. The composition always exists, because the source and the target for these morphisms are the same object. And it's associative by the rules of the category. The identity morphism is the neutral element of this product. So we can always recover a set monoid from a category monoid. For all intents and purposes they are one and the same.
|
||
|
||
A category in which morphisms between any two objects form a set is called locally small.
|
||
|
||
### Notes from video lecture "3.1 Examples of categories, orders, monoids"
|
||
|
||
The set of arrows between any two objects is called a *hom-set*.
|
||
|
||
## Chapter 4
|
||
|
||
A Kleisli category has objects, the types of underlying programming language. Morphisms from type **A** to type **B** are functions that go from **A** to a type derived from **B** using the particular embellishment. Each Kleisli category defines its own way of composing such morphisms, as well as the identity morphisms with respect to that composition. We will learn that imprecise term *embellishment* corresponds to the notion of an endofunctor in a category.
|
||
|
||
### Notes from video lecture "3.2 Kleisli Category"
|
||
|
||
Every set is a subset of itself. In terms of order, we call it reflexivity. How would we translate composition into this language of being a subset? If *A* is a subset of *B* and *B* is a subset of *C*, *A* is a subset of *C*. It's a partial order, there are no loops as *A* ⊆ *B* and *B* ⊆ *A* then *A* = *B*.
|
||
|
||
Monad is nothing special. It is just a way of composing functions.
|
||
|
||
## Chapter 5 - Products and Coproducts
|
||
|
||
Common construction in category theory called the *universal construction* for defining objects in terms of their relationships.
|
||
|
||
### Initial Object
|
||
|
||
The *initial object* is the object that has one and only one morphism going to any object in the category. The uniqueness of the initial object is not guaranteed. Only *uniqueness up to isomorphism*.
|
||
|
||
The initial object in a partially ordered set (often called a poset) is its least element. In the category of sets and functions, the initial object is the empty set.
|
||
|
||
### Terminal Object
|
||
|
||
The **terminal object** is the object with one and only one morphism coming to it from any object in the category. The terminal is unique upto isomorphism.
|
||
|
||
In a poset, the terminal object if it exists, is the biggest object. In the category of sets, the terminal object is a singleton. Corresponds to the unit type () in Haskell.
|
||
|
||
### Notes from video lecture "4.1 Terminal and initial objects"
|
||
|
||
Singleton set has an arrow coming from every other set. There is a function from any type to unit ().
|
||
|
||
∀*a*∃*f* : : *a* → ()
|
||
|
||
For all objects (type) *a*, there exists an *f*, that goes from *a* to
|
||
the terminal object ().
|
||
|
||
∀*f* : : *a* → (), *g* : : *a* → () ⟹ *f* ≡ *g*
|
||
|
||
For every two functions, from *a* to the terminal object, if we have *f* and *g*, also from *a* to the terminal object, then *f* ≡ *g*.
|
||
|
||
### Notes from video lecture "4.2 Products"
|
||
|
||
Outgoing arrows from the terminal object? There are outgoing arrows from a terminal object. These arrows help us define the generalised elements in other objects. Every arrow from a terminal object to another object, is a definition of a generalised element in this other object.
|
||
|
||
### Notes from video lecture "5.1 Coproducts, Sum Types"
|
||
|
||
Discriminated Union/Tagged Union/Variant.
|
||
|
||
### Duality
|
||
|
||
The only difference between the above two was the direction of morphisms. For any category **C** we can define the *opposite category* **C**<sup>op</sup> just by reversing all the arrows. The opposite category automatically satisfies all the requirements of a category, as long as we simultaneously redefine composition.
|
||
|
||
The set of arrows between any two objects is called a *hom-set*.
|
||
|
||
If original morphisms *f* :: *a* → *b* and *g* :: *b* → *c* composed to *h* : : *a* → *c* with *h* = *g* ∘ *f*, then the reversed morphisms
|
||
|
||
*f*<sup>op</sup> : : *b* → *a* and
|
||
*g*<sup>op</sup> : : *c* → *b* will compose to
|
||
*h*<sup>op</sup> : : *c* → *a* with
|
||
*h*<sup>op</sup> = *f*<sup>op</sup> ∘ *g*<sup>op</sup>
|
||
|
||
Reversing the identity arrows is a no-op.
|
||
|
||
### Isomorphisms
|
||
|
||
Isomorphic objects look the same - they have the same shape. It means that every part of one object corresponds to some part of another object in a one-to-one mapping.
|
||
|
||
Mathematically it means that there is a mapping from object *a* to object *b*, and there is a mapping from object *b* to object *a*, and they are the inverse of each other.
|
||
|
||
In category theory, we replace mappings with morphisms. An isomorphism is an invertible morphism, or a pair of morphisms, one being the inverse of the other.
|
||
|
||
Morphism *g* is the inverse of morphism *f* if their composition is the identity morphism.
|
||
|
||
``` haskell
|
||
f . g = id
|
||
g . f = id
|
||
```
|
||
|
||
### Products
|
||
|
||
A **product** of two objects *a* and *b* is the object *c* equipped with two projections such that for any other object *c*<sup>′</sup> equipped with two projections there is a unique morphism *m* from *c\`* to *c* that factorizes these projections.
|
||
|
||
A **coproduct** of two objects *a* and *b* is the object *c* equipped with two injections such that for any other object *c\`* equipped with two injections there is a unique morphism *m* from *c* to *c\`* that factorizes those injections.
|
||
|
||
### Asymmetry
|
||
|
||
Product behaves like multiplication, with the terminal object playing the role of one; whereas coproduct behaves more like the sum, with the initial object playing the role of zero. In particular for finite sets, the size of the product is the product of the sizes of the individual sets, and the size of the coproduct is the sum of the sizes.
|
||
|
||
## Chapter 6
|
||
|
||
Set (the category of sets) is a *monoidal category*. It's a category that is also a monoid, in the sense that one can multiply objects (take their Cartesian Product).
|
||
|
||
A product of two types *a* and *b* must contain both a value of type *a* and a value of type *b*, which means both types must be inhabited. A sum of two types on the other hand, contains either a value of type *a* or a value of type *b*, so it's enough if one of them is inhabited. Logical *and* and *or* also form a semiring, and it too can be mapped into type theory.
|
||
|
||
## Chapter 7
|
||
|
||
Functor composition is associative (the mapping of objects is associative, and the mapping of morphisms is associative). There is also a trivial identity functor in every category: it maps every object to itself and every morphism to itself. So functors have all the same properties as morphisms in some category. It would have to be a category in which objects are categories and morphisms are functors. It's a category of categories.
|
||
|
||
### Notes from video lecture "6.1 Functors"
|
||
|
||
If the mapping of *hom-sets* is injective, then we call such functors *faithful*. A faithful functor is injective on all *hom-sets*. If it is *ful*, then it is surjective.
|
||
|
||
## Chapter 8
|
||
|
||
A monoidal category defines a binary operator acting on objects, together with a unit object. **Set** is a monoidal category with respect to Cartesian product, with the singleton set as a unit. It's also a monoidal category with respect to disjoint union. One of the requirements for a monoidal category is that the binary operator should be a bifunctor. This is an important requirement, as the monoidal product should be compatible with the structure of the category, which is defined by morphisms.
|
||
|
||
### Notes from video lecture "7.1 Functoriality, Bifunctors"
|
||
|
||
Functors are mappings between categories. Endofunctors are mapping within a category.
|
||
|
||
"Basically, when you have some expression E that contains F, and we say E is functorial in F, it means that F → E, is a functor."
|
||
|
||
- https://math.stackexchange.com/questions/2009361/what-does-it-mean-to-be-functorial-in-something
|
||
|
||
## Chapter 9
|
||
|
||
### Notes from video lecture "8.1 Function Objects, Exponentials"
|
||
|
||
## Chapter 10
|
||
|
||
A parametrically polymorphic function between two functors (including the edge case `Const` functor) is always a natural transformation. Since all standard algebraic data types are functors, any polymorphic function between such types is a natural transformation.
|
||
|
||
### Notes from video lecture "9.1 Natural Transformations"
|
||
|
||
- Category is about structure.
|
||
- Functors are mappings between categories that preserve structure. They take a category and embed it in another category. It's like searching for a pattern inside a category or modelling a category inside another category.
|
||
- Categories and functors are necessary to define natural transformations.
|
||
|
||
## Chapter 12
|
||
|
||
- https://www.math3ma.com/blog/limits-and-colimits-part-1
|
||
- https://www.math3ma.com/blog/limits-and-colimits-part-2
|
||
- https://www.math3ma.com/blog/limits-and-colimits-part-3
|
||
- https://kavigupta.org/2016/05/10/A-Haskell-Class-For-Limits/
|
||
- http://blog.sigfpe.com/2010/03/products-limits-and-parametric.html
|
||
|
||
One interpretation of limits and co-limits with respect to Haskell is how they play with universal and existential quantification. We can write
|
||
|
||
``` haskell
|
||
{-#Language ExistentialQuantification#-}
|
||
newtype Limit f = Limit (forall a. f a)
|
||
data Colimit f = forall a. Colimit ( f a)
|
||
```
|
||
|
||
So *Limit* universally quantifies over all types a functor *f* can map over, and *CoLimit* let's us talk about an *f* *a* but forget about the exact *a* (existential quantification).
|