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

Parallel & Concurrent Haskell (2)

Continued from : (Part 1)

2.2 Data Structure

Function (+) ::  D -> D -> D
inc  x  = 1 + x ~ (+) ::  1 + x

Section (Partial appl) : inc  = (+ 1)

Type ~ Set {values} : Integer Set / Boolean Set {0,1} / Empty Set “Void” { } / …

Type of Singleton (1 element) : Unit ( )

Declare a new Type : data

data () = ()
1st () = Type of Unit
2nd () = constructor of Unit

Haskell convention : Type name = constructor name

(To avoid having too many nsmes)

Define cares Ian product of Types (Sets):

data Product a b = P a b

Product : Type constructor
P : Data constructor (function with 2 args of types a, b)
P :: a -> b -> Product a b

Data Immutable : remember how it was constructed.

(+) :: Num a => a -> a -> a 

sqDist ‘ ‘ (P x y ) = x^2 + y^2
sqDist ‘ ‘ :: Num a =-> Product a a -> a

Built-in for “pair”:

data ( , ) a b =( , ) a b

eg.
( , ) 1 2 gives (1, 2)

All data (Types) are formed by only 2 methods : Product or Sum.

\boxed {\text {Algebraic Data : by Product, Sum}}

Parallel and Concurrent Haskell: http://www.youtube.com/playlist?list=PLbgaMIhjbmEm_51-HWv9BQUXcmHYtl4sw

<b>Read Free Online Book:</b>
http://chimera.labs.oreilly.com/books/1230000000929/index.html
<a href=”https://tomcircle.files.wordpress.com/2017/07/20170712_200456.png”><img src=”https://tomcircle.files.wordpress.com/2017/07/20170712_200456.png&#8221; alt=”” class=”wp-image-13955 alignnone size-full” width=”1064″ height=”1262″></a>

Category Theory II 9: Lenses

Lens = {get, set}

w = whole tuple, p = a field

get :: w -> p
set :: w -> p -> w

Example: take a pair (tuple)

get1 (x, y) = x

get1 :: (a, b) -> a

set1 (x, y) x’ = (x’,y)

set1 :: (a, b) -> a -> (a,b)

Polymorphic Types: change type of field

set :: w -> p’ -> w’
set1 :: (a, b) -> a’ -> (a’,b)

Lens Laws:

set w (get w) = id 

get (set w p) = p

get (set w p) p’ = set w p’

Combine get & set (co-Algebra):

\boxed {w \to(p, p \to w)}

data Store p w = Store p (p-> w)

fmap g (Store p f ) = Store p (g.f)
g: w-> v
pf : p -> w
g.f : p-> v

Store = functor from w to Store = coalgebra = comonad [W a ->a]

instance Comonad (Store p) where

extract (Store p f) = f p

duplicate  (Store x f) = Store x ( λy -> Store y f)

[Think of p as key, f is the lookup function
f p = retrieve current value]

Comonad & coalgebra – compatible?

(Coalgebra) coalg ::a -> w a
(Comonad) extract :: w a -> a
duplicate :: w a ->w (w a)

coalg w = Store (get w) (set w)

set w (get w) = id [Lens Law]

\boxed {\text {Lens = comonad + coalgebra}}

If Type change (Set = Index Store : a = p, b = p’, t = w)

IStore a b t = IStore a (b ->t)

Object-oriented: eg. school.class.student

<=>”.” = functional programming 



9.2 Lenses 

Type Lense s t a b = forall f . Functor f => (a -> f b) -> s -> f t

s \to \forall f. (a \to f b ) \to f t

s  ->IStore a b t

forall  = polymorphism (?  Natural Transformation)

Yoneda Embedding Lemma

 [C, Set](C (a -> – ), C (b -> – )) ~ C(b, a)

Adjunction: C (Ld,C) ~ D (D,  Rc)


Reference: “Understanding Yoneda”

https://bartoszmilewski.com/2013/05/15/understanding-yoneda/

adjoint functor in nLab

Yoneda lemma in nLab

维基百科: Hom functor
https://www.zhihu.com/question/23324349/answer/54242934

BM Category Theory II 8: F-Algebra, Lambek’s Lemma , Catamorphism, Coalgebra, Anamorphism

[Continued from previous BM Category Theory …]

\boxed { \text {type Algebra f a = f a} \to \text {a} }

Intuition: [Artificial Intelligence] You teach the computer like to a Primary 6 kid, that Algebra is a type of expression (f) which, after evaluation,  returns a value.

If a = i (initial) [or u (terminal)],
\boxed { \text {(f i} \to \text {i )} \implies \text {f = Fix-point} }

Intuition: Fix-point because, the Initial “i”, after evaluating the expression f, returns itself “i”.

Lambek’s Lemma 
\boxed { \text {Initial Algebra is an Isomorphism} }

Note: Endo-functor is a functor (equivalent to function in Set Theory) within the same Category (Endo = Self = 自)

Video 8.1 F-Algebras & Lambek’s Lemma 

Video 8.2 Catamorphism & Anamorphism 

foldr ~ catamorphism (浅层变质) of a Fix-point endo-functor on a List.

Examples: Fibonacci, Sum_List

Remark: Cool Math! the more  advanced concept it is, the more closer to Nature (eg.Geology, Biology) : Catamorphism 浅层(风化)变质, or “thin-layer change in nature” (in Functional Programming languages: foldr or map) eg : add1 to a list (1 5 3 8…) 
= (2 6 4 9 …)

\boxed { \text {type Coalgebra f a = a} \to \text {f a} }

Intuition: Reverse of Algebra, given a value, Coalgebra returns an expression (f).

Anamorphism (合成变质) ~ unfoldr

Example: Prime numbers

Remark: Anamorphism (合成变质) or “synthesised change in nature“: eg. Start from a  “seed” prime number “2” generates  all other infinite prime numbers (3 5 7 9 11 13 17 …)

Note: In Haskell, no difference between Initial and Terminal Fix-points. However, since Fix-point is not unique, in Category Theory there is the Least Fix-point (Initial) and Greatest Fix-point (Terminal).

Ref: 

Reading “Understanding F-Algebra ” by BM: https://bartoszmilewski.com/2013/06/10/understanding-f-algebras/

Catamorphism (下态) : https://www.zhihu.com/question/52180621/answer/129582557

Anamorphism : https://zhuanlan.zhihu.com/cofree/21354189

F-Algebra & F-coalgebra: http://stackoverflow.com/a/16022059/5822795

BM 5&6 : Category Adjunctions 伴随函子

Adjunction is the “weakening of Equality” in Category Theory.

Equivalence of 2 Categories if:

5.2  Adjunction definition: (L, R, \epsilon, \eta ) such that the 2 triangle identities below ( red and blue) exist.

6.1 Prove: Let C any category, D a Set.

\boxed {\text {C(L 1, -)} \simeq \text {R}}

{\text {Right Adjoint R in Set category is }} {\text {ALWAYS Representable}}

1 = Singleton in Set D

From an element in the singleton Set always ‘picks’ (via the function) an image element from the other Set, hence :
\boxed {\text{Set (1, R c) } \simeq \text{Rc }}

Examples : Product & Exponential are Right Adjoints 

Note: Adjoint is a more powerful concept to understand than the universal construction of Product and Exponential.

6.2

\boxed  {\text {Every Adjunction gives a Monad}}

vice-versa.

\boxed {\text {Left Adjoint: L } \dashv \text { R }}

R \circ \ L = m = \text { Monad}

L \circ \ C = \text { Co-Monad}

With Product (Left Adjoint) and Exponential (Right Adjoint) => \text {State Monad}

Category Theory II 2: Limits, Higher order functors

1.2 Introduction to Limit 

Analogy : Product to Cones (Limit)

2.1 Five categories used to define Limit:

  1. Index category (I)
  2. Category C: Functors (constant ,  D)
  3. Cones (Lim D)
  4. Functor Category [I, C ]:objects are (constant, D ), morphisms are natural transormations
  5. Set category of Hom-Set Cones [I,C] to Hom-Set C (c , Lim D )

2.2 Naturality

3.1 Examples: Equalizer

CoLimit = duality of Limit (inverted cone = co-Cone)

Functor Continuity = preserve Limit

BM Category Theory 8 : Function objects (Exponentials), Curry / unCurry

8.1 

[Revision] Product (or Sum = co-Product) is a Bifunctor

  • takes 2 objects to produce 3rd object;
  • takes 2 morphisms to produce 3rd morphism. 

Functions are “morphisms between Category objects”  = a Hom-Set, which itself is an object : ‘a -> b’.

Using the same method of Universal Construction of Product objects in category :  

  1. Define a Pattern ,
  2. Ranking which object is better, 
  3. Pick the best object up to an UNIQUE Isomorphism.

we can similarly construct the Function Objects ‘a => b‘ (in Haskell as ‘a -> b’) :

Intuitively, the above diagram is interpreted as: 

  • evalthe Function object(a=>b) x ato return result b
  • g is up to Unique isomorphism (hSAME as ‘eval: \boxed {g = eval \circ (h \text { x } id )}

Curry / Non-curry : Associative (yellow brackets below are optional).

\boxed {z \to (a \to b ) \iff z \to a \to b }

\boxed { (f a ) \: b \iff f a \: b }

Note: function (f a) returns as a new  function which applies on argument b. Equivalently, also read as “f takes 2 arguments a, b”.

Example: 

f :: Bool -> Int

Bool = {0, 1}
{ f = (Int \text { x }  Int) = Int^{2} = Int ^ {Bool}}

The number of possibilities of applying f from a to b is \boxed {b^{a}} , hence we call:  
\boxed {\text {Function object f as EXPONENTIAL}}

8.2  Algebraic Data Types

BM Category Theory 6: Functors & Examples

6.1 

Discrete Category:  no other Morphism except the Identity Morphism. 

Functor between 2 categories : preserve structures.

6.2 Examples of functors

In-lining & Refactoring (in Pure Function)

1. In-lining: function f = function g
Replace everywhere in the program each f by g.

2. Re-factoring: In the program: {expressions}
We can define a function h = {expresions}, then use h throughout.

class Functor f where
\boxed {fmap : : (a \to b) \to (f a \to f b)}

Examples of Functors:

1. List

2. Reader

Functor (esp. Endo-functor) can be viewed as a Container where you can opetate on its content. Eg. Functor List [1 ..] = container of 1 2 3 … infinity, operared on it by generating (lazily) the next number.

Illustrations of Functors and Monad (Endo-functors): a “wrapped container”.

http://adit.io/posts/2013-04-17-functors,_applicatives,_and_monads_in_pictures.html#functors

BM Category Theory 5: Coproducts = Sum types

5.1 Coproducts = Sum types

Product c is the “Best” than any others like c’, with projections p, q into a and b respectively (Haskell “fst“, “snd“) — because all c’ = c (up to a unique isomorphism m).

Coproduct is like “yin-yang” (阴阳合一) sum of 2 objects {a, b} into c – injection “discriminately” (in Haskell by “Left” and “Right”)

5.2 Algebraic Data Types

Prove that Product and Sum are Monoids ? They are!

  • Both are Associative. 
  • Identity for Product = Unit ()
  • Identity for Sum  = Void

 Product (*) , Sum (+) are Distributive : 

a * (b + c ) = a * b + a * c \iff (a , (Either \: b \: c)) = Either \:  (a, b) \:( a, c)

There is is no inverse for “sum”, or negative.

Hence, it is a  structure  Ring without “n” = Rig (or Semi-Ring)

Maybe (= 1+a)

data Maybe = Nothing | Just a

\boxed {\text {Maybe } a = \text {Either () } a}

Algebraic Data Types: 

We can solve algebraic equation with Product & Sum :

BM Category Theory II 1.1: Declarative vs Imperative Approach

Excellent lecture using Physics and IT to illustrate the 2 totally different approaches in Programming:

  1. Imperative (or Procedural) – micro-steps or Local 微观世界 [eg. C / C++, Java, Python…]
  2. Declarative (or Functional) – Macro-view or Global 大千世界 [eg. Lisp / Clojure, Scala, F#, Haskell…]

In Math

  1. Analysis (Calculus) 
  2. Algebra (Structures: Group, Ring, Field, Vector Space, Category …)

In Physics:

  1. Newton (Laws of Motion), Maxwell (equations) 
  2. Fermat (*)  (Light travels in least time), Feynman (Quantum Physics).

In IT: Neural Network (AI)  uses both 1 & 2.

More examples…

In Medicine:

  1. Western Medicine: germs/ viruses, anatomy, surgery
  2. Traditional Chinese Medicine (中医): Accupunture, Qi, Yin-Yang.

Note (*): Fermat : My alma mater university in Toulouse (France) named after this 17CE amateur mathematician, who worked in day time as a Chief Judge of Toulouse City, after works spending time in Math and Physcis. He co-invented Analytic Geometry (with Descartes), Probability (with Pascal), also was the “Father of Number Theory” (The Fermat’s ‘Little’ Theorem and The Fermat’s ‘Last’ Theorem). He used Math to prove light travels in straight line (before Newton) due to “Least Time taken” (explained here in this BM video).

https://tomcircle.wordpress.com/2013/04/05/lay-cables-at-least-cost/


Revision :Part 1 Motivation & Philosophy of Category Theory