Russian School of Math


Propositions as “Types” by Philip Wadler 2015

Programming languages which are discovered (man-made) are Functional Programming (Lisp, Haskell, Scala, ML,… ) using “Propositional Logic” (Typed Lambda Calculus).

Note: Java, C++, Python are invented, not discovered!

Ref: Curry Howard Lambek Isomorphism: they are all the same thing with different ‘faces’ :

“Logic = Algebra = Lambda-Calculus = Category = Type”

Notes: Layman’s terms equivalent:

  1. Isomorphism = Same = Congruence
  2. Homomorphism = Similar
  3. Proposition = Claim / Fact

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:

Different Views of Category, Type & Set

Different views of objects 对象 by:

1. Category 范畴 (morphism* between Objects, Functors ‘F‘ between Cats);

2. Set 集合 (a “smaller Cat”, only objects);

3. Type 类型 (deal only with same kind of objects: Int, String, Boulean…).

Note : Category can be a Set (SET) , Group, Ring, Vector Space (Vect) , “Topo” (Topology) … any algebraic structure with Associative Morphism (Map or ‘Arrow’ ) between them.

Note (*) : A morphism 态 in layman’s term is best illustrated by geometry:

2 triangle objects are similar 相似 = homomorphism 同态

2 triangle objects are congruent = isomorphism 同构

Note: Analogy –
Category : School
Type : Boy Class, Girl Class
Set : Students mixed of Boys, Girls