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?
What do we talk about when we talk about types? We don’t talk about types, we argue about them.
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”
||Generalized function space (PI type)
||Generalized cartesian product (SIGMA 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
- 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
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
- Gradual type checking exists and works
Typed Scheme: From Scripts to Programs, Tobin-Hochstadt - 2010
- Scripts: no need for upfront thinking
- 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.
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.
- Types systems are really cool
- Types are a prism - another way to view code
- Can be a guide