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:
(these are from Category Theory refound in Type Theory).
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 ? “
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.
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.
Two Key Takeaway Points:
Key Points :
Static Type (Compile-Time Check ) vs Dynamic Type (Run-Time Check)
Weak Type vs Strong Type
La Theorie des Types