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

Link

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

Link

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

Link

You can have a robotic guide to help with your programs

Gradual Type Systems

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

Link

(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

Link

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

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

Link

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

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

Link

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

Experience from Developing the Dialyzer - Sagonas, 2005

Link

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

Conclusions