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

L = Free,
R = Conservative (get rid of structure / forgetful)

Examples
L: C- >D
Monoid – > Free Monoid
Algebras – > Free Algebras

R: D – > C

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. $\boxed {\text {Algebraic Data : by Product, Sum}}$

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]

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]

(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/

Yoneda lemma in nLab

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