Notes on - Know Your Types - Michael Bernstein

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

Talk: Link

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?

What do we talk about when we talk about types? We don’t talk about types, we argue about them.

Cardelli, 1996 - Type Systems


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

How Can Types Help Us?

Phillip Wadler, 2014 - Propositions 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

Types and Programming Languages, Pierce - 2002


You can have a robotic guide to help with your programs

Gradual Type Systems

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


(ns typed.test.collatz
  (:require [typed.core :refer (check-ns ann)))

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

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


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

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

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

Experience from Developing the Dialyzer - Sagonas, 2005


…testing, no matter how thorough, cannot of course detect all software defects. Tools that complement testing, such as static analyzers, have their place in software development regardless of language.