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:
Robert Harper 2013
Holy Trinity: A Scientific Discovery is TRUE if fulfills:
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”.
[Left] : Proof Theory Logic
[Right] : Category Theory
(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.
Different views of objects 对象 by：
1. Category 范畴 (morphism* between Objects, Functors ‘F‘ between Cats);
2. Set 集合 (a “smaller Cat”, only objects);
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