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).

Why Type Theory matters

Note: Proposition (命题, 主张) means Claim / Fact

Proposition as Types vs (Classical) Propositional Logic vs Predicate Logic

With “Proposition as Types“, we can prove theorems using computers.

\boxed {\frac {\text {Proofs} }{\text {Propositions}} =\frac {\text {Programs}}{\text {Types}} }

… Propositions written in “Type” forms (right column).

Prove Tautology :

Prove: “To be” or “Not To be” (Shakespeare’s 《Hamlet》)

Naive Type Theory

Thorsten Altenkirch -| Lambda Days 2019

“Why Type Theory Matters ? “

Type Theory (类型论) Foundations

Robert Harper 2013

Lecture 1:

Holy Trinity: A Scientific Discovery is TRUE if fulfills:

  1. Proof Theory Logic
  2. Algebraic Category Theory
  3. Program Type Theory

A Program is an ABSTRACT Mathematical Object (“M”) :

“A is true” written as “M A”,

ie M is of Type A.

Note: Program M is not about “Coding”.

Above diagram:

[Left] : Proof Theory Logic

[Right] : Category Theory

Lecture 2:

Lecture 2.1

(Video 15:30 mins)

Type Theory is the theory of construction of programming language:

Higher Order Function <=> Exponential Type

Struct, Tuple <=> Cartesian Product Type

Choices of classes of data <=> ‘Some’ Type

Logic is an application of Type Theory

Logic is a part of Math which is a part of Computer Science in which Type Theory is the ‘Theory of Construction’ of Programming Languages.

Lecture 2.2:

Lecture 3:

A Functional Programmer’s Guide to Homotopy Type Theory (HoTT)

Since April 2019 until I re-visit this Youtube video on 12 August 2019, I can now totally understand his speech after a pause of 4 months by viewing other related Youtube (below prerequisite) videos on Category Theory, Type Theory, Homotopy Type Theory.

That is the technique of self-study:

  1. First go through the whole video,
  2. Don’t understand? view other related simpler videos.
  3. Repeat 1.

Prerequisite knowledge:

  1. Homotopy
  2. Type Theory
  3. Homotopy Type Theory
  4. Bijection = Isomorphism
  5. Functional Programming in Category Theory Concept: Monad & Applicative

Two Key Takeaway Points:

  1. In the Homotopy “Space” : Programs are points in the space, Paths are Types.
  2. “Univalence Axiom” : Paths Induce Bijection, vice versa.