Category Theory Dump

I’m really enjoying Bartosz Milewski’s lectures on category theory.

Categories

  • Categories consist of objects and morphisms (the relationships between them)
  • Objects are understood and reasoned about in terms of their morphisms, and not in terms of any internal constitution
  • Must feature composition and identity

Monoids

  • Monoids are categories with only one object in them
  • The monoid in set theory is a set of elements which has a binary operator, i.e. an operator, defined in terms of all elements of the set, which takes two elements and returns a third
  • The set also has a unit element, which, when operated on/with, produces no change (e.g. 1 in 5 x 1)
  • Also, associativity
  • Examples of monoid types: numbers with multiplication (unit: 1, associative, binary operator); numbers with addition (unit: 0); strings with concatenation (unit: empty string); lists with concatenation (unit: empty list)
  • The monoid category (“M”) has only one homset (M(m, m)), i.e. reflexive relationships with itself
  • Any two morphisms beget a third via composition, so the binary operation is obtained for free (third element is obtained from two elements of the homset)
  • One element in the homset is an id morphism, so unity is also obtained (the id morphism, when composed with any other, returns the same morphism without change)
  • The monoid categories correspond to weakly typed systems (all functions are composable)
  • The category of sets or types corresponds to a strongly typed system (only functions with inputs and outputs of the same type are composable)
  • But in a sense, ‘weak typing’ is ‘inside’ ‘strong typing’, in that you can pick a trivial category which has only one object, one type, wherein any function can be composed with any other
Advertisements

Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

w

Connecting to %s