autoscale: true
# [fit] **TDD**
---
# [fit] **$$λ$$-calculus**
---
# **$$λ$$-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] Let's think of a **unit test**
# [fit] like **function application**
---
# [fit] we'll **vary** our **input**s
# [fit] while **assert**ing on our **output**s
---
# [fit] Unit test
# [fit] **Input → Output**
---
# [fit] **Local reasoning**
### the idea that the reader can **make sense of** the **code** directly in front of them, **without** going on a journey **discovering how** the code **works**.
---
# [fit] **Pure**
# [fit] Functions
---
# [fit] **Pure** Functions
### The function return values are identical for identical arguments
### The function application has no side effects
---
# [fit] **Curry-Howard-Lambek**
# [fit] correspondence
---
## [fit] **Intuitionistic Logic**
## [fit] ≅
## [fit] **Typed Lambda Calculus**
## [fit] ≅
## [fit] **Cartesian Closed Categories**
---
## [fit] **Logic**
## [fit] ≅
## [fit] **Types**
## [fit] ≅
## [fit] **Categories**
---
# [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] **Propositions**
# [fit] as **types**
---
# [fit] **proofs**
# [fit] as **programs**
---
# [fit] **normalization of proofs**
# [fit] as **evaluation of programs**
---
# [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] **implication**
# [fit] a → b
# [fit] **if a then b**
---
# [fit] **Tagged**
-
-
```typescript
type Dollars = number & { readonly __tag: unique symbol };
```
---
# [fit] **Scoping**
## [fit] The extent of the area or subject matter
## [fit] that something deals with or to which it is relevant.
---
# [fit] **Total** Functions
---
### Just another name for a regular **function** to make it clear that it is **defined** for **all** elements of its **input**.
---
```typescript
head :: [a] -> a
```
---
```typescript
safehead :: [a] -> Maybe a
```
---
```typescript
type NonEmptyArray<T> = [T, ...T[]];
```
---
# [fit] **[Parse don't validate](https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate)**
---
# [fit] Make **impossible**
# [fit] **states** impossible
---
# [fit] Functions with **side effects**
---
### A **function** that has an observable **effect** besides returning a value.
---
```typescript
interface Writer<W, A> {
  (): [A, W]
}
```
---
# [fit] **Architecture**
---
# [fit] **UI** is a **function** of **state**
---
```typescript
UI = fn(state)
```
---
# [fit] Model–view–viewmodel (**MVVM**)
---
# [fit] **Moore** machine
---
### a finite-state machine whose output **values** are **determined** only by its current **state**.
---
# [fit] **elm**
---
# [fit] **Redux**
---
# [fit] **[Janus](http://janusjs.org)**
---
# [fit] **The Composable**
# [fit] **Architecture**
---
# [fit] **Property tests**
---
# [fit] **Galaxy brain**
![](https://i.imgur.com/br96EPe.jpeg)

---
![](https://i.imgur.com/br96EPe.jpeg)
# [fit] **Dependent types**
---
![](https://i.imgur.com/br96EPe.jpeg)
# [fit] **[Systems as Wiring Diagram Algebras](https://johncarlosbaez.wordpress.com/2019/01/28/systems-as-wiring-diagram-algebras)**
---
![](https://i.imgur.com/br96EPe.jpeg)
# [fit] **[Fabulous Fortunes, Fewer Failures, and Faster Fixes from Functional Fundamentals](https://www.youtube.com/watch?v=FskIb9SariI)**