module Lang.intro whereThe following work aims to be a primer and motivator for functional programmers to peer into the world of pure mathematics. This work is created by a functional programmer who, while discovering and using libraries and constructs like cats, scalaz, lens, monads and various other functional constructs built into languages such as haskell, scala, clojure, rust, purescript and so on, ended up with interest about the math behind them.
This work primarily stems from a personal journey of peering deeper into pure mathematics. The journey started in about 2014 partly as hatred toward the verbosity of java and as a curiosity into the functional programming paradigm made possible on the JVM through scala. Learning scala was soon followed by several PL treats such as generics, parametric polymorphism and the likes making my life easier. Being a data engineer at that time, twitter’s work on designing metrics as monoids and the Algebird project had a lasting impression on my own work. This led me to explore libraries implementing bits of category theory such as shapeless, cats, Algebird’s hyperloglog monoid, scalaz followed by several “for programmer” tutorials into category theory, notably the ones by Bartosz Milewski. Soon I had to learn haskell − it being more “pure” and having a stronger ecosystem of libraries with a more formal programming-language-theory flavor so as to have more things accessible to explore.
In tandem, I started a parallel hobby-type thing where I picked up a few books on the subjects of abstract algebra and category theory to get a theoretical understanding of the “whole thing”:
After trudging through some parts of the above books and getting a “feel” and practice of the mathematics in them, specifically category theory in various contexts, I turned toward some PL-theory:
By 2018, I decided to converge some aspects of my programming job with the act of taking math notes. After I came to know of Agda’s capability to compile code in markdown docs (being a huge proponent of markdown for documentation), I decided to learn agda and concurrently document and code my exploration path into a series of notes, which ended up being this work.
One fine day, I saw this new “foundations of mathematics” thing, which apparently “cool kids” were reading on twitter. On further searching followed by reading online, I ended up ordering 2 copies from different sources, one of them never got delivered:
It took me a few months to read and grasp what was going on in that book. After spending considerable amounts of time through various other notes, mathoverflow, nlab, arxiv, I ended up with the feeling that I knew nothing about geometry and in no way could grasp homotopy theory. I took some time off in 2019 as these notes grew in volume and it became increasingly difficult to code them. During that time off I decided to cover some ground in geometry:
After going through these I finally was able to have at least a sketchy view of homotopy type theory, higher category theory and higher topos theory. As things started getting more cutting-edge, I’ve mostly ended up printing and reading through various parts of:
Of late, I stumbled upon this work on mathematical physics:
opening the path to these shiny new thingys that await:
Meanwhile I try to play catchup with this work and sometimes re-do some parts as my understanding gets clearer and sometimes implement new stuff as and when I have time (and patience). The direction I’ve been following here is if I could implement real numbers, followed by manifolds and such, I perhaps could attempt to implement gauge theories or Supermanifolds albeit it would take me a few years at least. I also need to finish a lot of TODOs. 😛
It has been almost 4 years now, and the “whole thing” does not seem to have an end!
This work is intended to be a resource for anyone (like me) making a foray into pure mathematics. The “like me” here implies someone who:
Agda is a dependently-typed functional programming language that can be used as a “proof assistant” of the
“propositions-as-types” flavor, i.e. it is a language used to write mathematical proofs, using a typesystem, which its
compiler then verifies to check if the proofs really do what they claim. This is done by using Type theory as the
language for writing proofs in Agda. Traditionally, the act of checking the validity of a proof has been a manual and
painstaking process, however, the proofs when represented in this code ⇆ compiler paradigm, does away with
the need for manual checking, thus making things considerably easier to implement, test and distribute. There are other
alternative theorem provers, each with their own feature-sets, strengths and weaknesses, documented here.
Agda was originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The current version is a full rewrite, and should be considered a new language that shares a name and tradition.