- Milewski, Bartosz
- Computation–Logic–Category theory are isomorphic
OOP is bad for concurrent programming because OOP hides data mutation and sharing (pointers). Mixing sharing and mutation is data race.
- this makes objects non-composable
- locks do not compose either
Template metaprogramming in C++ draws many ideas from Haskell. So you translate Haskell ideas into ugly C++ metaprogramming language.
- Haskell draws many ideas from Category Theory. So you translate concise Category Theory ideas into ugly Haskell language.
Category Theory unifies different branches of mathematics: type theory, logic, algebra, etc.
- Mathematics get philosophical: do mathematicians invent things or discover truth?
It might be that composition and this universal structure is not the property of the universe, but the property of human minds.
- It might be that humans evolved to work with abstraction and composition, and we don’t understand what we can’t explore using these tools.
- In that sense, Category Theory might be about human minds really and be closer to epistemology.
- Functors consist of functions and functions compose, so we can compose functors
- Identity functor is trivial
Cat = Category of functors
- Objects are categories
- Morphisms are functors
- It’s a category of small categories. For large categories, we need a more powerful mechanisms
- (Now, Haskell does not really allow composition of functors. If you have a
Maybe [Int](composition of two functors: Maybe and ), you have to use two fmaps instead of one.)
- all algebraic data types are automatically functorial
bifunctor — is a functor from a product category (C×D → E)
- sum type is bifunctor as well
(cartesian) product (operator) + terminal object (Void) (a unit) is a monoidal category
terminal object is a unit of product
- by the same token, coproduct + initial object is a monoidal category
a monoidal category (or tensor category)
a bifunctor: called a tensor product
- (e.g., product or coproduct)
- an object or called the unit object or identity object.
Contravariant functor — is a functor defined on the opposite category (cofunctor? no)
class Contravariant f where contramap :: (a -> b) -> f b -> f a -- must satisfy: -- contramap id = id -- contramap f . contramap g = contramap (g . f)
- (Strictly speaking, “cofunctor” is not the right name as the dual of a functor is a functor)
- you can think of Contravariant as an opposite of container. it does not contain As, but it requires As
(->) a bis Contravariant in
aand Covariant in
- that is called a Profunctor
class Profunctor p where dimap :: (a' -> a) -> (b -> b') -> p a b -> p a' b' instance Profunctor (->) where -- dimap :: (a' -> a) -> (b -> b') -> (a -> b) -> (a' -> b') dimap f g h = g . h . f
- (how does that definition match to the Profunctor definition on wikipedia or nLab? )
hom-set between two objects (if it’s a set), can be represented as an object in the same category
- “internal hom-set”
zis a function,
ais an argument type,
- the category must have products
- (this relies on that a morphism between two products can be constructed as a product of two morphisms ( and here), and we know that that is a correct way to obtain from using )
in haskell, the next two are equivalent
h :: z -> (a -> b) g :: (z, a) -> b
curry :: ((a, b) -> c) -> (a -> (b -> c)) curry f = \a -> \b -> f (a, b) uncurry :: (a -> (b -> c)) -> ((a, b) -> c) uncurry f = \(a, b) -> f a b
cartesian closed category (CCC)
- cartesian — has products
closed — has all exponentials
- A category is closed if for any pair of objects the collection of morphisms from to can be regarded as forming itself an object of .
- has a terminal object (0th power of an object)
Bicartesian closed category (BCCC)
- has products, co-products, exponentials, and initial and terminal objects
- bicartesian = both cartesian and cocartesian