Benefits of types

!

Correctness

Types enforce logical correctness

// ages have to be numbers
// your age cannot be "carrot"
val age: Int = 34

// in un-typed languages your age can be "carrot"
// that sucks

Your compiler reasons about your code. Instead of just you

This is the obvious one

Documentation

Types tell you what your code does

If you change your "documentation", your code won't compile until it matches!

// what does this function do?
func concat(x: String, x: String): String

// what does this function do?
func concat(x: [Int], y: [Int]): [Int]

If you change code attached to a comment,

the compiler won't stop you

/**
 * Concat two strings to make a larger one
 */
var z = x + y

Whenever I find myself writing a comment I always think, can I express this clearly with better types or another function?

Reuse + Testability

Types help you write composable code

// after
func prefetch(photo: Photo, /*...*/): Eventually<PrefetchedPhoto>

In Roll, the we have a step where we prefetch photos for the cards in the feed.

This is what the code used to look like:

Handling the prefetch finishing wasn't exposed in the type signature.

We wanted to reuse this logic for getting photos for notifications:

// before
func prefetch(photo: Photo, /*...*/)

Now we can do whatever we want with the result!

Performance

How do untyped languages work?

var x = 4 // computer: x is a number
var y = x + 1 // computer: is x a number? good. y is a number
println(fib(y)) // computer: is fib a function? does fib return something I can print? good

They're actually uni-typed of type

"you can ask me what I really am"

Types let the computer solve these problems at compile time

Reading type theory

it's a science!

The Rules of Rules + Guide

(above the line) implies (below the line)

Γ = context (other things you proved)

Γ,(Γ1) = extend your context with Γ1

⊢ = entailment

stuff right of ⊢ = judgement

These are common axioms:

if J is in your context, then J is true

if J is true, then you can weaken your context (add judgements) and J is still true

if K is true, and if you show J with K, you can treat GAMMA as having K later

Non-recursive types

basically primitives

Zero

(type theory void)

// Swiftish
func f(x: Int) -> Void {
  while (true) { }
}

aka void, bottom, or ⊥

T -> Void functions diverge

One

(the void in Java)

// in Kotlin `Unit` is both a type and a value
val x: Unit = Unit

// in Swift `Void` or `()` is the type of Unit, `()` is the value
let x: () = ()

aka unit, 1

Functions where you omit a return statement and that don't diverge are actually return unit

// f : Int -> Unit
func f(x: Int) {
  println("You passed in ${x}")
}

Everything else

(Bool (or 2), Int, String, etc.)

val x: Int = 0
val s: String = ""
// Bools are also known as 2 because there are two choices
val y: Bool = false 

These types exist obviously but they usually don't matter unless you talk about something extremely specific

Product types

(tuples / structs / classes)

Product types

// kotlin
val oneTwo: Pair<Int, Int> = 1 to 2 // intro
println(oneTwo.first) // elim
data class Person(name: String, age: Int)

// swift
struct Person { name: String, age: Int }
let p: Person = Person(name: "Doug", age: 34) // intro
println(p.name) // elim

Why product?

How many values exist of type Bool x Unit?

What about Bool x Bool?

What about Bool x (Bool x Unit)

(T1 x T2)

intro

elim

Sum types

(tagged unions / good enums)

Sum types

// swift
enum ViewCell {
  case HeaderCell(title: String, childrenCount: Int),
  case ContactCell(name: String, phoneNumber: String),
  /* etc */
}

This is what I call a "good" enum

let v: ViewCell = HeaderCell("Suggested Invites", 9) // intro

switch v { // elim
  case HeaderCell(let title, _): println("This is ${title}")
  case ContactCell(_, let num): println("Contact me at ${num}")
}

intro

elim

(T1 + T2)

Sum types

// kotlin
enum Color(val rgb: Int) {
  Red(0xF00),
  Green(0x0F0),
  Blue(0x00F)
}

This is what I call a "bad" enum

Notice that I didn't give the parameters in the cases names. The rgb value MUST be included for all cases.

You can only declare types of the form p1 + p1 not p1 + p2 for any products p1,p2

Sum types

// kotlin
object ViewCell {
  abstract class Sum{
    fun match<T>(
      headerCell: (HeaderCell) -> T
      contactCell: (ContactCell) -> T
    ): T {
      when (this) {
        is HeaderCell -> return headerCell(this)
        is ContactCell -> return contactCell(this)
        else -> throw MatchException()
      }
    }
  }

  data class HeaderCell(val title: String, val children: Int): Sum()
  data class ContactCell(val name: String, val phoneNumber: String): Sum()
}

Hacking in "good" enums

val x: ViewCell.Sum = HeaderCell("Suggested Invites", 9) // intro

// elim
viewCell.match(
  headerCell = { h -> println("My title is ${h.title}") }
  contactCell = { c -> println("My name is ${c.name}") }
)

Option type

// swift/kotlin (we write Unit + Int as Int?)
// and we use null or nil to get the left projection
// and some value that's not null or nil to get the right projection
val imNotHere: Int? = nil
val imHere: Int? = 3

(Unit + T1)

Option types are sum types where the left projection is Unit !

Sloppy Products

struct SloppyCar {
  hasRoof: Bool
  roofColor: Color?
  /* other stuff */
}

Why is this bad? (contrived example but whatever)

Sloppy Products

struct SloppyViewCell {
  headerCell: HeaderCell?
  contactCell: ContactCell?
}

Why is this bad? (contrived example but whatever)

Moral

Sum types are the dual of product types.

You should probably be using them as often as you use products.

Think about what values your data structures permit and if there is a logical flaw than you've defined a bad type

Exponential types

(Functions)

Exponential types

(T1 -> T2)

// intro
val addOne: (Int) -> Int = { x -> x + 1 }
// elim
val three = addOne(2)

intro

elim

Why exponential?

How many values inhabit 'Bool -> Bool?' ?

How many values inhabit 'Bool? -> Bool' ?

Bool -> Bool?

1: 0 -> 0
   1 -> 0
2: 0 -> 0
   1 -> 1
3: 0 -> 1
   1 -> 0
4: 0 -> 1
   1 -> 1
5: 0 -> 0
   1 -> 2
6: 0 -> 1
   1 -> 2
7: 0 -> 2
   1 -> 0
8: 0 -> 2
   1 -> 1
9: 0 -> 2
   1 -> 2

(0 = false, 1 = true, 2 = nil)

Side-effects

(making sadness)

Side-effects

(they're scary)

Side effects are the things that an expression does that isn't expressed in the type signature

Why is this bad?

Side-effects

examples

Some common side effects

// printing to the console
println("hello") // benign usually

// reading/writing to a mutable variable
// the less isolated it is the harder it is to reason over
// if the variable is immutable it's easy to reason
global = 4

// reading/writing to a database or disk
db.read(data)

// making a network request
network.get("http://google.com")

// getting a random number
Math.random() // benign usually

Side-effects

(deal with it)

Unfortunately, you need side effects.

You need to talk to the network. You need to save things to databases.

This sucks

To deal with it:

Isolate

Hide

Isolation

(peripheralize it)

The idea here is because it's hard to reason about side effects.

Put all the side effect crap off to the side and then keep the rest of your program pure

http://cycle.js.org/drivers.html is a good example of this

Referential Transparency

(hide them)

Referential transparency means you can replace the expression with its evaluated value and your program is the same.

Thus, your types express what your code does.

Pure functions are always referentially transparent.

Functions with side effects CAN be referentially transparent sometimes

object Fib {
  // state. impureness
  private val memo = 
     hashMapOf<Int, Int>()
  
  fun fib(x: Int): Int {
    return memo.get(x).getOrElse {
      if (x == 0 || x == 1) {
        1
      } else {
        val res = fib(x-1) + fib(x-2)
      	memo.put(x, res)
      	res  
      }
    }
  }
}
// state is hidden.
// function call can always replace with value.

Immutability

(life is good)

Using immutable variables and values as much as possible ELIMINATES a class of side-effects.

Parallelism works. 

Concurrency becomes easy.

This is important in the age of multi-core processors

Immutability

(important distinction)

// a mutable variable of a mutable list
var x = arrayListOf(1,2,3)
x = arrayListOf(2,3) // valid
x.add(4) // valid

// an immutable variable holding a mutable list
val x = arrayListOf(1,2,3)
x = arrayListOf(2,3) // INVALID
x.add(4) // valid!
 

// a mutable variable holding an immutable list
var x = listOf(1,2,3)
x = listOf(2,3) // valid!
x.add(4) // INVALID
// be careful!
// I find that I get a lot of side-effect related logic errors using this

// an immutable variable holding an immutable list
val x = listOf(1,2,3)
x = listOf(2,3) // INVALID
x.add(4) // INVALID
// try to use this as much as possible

Immutability

more next week