## Notes on - Know Your Types - Michael Bernstein

Update: Corrected false relation between Tobin-Hochstadt’s and Siek’s & Taha’s efforts. Thanks @samth!

This post is a sort of outlining of Michael Bernstein’s excellent talk, Know Your Types. Several links are captured below for convenience.

## What are Types?

### Cardelli, 1996 - Type Systems

• Bernstein’s law: the more outdated the web page, the more advanced the material.

Types: An estimate of the collection of values that a program can assume during program execution.

• Type rule: a component of a type system. Rules that forbids programs from going wrong.
• A collection of type rules for a typed programming language. Same as a static type system.
• Statically checked language: A language where good behavior is determined before execution.
• Dynamic languages: good for building small programs to do specific things
• Static languages: large programs, financial applications
• Typechecking: The process of checking a program before execution to establish its compliance with a given type system and therefore to prevent the occurrence of forbidden errors.
• Type inference: The process of finding a type for a program within a given type system.

## How Can Types Help Us?

### Phillip Wadler, 2014 - Propositions as Types

• Isomorphism: a deep structural equivalence - equal shape
• “Guts of mathematical proof are made of the same stuff as types”
Logic Programming
Universal quantification Generalized function space (PI type)
Existential quantification Generalized cartesian product (SIGMA type)
Implication Function Type
Conjunction Product Type
Disjunction Sum Type
True formula Unit Type
False formula Bottom Type
• Normalization of proofs is evaluation of a program
• We leverage proof tools for programming purposes
• We can reach enlightenment
• What can types do for us?

### Types and Programming Languages, Pierce - 2002

• Detecting errors
• Typos
• Not all parameters provided
• Enforces abstraction
• You can define a program through its types
• What does it accept?
• What does it return?
• An unchanging interface -> documentation
• Safety

You can have a robotic guide to help with your programs

• Inferencer + type checker is very potent

### A Practical Optional Type System for Clojure, Bonnaire-Sergeant - 2012

• Gradual type checking exists and works
``````(ns typed.test.collatz
(:require [typed.core :refer (check-ns ann)))

(ann collatz [Number -> Number])
(defn collatz [n]
(cond
(= 1 n)
1
(and (integer? n)
(even? n))
(collatz (/ n 2))
:else
(collatz (inc (+ 3 n)))))``````

### Typed Scheme: From Scripts to Programs, Tobin-Hochstadt - 2010

• Scripts: no need for upfront thinking
• Stuff in -> stuff out
• Related: Gradual Typing for Functional Languages Siek & Taha, 2006
• A means for annotating a program to see what it actually does so that you don’t have to run it to see what goes wrong

…safe interoperability between typed and untyped portions of a single program

• As long as the boundaries between static/dynamic portions of program are marked, it works.
• Easier in a functional programming language

### Dynamic Inference of Static Types for Ruby, An, Chaudhuri, Foster - 2011

…constraint-based dynamic type infererncer, a technique that infers types based on dynamic program execution

• Generates types from running existing code

### The Ruby Type Checker - Ren, Toman, Strickland - 2013

RTC is designed so programmers can control exactly where type checking occurs: type-annotated objects serve as “roots” of the type checking process, and unannotated objects are not typed checked.

``````require 'rtc.lib'

class Person
rtc.annotated
...
typesig "personnel_id: () -> Fixnum"
def personnel_id ... end

typesig "self.from_id: (Fixnum) -> Person"
def self from_id(id) ... end

typesig "manager: () -> Manager or %false"
def manager ... end
end``````