Contents Previous Next


module Lang.intro where

A Personal Journey

This work primarily stems from a personal journey of peering deeper into pure mathematics. The journey started as a curiosity into the functional programming paradigm, initially involving learning scala and basic PL theory such as generics, parametric polymorphism and the likes. Being a data engineer at that time, twitter’s work on designing metrics as monoids culminating in Algebird was something that 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 in this space to explore.

In tandem, 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 that I turned toward some PL-theory:

Followed by some “time off” into other areas of math:

The “time off” ended upon discovering this new “foundations of mathematics” thing seen of twitter, materialized into 2 copies ordered from different sources, one of them never got delivered:

As things started getting more cutting-edge, it has mostly been a paper and articles reading affair since then. Major ones being:

Of late, I stumbled upon this work on mathematical physics:

opening the path to these shiny new thingys that await:

It has been almost 4 years now, and the “whole thing” does not seem to have an end!

Who is this for

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

Agda’s Logo

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.


Setup