Instantly share code, notes, and snippets.

Last active July 4, 2023 17:16
Show Gist options
• Save tkersey/69c36bcf40e23f7ef5c82a9c63983a13 to your computer and use it in GitHub Desktop.

# \$\$A × A → A\$\$

```protocol Magma {
static func <> (lhs: Self, rhs: Self) -> Self
}```

# \$\$A × A → A\$\$

```interface Magma<A> {
readonly concat: (x: A, y: A) => A
}```

# \$\$A × A → A\$\$

`protocol Semigroup: Magma {}`

# \$\$A × A → A\$\$

`interface Semigroup<A> extends Magma<A> {}`

# [fit] Associativity

\$\$a <> (b <> c) ≅ (a <> b) <> c\$\$ \$\$a + (b + c) ≅ (a + b) + c\$\$ \$\$a × (b × c) ≅ (a × b) × c\$\$ \$\$a → (b → c) ≅ (a → b) → c\$\$

# \$\$A × A + 1 → A\$\$

```protocol Monoid: Semigroup {
static var empty: Self { get }
}```

# \$\$A × A + 1 → A\$\$

```interface Monoid<A> extends Semigroup<A> {
}```

# [fit] Identity

\$\$a <> empty = empty <> a = a\$\$ \$\$a + empty = empty + a = a\$\$ \$\$a × empty = empty × a = a\$\$

# Sum

```struct Sum<A: Numeric>: Monoid {
let sum: A

init(_ sum: A) {
self.sum = sum
}

static func <> (lhs: Sum, rhs: Sum) -> Sum {
self.init(lhs.sum + rhs.sum)
}

static var empty: Sum {
0
}
}```

# Sum

```const Sum: monoid<number> = {
empty: 0,
concat: (u: number, v: number) => u + v
}```

# Product

```struct Product<A: Numeric>: Monoid {
let product: A

init(_ product: A) {
self.product = product
}

static func <> (lhs: Product, rhs: Product) -> Product {
self.init(lhs.product * rhs.product)
}

static var empty: Product {
1
}
}```

# Product

```const Product: monoid<number> = {
empty: 1,
concat: (u: number, v: number) => u * v
}```

# Endo

```struct Endo<A>: Monoid {
let call: (A) -> A

init(_ call: @escaping (A) -> A) {
self.call = call
}

static func <> (lhs: Endo<A>, rhs: Endo<A>) -> Endo<A> {
.init { rhs.call(lhs.call(\$0)) }
}

static var empty: Endo<A> {
.init { \$0 }
}
}```

# Endo

```const Endo = <A>(): Monoid<Endo<A>> => ({
empty: (a) => a,
concat: (lhs: Endo<A>, rhs: Endo<A>) => rhs(lhs())
})```

# All

```struct All: Monoid {
let bool: Bool

init(_ bool: Bool) {
self.bool = bool
}

static func <> (lhs: Bool, rhs: Bool) -> Bool {
.init(lhs.bool && rhs.bool)
}

static var empty: Bool {
.init(true)
}
}```

# All

```const All: monoid<boolean> = {
empty: true,
concat: (x, y) => x && y
}```

# Any

```struct Any: Monoid {
let bool: Bool

init(_ bool: Bool) {
self.bool = bool
}

static func <> (lhs: Bool, rhs: Bool) -> Bool {
.init(lhs.bool || rhs.bool)
}

static var empty: Bool {
.init(false)
}
}```

# Any

```const Any: monoid<boolean> = {
empty: false,
concat: (x, y) => x || y
}```

# Array

```extension Array: Monoid {
static func <> (lhs: Array, rhs: Array) -> Array {
lhs + rhs
}

static var empty: Array {
[]
}
}```

# List

```const List: monoid<Array<A>> = {
empty: [],
concat: (x, y) => x.concat(y)
}```

# String

```extension String: Monoid {
static func <> (lhs: String, rhs: String) -> String {
lhs + rhs
}

static var empty: String {
""
}
}```

# String

```const String: monoid<string> = {
empty: '',
concat: (x, y) => x + y
}```

# Maybe

```extension Optional: Monoid where Wrapped: Monoid {
static func <> (lhs: Optioanl, rhs: Optional) -> Optional {
switch (lhs, rhs) {
case (.none, _):
return rhs
case (_, .none):
return lhs
case let (.some(l), some(r)):
return .some(l <> r)
}
}

static var empty: Optional {
.none
}
}```

# Maybe

```export interface None {
}

export interface Some<A> {
}

export type Option<A> = None | Some<A>

export const isSome: <A>(fa: Option<A>) => fa is Some<A> = _.isSome
export const isNone = (fa: Option<unknown>): fa is None => fa._tag === 'None'

export const Maybe = <A>(S: Semigroup<A>): Monoid<Option<A>> => ({
empty: none,
concat: (x, y) => (isNone(x) ? y : isNone(y) ? x : some(S.concat(x.value, y.value)))
})```

# O(N²)

```reverse :: [a] -> [a]
reverse [] = []
reverse (a : as) = reverse as ++ [a]```

# List monoid

```instance Monoid [a] where
mempty = []
mappend as bs = as ++ bs```

# Every monoid can be represented by a set of endo-functions.

`type DList a = [a] -> [a]`
```rep :: [a] -> DList a
rep as = \xs -> as ++ xs```
```unRep :: DList a -> [a]
unRep f = f []```
```rep [] = id
rep (xs ++ ys) = rep xs . rep ys```
```rev :: [a] -> DList a
rev [] = rep []
rev (a : as) = rev as . rep [a]```

# O(N)

```fastReverse :: [a] -> [a]
fastReverse = unRep . rev```

# Foldable

```protocol Foldable {
associatedtype A
associatedtype B

func foldr(_ folder : (A) -> (B) -> B, _ initial : B) -> B

func foldl(_ folder : (B) -> (A) -> B, _ initial : B) -> B

func foldMap<M : Monoid>(_ map : (A) -> M) -> M
}
https://github.com/alskipp/Monoid/commit/86b6f0f85e85f0eec5a005f092501f8dc8f2da80```

# [fit] solves data engineering (Podcast)

How the abstract algebra and probabilistic data structures help solve fast versus big data issues that many are struggling with.

autoscale: true

# Algebra

Symbols Operations Laws
0, 1, 2, x, y, z +, –, ×, % 0 + x = x

# Algebra

Symbols Operations Laws
Types Type constructors ?
(Void, Int, Bool) (Optional, Either) ?

# Algebra

Symbols Operations Laws
Things Ways to make
new things
Rules the
things follow

# \$\$0\$\$

`enum Never {}`

# \$\$0\$\$

`type Void = never`

# \$\$1\$\$

`struct Unit {}`

# \$\$1\$\$

`type Unit = void`

# \$\$2\$\$

```enum Bool {
case true
case false
}```

# \$\$2\$\$

`type Bool = False | True`

# \$\$3\$\$

```enum Three {
case one
case two
case three
}```

# \$\$3\$\$

`type Three = One | Two | Three`

# \$\$+\$\$

```enum Either<L, R> {
case left(L)
case right(R)
}```

# \$\$+\$\$

`type Either<L, R> = Left<L> | Right<R>`

# \$\$+\$\$

```Either<Bool, Three>
.left(.false)
.left(.true)
.right(.one)
.right(.two)
.right(.three)```

# \$\$+\$\$

```Either<Bool, Three>
Left<False>
Left<True>
Right<One>
Right<Two>
Right<Three>```

# \$\$×\$\$

```struct Pair<First, Second> {
let first: First
let second: Second
}```

# \$\$×\$\$

`type Pair<First, Second> = [First, Second]`

# \$\$×\$\$

```Pair<Bool, Three>
Pair(.false, .one)
Pair(.false, .two)
Pair(.false, .three)
Pair(.true, .one)
Pair(.true, .two)
Pair(.true, .three)```

# \$\$×\$\$

```Pair<False,One>
Pair<False,Two>
Pair<False,Three>
Pair<True,One>
Pair<True,Two>
Pair<True,Three>```

# AR

```struct Reader<R, A> {
let run: (R) -> A
}```

# AR

```interface Reader<R, A> {
(r: R): A
}```

# AR

```Set<(Three) -> Bool>
(.false, .false, .false),
(.false, .false, .true),
(.false, .true,  .true),
(.false, .true,  .false),
(.true,  .true,  .true),
(.true,  .true,  .false),
(.true,  .false, .false),
(.true,  .false, .true),```

# \$\$1 + A\$\$

```struct Optional<A> {
case none
case some(A)
}```

# \$\$1 + A\$\$

`type Option<A> = None | Some<A>`

# \$\$1 + A × List\$\$

```enum List<A> {
case empty
indirect case cons(A, List<A>)
}```

# \$\$1 + A × List\$\$

`type List<A> = Nil | Cons<Pair<A, List<A>>>`

### \$\$List = 1 / (1 - A)\$\$

``````List<A> = 1 / (1 - A)
= 1 + A + A×A + A×A×A + A×A×A×A + ...
= 1 + A + A² + A³ + A⁴ + ...
``````

# \$\$T = 1 + A × T²\$\$

```enum Tree<A> {
case empty
indirect case node(A, Pair<Tree<A>, Tree<A>>)
}```

# \$\$T = 1 + A × T²\$\$

`type Tree<A> = Empty | Node<A, Pair<Tree<A>, Tree<A>>>`

autoscale: true

# [fit] then tune and adjust behavior accordingly

## Footnotes

1. [Intro to Empirical Software Engineering: What We Know We Don't Know]((https://youtu.be/WELBnE33dpY?t=1698)

autoscale: true

# \$\$λ\$\$-calculus

Syntax Name Description
x Variable A character or string representing a parameter or mathematical/logical value
(λx.M) Abstraction Function definition (M is a lambda term). The variable x becomes bound in the expression
(M N) Application Applying a function to an argument. M and N are lambda terms

# [fit] Curry-Howard-Lambek

Logic Types Categories
propositions types objects
proofs terms arrows
proof of proposition A inhabitation of type A arrow f: t → A
implication function type exponential
conjunction product type product
disjunction sum type coproduct
falsity void type (empty) initial object
truth unit type (singleton) terminal object T

# [fit] Curry-Howard-Lambek

Logic Types Categories
propositions types objects
proofs terms arrows
proof of proposition A inhabitation of type A arrow f: t → A
implication function type exponential
conjunction product type product
disjunction sum type coproduct
falsity void type (empty) initial object
truth unit type (singleton) terminal object T

# [fit] Tagged

`type Dollars = number & { readonly __tag: unique symbol };`

# [fit] Total Functions

### Just another name for a regular function to make it clear that it is defined for all elements of its input.

`head :: [a] -> a`

`safehead :: [a] -> Maybe a`

`type NonEmptyArray<T> = [T, ...T[]];`

# [fit] Functions with side effects

### A function that has an observable effect besides returning a value.

```interface Writer<W, A> {
(): [A, W]
}```

# [fit] UI is a function of state

`UI = fn(state)`

# [fit] Correspondence

^ A direct relationship between computer programs and mathematical proofs ^ Pictures and bios of Curry and Howard ^ Give a little explaination of your passion for mathematical thinking

# [fit] Curry-Howard

Logic Types
propositions types
proofs terms
proof of proposition A inhabitation of type A
implication function type
conjunction product type
disjunction sum type
falsity void type (empty)
truth unit type (singleton)

# [fit] Curry-Howard

Logic Types
propositions types
proofs terms
proof of proposition A inhabitation of type A
implication function type
conjunction product type
disjunction sum type
falsity void type (empty)
truth unit type (singleton)
^ It's enough to have an instance (inhabitant) of a type to prove it

# [fit] Curry-Howard

Logic Types
propositions types
proofs terms
proof of proposition A inhabitation of type A
implication function type
conjunction product type
disjunction sum type
falsity void type (empty)
truth unit type (singleton)

# [fit] into structured data

`const head = (i: Array<a>): a = {...}`

`const head = (i: Array<a>): Maybe<a> = {...}`

```export interface None {
}

export interface Some<A> {
}

export type Maybe<A> = None | Some<A>```

# [fit] Curry-Howard-Lambek

Logic Types Categories
propositions types objects
proofs terms arrows
proof of proposition A inhabitation of type A arrow f: t → A
implication function type exponential
conjunction product type product
disjunction sum type coproduct
falsity void type (empty) initial object
truth unit type (singleton) terminal object T