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

# Beginner Notes on Type Theory

Key Points :

1. Types in programming language prevent run-time errors
2. Use Java Types as examples
3. Prove them using Math : Symbolic / Predicate Logic.

Static Type (Compile-Time Check ) vs Dynamic Type (Run-Time Check)

Weak Type vs Strong Type

La Theorie des Types