Programming with Math (Exploring Type Theory)

If you are inventing a new language, start to study Type Theory.

These 3 are the same thing:

Logic = Category = Type

Unfortunately Milewski’s presentation was cut short due to time constraint, he only presented the first few “Type” functions:

  • Unit,
  • Product,
  • Sum,
  • Exponential,…

(these are from Category Theory refound in Type Theory).

Quora: What is an ALGEBRA structure

What is an algebra? by Tikhon Jelvis

“Basically, an algebra is just an algebraic structure. It’s some set A along with some number of functions closed over the set. It’s a generalization over the structures we normally study: a group is an algebra, a ring is an algebra, a lattice is an algebra… etc.

Algebras have different “signatures” which specify the functions it has. For example, a group is an algebra that has an identity element, a function of one argument and a function of two arguments.

That is, a group with a carrier set A is just a tuple:
⟨A, 0:A, −:A→A, +:A×A→A⟩

For uniformity, we can write all of these as functions in the form An→A, where n is the “arity” of a function—the number of arguments it has. The identity element is a function A0→A, which just identifies a single element from A. Thus, we can talk about the signature of an algebra as the arities of its functions.

A group would be (0, 1, 2) while a ring would be (0, 0, 1, 2, 2).

Generally, the functions of an algebra have to be associative. Sometimes, we also look at other laws—for example, we might want to study algebras with commutative operations like Abelian groups.

So the intuition for an algebra in general is that it’s any structure like a group, a ring or whatever else we like. As the name “structure” implies, these additional operations on a set expose the internal structure of its elements: a group describes symmetries, a lattice describes a partial order and so on.

The study of algebras, then, can be thought of as the study of “structured sets” in general.”