Native Type Theory

Category theory is likely to contribute by giving specialists a language they can use to communicate, and it seems likely to me that at some point general tools rooted in category theory will have some sort of interesting implication for testing and debugging. Taking Haskell for example; the language isn't anything to write home about but the type checking in the tooling enabled a big improvement in writing bug free code.

So there is a probably a lot on offer for the sort of people who write tooling, and less on offer for everyone else.

Same. It makes me kind of sad that pure math is not more helpful here! I think its possible that coding standards today are really high quality, and that any improvements are going to require a revolutionary paradigm shift in how we think about programming at an extreme level of generality. That's where pure math comes in, its a good place to shop around for new ideas, since we are kind of at a local maximum now in terms of best practices, imo.

This is how I use math while coding: Instead of tinkering with numbers, just calculate the thing and get all the numbers right the first time. When trying to solve a problem, it's super helpful to have spent years proving theorems in pure math, it helped me compile programs in my head. When I am suuuuuuper stuck and need to figure out if what I am trying to do has already been done in math somewhere. When constructing an overall plan for a project, using abstract concepts in mathematics to properly anticipate the limits of what various implementations will be in order to pick the best one.

> It is well-known that the simply typed lambda-calculus is modeled by any cartesian closed category (CCC). This correspondence suggests giving typed functional programs a variety of interpretations, each corresponding to a different category. A convenient way to realize this idea is as a collection of meaning-preserving transformations added to an existing compiler, such as GHC for Haskell. This paper describes such an implementation and demonstrates its use for a variety of interpretations including hardware circuits, automatic differentiation, incremental computation, and interval analysis. Each such interpretation is a category easily defined in Haskell (outside of the compiler). The general technique appears to provide a compelling alternative to deeply embedded domain-specific languages.

http://conal.net/papers/compiling-to-categories/

As a foundational language it’s there to formalize mathematical objects, but that doesn’t mean people think in either set or category theory, as opposed to higher level objects in their domain.

[0] http://mathieu.anel.free.fr/CLcourse.html

[1] http://mathieu.anel.free.fr/mat/80514-814/Awodey-Bauer-catlo...

Paper [2] has brought renewed attention to set-theory as a basis for automating mathematics.

[1] https://cs.nyu.edu/pipermail/fom/2018-June/021032.html

[2] https://arxiv.org/abs/1707.04757

The usual formal interpretation of what Set Theory is Zermelo Fraenkel set theory, which is roughly first order logic with some axiom schema about how sets behave https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t.... I would be somewhat skeptical that this notion of set theory is all that practically useful to use, although people have managed (metamath). In my opinion, first order logic is great in simplicity a degree of automatability, but clunky and awkward in terms of expressivity. Usually the awkwardness of expressing yourself outpaces the automation, and at that point there may be such a mess that it would be terrible to do it manually Type theory and dependent types are different formalizations of intuitive set theory. In a sense, types are kind of sets. From a pure english perspective, the words are close to synonyms and in practice the analogy is pretty close. 3 being of type Int is intuitively like saying 3 is in the set of ints.

Type theory seems to me to lead to a cleaner system of syntactic formal reasoning, which sounds esoteric except that syntactic reasoning is what computers have to do since we can't convince them with English paragraphs. And perhaps we don't want to, since English is ambiguous.

I think the success Lamport alludes to is even though he bases the TLA+ system on ZFC in some sense, users stick to the fragment of very intuitive notions of set where perhaps your foundations don't matter so much and all should basically agree. This may be more of a pedagogical emphasis than a true difference in systems, since almost everyone interested in dependent types finds the parts that go off into the stratosphere the most interesting.

My understanding is that nothing new was constructed here. Maybe the well-known theory of dependent types has been reconstructed in a new way based on categories; this may be exciting to fans of category theory, but I don't see how it advances programming languages in any way. The actual paper isn't any more helpful either: It name-drops JavaScript in the introduction and at the very end, but doesn't really do anything with it, it certainly doesn't show any kind of model of a type system for even a trivial JavaScript subset.

(Groups might have been a better example than monoids, given that groups are more familiar to mathematicians and the point is to emphasise that this is normal everyday mathematics).

A monoid is (S,•,e): a set S equipped with a binary operation • : (S,S) -> S such that for all x, y, z in S, x•(y•z)=(x•y)•z, and an element e in S such that for all x in S, x•e=e•x=x. Examples of monoids include (String,concat,""), (int,0,+) and so on.

One recurring theme in universal algebra and category theory is the notion of an algebra[0], in programmer terms it's like a module declaration. (see also F-algebra[1] which is heavily used in functional programming to formalize the notion of folding and more)

Dependent type theory allows one to encode these algebras, e.g. encoding monoids and their laws in Coq's type system CoC[2]. Just like how ADTs in Haskell/OCaml and enums in Rust are comprised of a "sum of products", products and sums can be generalized in dependent types as well:

Length-indexed lists via the dependent sum: Σn:ℕ.List(n) consists of dependent pairs ⟨n,l:List(n)⟩. Σn:ℕ.List(n) can be read as a function that takes a natural number n and returns a type List(n)

Type-parametrized types: ΠS:Set.List(S) consists of dependent functions λS:Set.φ(S), ΠS:Set.List(S) can be read as a function that takes a type S and returns a type List(S)

So to encode monoids in a dependent type theory using those dependent sums and products, we can just put the operations and laws into some big record, say

  Monoid:= 
    ΣM:Set.
    Σm:M²→M.
    Σe:()→M.
    Π(a,b,c):M³.m(m(a,b),c)=m(a,m(b,c)).
    Πa:M.m(e,a)=a=m(a,e).

[0] https://en.wikipedia.org/wiki/Universal_algebra#Basic_idea

[1] https://en.wikipedia.org/wiki/F-algebra

[2] https://gist.github.com/puffnfresh/11258181#file-monoid-v-L5

In the category Set, the "exponential" of two sets X and Y is exactly the set of functions from X to Y. In other categories with a concept of exponential, you get a similar internalization of collections of the category's morphisms as objects of the category. You also almost always have an exponential law, (Z^Y)^X = Z^(X*Y)). (If you interpret ^ as "if" and * as "and", you get a common law of logic that we often use when refactoring nested if-statements!)

For a functor to "preserve" an exponential operation (or any other operation) is to be able to do the exponentiation either before or after the functor without changing the result. In symbols, F(X^Y) = F(X)^F(Y). (Compare with linear transformations from linear algebra, in which f(a*x + y) = a*f(x) + f(y).)

Limits are a bit more fundamentally categorical, and I still don't have a good intuition for them. If you think of a functor as projecting the shadow of some index category onto your target category, a limit is in some sense a "best pre-approximation" in the target category, such that if you have a function from elsewhere in the target category into the part under your functor, you can equivalently make a pit stop at the limit object before continuing on into the functor's image.

In some sense, it's like an optimal border control point just outside your functor's image -- you can systematically divert traffic through the limit without actually changing the results.

I'm not sure how to intuitively interpret "preserves limits", since I guess you'd need another functor lying around whose limit is preserved under composition with your first functor. Something like F(Lim(G)) = Lim(F . G), perhaps. But now I'm just reading Wikipedia.