# Tag Archives: Type Theory

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

… 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:**

**Proof Theory Logic****Algebraic Category Theory****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:

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

**Prerequisite** knowledge:

- Homotopy
- Type Theory
- Homotopy Type Theory
- Bijection = Isomorphism
- Functional Programming in Category Theory Concept: Monad & Applicative

**Two Key Takeaway Points:**

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

…

…

…

# Beginner Notes on Type Theory

**Key Points** :

- Types in programming language prevent run-time errors
- Use Java Types as examples
- 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**