# Tag Archives: BM

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

…

# Category Theory III Part 3

**3.1 Adjunction and Monad**

Tip:

L = Free,

R = Conservative (get rid of structure / forgetful)

Examples

L: C- >D

Monoid – > Free Monoid

Algebras – > Free Algebras…

R: D – > C

**Adjunction gives “Monad” **

**3.2 Monad Algebras**

Tip: Think Monad as “List” container

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

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” 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):

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]**

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 ->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 …]

Intuition:[Artificial Intelligence] You teach the computer like to a Primary 6 kid, thatAlgebrais atypeof expression(f) which, after evaluation, returns a value.

**If a = i (initial) **

*[or u (terminal)]*,

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

**Lambek’s Lemma**

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

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

# Category Theory II 7: Comonads

# BM 5&6 : Category Adjunctions 伴随函子

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

**Equivalence** of 2 Categories if:

5.2 Adjunction definition: such that the 2 **triangle identities** below ( red and blue) exist.

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

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 :

**Examples** : Product & Exponential are Right Adjoints

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

vice-versa.

With **Product** (**Left Adjoint**) and **Exponential** (**Right Adjoint**) =>

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

- Index category (I)
- Category C: Functors (constant , D)
- Cones (Lim D)
- Functor Category [I, C ]:objects are (constant, D ), morphisms are natural transormations
- 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

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

- Define a
**Pattern**, **Ranking**which object is better,- 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: **

**‘**the Function object*eval*‘**‘**to return*(a=>b) x a*‘**result b**is up to*g***Unique****isomorphism (**SAME as ‘*h*):*eval*‘

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

**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}

The number of possibilities of applying **f** from **a to b** is , hence we call:

8.2 Algebraic Data Types

# BM Category Theory 7: Category of categories

# BM Category Theory 6: Functors & Examples

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

**Examples of Functors**:

1. **List**

2. **Reader**

Functor (esp. Endo-functor) can be viewed as a

Containerwhere 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 :

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

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

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

In **Math**:

- Analysis (Calculus)
- Algebra (Structures: Group, Ring, Field, Vector Space, Category …)

In **Physics**:

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

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

More examples…

In **Medicine**:

- Western Medicine: germs/ viruses, anatomy, surgery
- 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/