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

• 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

Link

• Isomorphism: a deep structural equivalence - equal shape
• “Guts of mathematical proof are made of the same stuff as types”

• 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

Link

• Detecting errors
  • Typos
  • Not all parameters provided
• Enforces abstraction
  • You can define a program through its types
  • When you talk about methods, it’s about 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

• Front load checking -> front load design
• Inferencer + type checker is very potent

Gradual Type Systems

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

Link

• 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

Link

• 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

Link

…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

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

• Types systems are really cool
• Types are a prism - another way to view code
• Can be a guide