Oliver Wong (olivwong@) — Amazon 2014
“People sometimes make errors. The problem here was not the error, it was the failure of NASA's systems engineering, and the checks and balances in our processes to detect the error. That's why we lost the spacecraft.”Dr. Edward Weiler, NASA's Associate Administrator for Space Science
def getImpulse(): double {
//...
}
def updateThrusters(impulse: double) {
//...
}
updateThrusters(getImpulse());
/**
* ...
* @return the impulse in pound * seconds.
*/
def getImpulse(): double {
//...
}
/**
* ...
* @param impulse the impulse in newton * seconds.
*/
def updateThrusters(impulse: double) {
//...
}
updateThrusters(getImpulse());
/**
* ...
* @return the impulse in pound * seconds.
*/
def getImpulse(): PoundSecond {
//...
}
/**
* ...
* @param impulse the impulse in newton * seconds.
*/
def updateThrusters(impulse: NewtonSecond) {
//...
}
updateThrusters(getImpulse()); //Compile error
def getImpulse(): Impulse {
//...
return new PoundSecond();
}
def updateThrusters(impulse: Impulse) {
var x = Impulse.getNewtonSecond();
//...
}
updateThrusters(getImpulse()); //Autoconversion via polymorphism
v : ℝ m/s = (3 meters + 4 meters )/5 seconds (* OK *)
v : ℝ m/s = (3 meters + 4 seconds)/5 seconds (* type error *)
v : ℝ m/s = (3 meters + 4 meters )/5 (* type error *)
http://www.eecis.udel.edu/~cavazos/cisc879-spring2008/papers/fortress.pdf
Bugs happen when a programmer expects a piece of code to do something, but the code does something else.
“People sometimes make errors. The problem here was not the error, it was the failure of NASA's systems engineering, and the checks and balances in our processes to detect the error. That's why we lost the spacecraft.”Dr. Edward Weiler, NASA's Associate Administrator for Space Science
public ; class void } 3<null>
No idea what you're trying to say.
int foo = (int) "Hello";
I know what you're trying to do, but I'm not gonna let you do it because it looks like a bug.
A type system is a collection of rules that assign a property called a type to the various constructs […] a computer program is composed of. The main purpose of a type system is to reduce bugs in computer programs by defining interfaces between different parts of a computer program, and then checking that the parts have been connected in a consistent way.http://en.wikipedia.org/wiki/Type_system
I expect the code to do something:
def executeAction(user) {
//...
}
val user = User.findById(userId);
executeAction(user);
But the code does something else:
/**
* user: the id of user making the request.
*/
def executeAction(user: Int) {
//...
}
val user = User.findById(userId);
executeAction(user); //BUG
A type system is a set of types […] along with the rules that govern whether or not a program is legal with respect to [those] types.http://www-plan.cs.colorado.edu/diwan/3155-f04/TypeChecking.pdf
The rules in a given type system allows some programs and disallows other programs. For example, unlike assembly language, one cannot write a program in Java that grabs a random word from memory and treats it as if it were an integer.http://www-plan.cs.colorado.edu/diwan/3155-f04/TypeChecking.pdf
Thus, every type system represents a tradeoff between expressiveness and safety.http://www-plan.cs.colorado.edu/diwan/3155-f04/TypeChecking.pdf
boolean
Choosing a language is implicitly choosing a type system.
(We'll get back to this later).A type system is a collection of rules that assign a property called a type…http://en.wikipedia.org/wiki/Type_system
A type system is a set of types […] along with the rules…http://www-plan.cs.colorado.edu/diwan/3155-f04/TypeChecking.pdf
Definition: a type is a set of values.http://www-plan.cs.colorado.edu/diwan/3155-f04/TypeChecking.pdf
A type is a set of values… and the set of operations allowed on those values.me
class Foo {
}
class Bar extends Foo {
public void frobulate();
}
Foo f = new Foo();
Bar b = new Bar();
The distinction is not important for this talk.
Types are sets of values, ∴ if you completely specify the types of your program, you completely specify the allowed values that variables can have, that methods can take as input, etc.
In other words, you are completely specifying all possible states the program can have while it is running, and thus all possible behavior it can exhibit.
Static typing fanatics try to make us believe that “well-typed programs cannot go wrong”. While this certainly sounds impressive, it is a rather vacuous statement. […] [Static type checking] is necessarily only partially sound and incomplete. This means that programs can still go wrong because of properties that are not tracked by the type-checker.Erik Meijer and Peter Drayton — Static Typing Where Possible, Dynamic Typing When Needed
Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete.http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems
(Also: Halting Problem, Rice's Theorem, etc.)
Erik Meijer and Peter Drayton — Static Typing Where Possible, Dynamic Typing When NeededWhen programmers say “I need […] static typing”, they really mean […] “I want contracts”
Static typing provides a false sense of safety, […] even if a program does not contain any static type-errors, this does not imply that you will not get any unwanted runtime errors.
Current type-checkers basically only track the types of expressions and make sure you do not assign a variable with a value of an incompatible type, that the arguments to primitive operations are of the right type (but not that the actual operation succeeds), and that the receiver of a method call can be resolved statically (but not that the actual call succeeds).Erik Meijer and Peter Drayton — Static Typing Where Possible, Dynamic Typing When Needed (No date on PDF, but includes citations from 2004)
Erik Meijer and Peter Drayton — Static Typing Where Possible, Dynamic Typing When NeededHowever in general programmers want to express more advanced contracts about their code. For example, an invariant that the value of one variable is always less than the value of another, a precondition that an argument to a method call is within a certain range, or a postcondition that the result of a method call satisfies some condition.
Erik Meijer and Peter Drayton — Static Typing Where Possible, Dynamic Typing When NeededHowever in general programmers want to express more advanced contracts about their code. For example, an invariant that the value of one variable is always less than the value of another, a precondition that an argument to a method call is within a certain range, or a postcondition that the result of a method call satisfies some condition.
http://en.wikipedia.org/wiki/Dependent_typeA dependent type is a type that depends on a value.
[…]
Two common examples of dependent types are dependent functions and dependent pairs. […] A dependent pair may have a second value that depends on the first. It can be used to encode a pair of integers where the second one is greater than the first.
abstract class Nat<Me extends Nat> {
Succ<Me> next() { return new Succ<Me>(); }
}
class Zero extends Nat<Zero> { }
class Succ<Prev extends Nat> extends Nat<Succ<Prev>> { }
Note that you “pass in” the “current” value to Nat
, but the "previous" value to Succ
static <N extends Nat> void acceptsConsecutive(N first, Succ<N> second) {
System.out.println("Yup, they're consecutive allright.");
}
//...
Zero zero = new Zero();
Succ<Zero> one = zero.next();
Succ<Succ<Zero>> two = one.next();
Succ<Succ<Succ<Zero>>> three = two.next();
//acceptsConsecutive(zero, zero); //compile error
acceptsConsecutive(zero, one);
//acceptsConsecutive(zero, two); //compile error
//acceptsConsecutive(zero, three); //compile error
//acceptsConsecutive(one, zero); //compile error
//acceptsConsecutive(one, one); //compile error
acceptsConsecutive(one, two);
//acceptsConsecutive(one, three); //compile error
//acceptsConsecutive(two, zero); //compile error
//acceptsConsecutive(two, one); //compile error
//acceptsConsecutive(two, two); //compile error
acceptsConsecutive(two, three);
Erik Meijer and Peter Drayton — Static Typing Where Possible, Dynamic Typing When NeededHowever in general programmers want to express more advanced contracts about their code. For example, an invariant that the value of one variable is always less than the value of another, a precondition that an argument to a method call is within a certain range, or a postcondition that the result of a method call satisfies some condition.
Presumably this range is a subset of some larger type (e.g. only integers between 10 and 20).
Therefore, you can use subtyping to express this.
Erik Meijer and Peter Drayton — Static Typing Where Possible, Dynamic Typing When NeededHowever in general programmers want to express more advanced contracts about their code. For example, an invariant that the value of one variable is always less than the value of another, a precondition that an argument to a method call is within a certain range, or a postcondition that the result of a method call satisfies some condition.
That the output is larger than the input (or vice versa?)
abstract class Stack<E, N extends Nat<N>> {
public Stack<E, Succ<N>> push(E element) {
return new StackNode<E, N>(element, this);
}
}
class EmptyStack<E> extends Stack<E, Zero> { }
class StackNode<E, N extends Nat<N>> extends Stack<E, Succ<N>> {
private final E head;
private final Stack<E, N> next;
public StackNode(E head, Stack<E, N> next) {
this.head = head; this.next = next;
}
public Stack<E, N> pop() { return next; }
public E get() { return head; }
}
class StackOperations {
static <E, N extends Nat<N>> Stack<E, N> pop(Stack<E, Succ<N>> stack) {
assert stack instanceof StackNode;
return ((StackNode)stack).pop();
}
static <E, N extends Nat<N>> E get(Stack<E, Succ<N>> stack) {
assert stack instanceof StackNode;
return ((StackNode<E, N>)stack).get();
}
}
class Test2 {
public static void main(String[] args) {
Stack<String,Zero> zero = new EmptyStack();
//StackOperations.pop(zero); //Compile Error
//StackOperations.get(zero); //Compile Error
Stack<String,Succ<Zero>> one = zero.push("A");
StackOperations.get(one);
Stack<String,Zero> zeroAgain = StackOperations.pop(one);
//StackOperations.get(zeroAgain); //Compile Error
//StackOperations.pop(zeroAgain); //Compile Error
}
}
Erik Meijer and Peter Drayton — Static Typing Where Possible, Dynamic Typing When NeededHowever in general programmers want to express more advanced contracts about their code. For example, an invariant that the value of one variable is always less than the value of another, a precondition that an argument to a method call is within a certain range, or a postcondition that the result of a method call satisfies some condition.
That the output lies within a certain range?
Again, use subtyping to express this
Choosing a language is implicitly choosing a type system.
Succ<Succ<Succ<Succ<Succ<Succ<Succ<N>>>>>>> seven = ...
Writing dependent-type code in a Java sucks.
Erik Meijer and Peter Drayton — Static Typing Where Possible, Dynamic Typing When NeededHowever in general programmers want to express more advanced contracts about their code. For example, an invariant that the value of one variable is always less than the value of another, a precondition that an argument to a method call is within a certain range, or a postcondition that the result of a method call satisfies some condition.
Created Design by Contract in 1986-1997, trademarked in 2003-2004.
put (x: ELEMENT; key: STRING) is
require
count <= capacity
not key.empty
do
-- Implementation of method here.
ensure
contains(x)
get(key) = x
count = old count + 1
end
require
and ensuring
def put(x: Element, key: String) {
require(count <= capacity)
require(! key.empty)
//implementation of method here
} ensuring { (result) =>
result.contains(x) &&
result.get(key) == x
}
class Sum {
int add(int x, int y) {
return x + y;
}
unittest {
Sum sum = new Sum;
assert(sum.add(3,4) == 7);
assert(sum.add(-2,0) == -2);
}
}
http://dlang.org/unittest.html
def list_to_0_index(lst):
"""
Given a list, lst, say for each element the 0-index where it appears for
the first time. For example:
>>> x = [0, 1, 4, 2, 4, 1, 0, 2]
>>> list_to_0_index(x)
[0, 1, 2, 3, 2, 1, 0, 3]
>>>
"""
return [lst.index(i) for i in lst]
http://en.wikipedia.org/wiki/Doctest
/**
* @return the sum of x and y, mod Integer.MAX_VALUE.
*/
public int add(int x, int y) {
Unit tests are specific examples.
assertEquals(7, add(3, 4));
Let q(x) be a property provable about objects x of type T. Then q(y) should be provable for objects y of type S where S is a subtype of T.
In other words, think of types as sets of values, and think of "is a subtype of" as meaning "is a subset of".
Any property that is true about any instance of Foo
should also be true about any instance of Bar
, or else Bar
is not a subtype/subset of Foo
!
Lots of people get Liskov Substitution Principle wrong.
I've seen LSP-violations in blogs posts, web tutorials, and published books on OO design.
I was part of a thread in java-dev@amazon.com just one week ago, where someone got LSP wrong.
A square is a (IS-A) rectangle, Wikipedia says so!
public class Rectangle {/*...*/}
public class Square extends Rectangle {/*...*/}
public void methodExpectingRectangle(Rectangle r) {
r.setWidth(3);
r.setHeight(7);
assertThat(r.getWidth(), is(3));
assertThat(r.getHeight(), is(7));
}
methodExpectingRectangle(new Square(/*...*/));
A rectangle is just a square, with a few other fields and methods, right?
public class Square {/*...*/}
public class Rectangle extends Square {/*...*/}
public void methodExpectedSquare(Square s) {
assert "The diagonals of s bisect each other at right angles", //...
}
methodExpectedSquare(new Rectangle(/*...*/));
A mutable list is just an immutable list, but with setters, right?
public class ImmutableList { /*...*/}
public class MutableList extends ImmutableList {
public void add(E element) {/*...*/}
}
An immutable list is just a mutable list, whose setters throw UnsupportedOperationException
, right?
//see http://docs.oracle.com/javase/7/docs/api/java/util/Collection.html
(To be fair, this last one isn't an LSP violation, just a terrible API design.)
Let q(x) be a property provable about objects x of type T. Then q(y) should be provable for objects y of type S where S is a subtype of T.
Two techniques:
Preconditions are contravariant, post-conditions are covariant
In other words:
IntAdder: must be given two ints as input. Guarantees output is an int.
Example:
/**
* Instances might be mutable or immutable
*/
abstract class Data { public int get() { /*...*/ } }
/**
* New contract: these instances are guaranteed to be immutable.
*/
class ImmutableData { /* No new API defined */ }
/**
* New contract: these instances are guaranteed to be mutable.
*/
class MutableData { public void set(int newValue) { /*...*/ } }
LSP cannot be verified by static analysis!
(Proof: let the property q(x) be "always terminates", reduces to halting problem.)We (humans) must manually verify LSP.
We (humans) need to distinguish between implementation details and intended contract.
(e.g. "there is no setter" vs "the contract states that instances of this class are immutable")Write the contract in the javadoc!
interface ImmutableCircle {
float diameter();
float area();
}
interface ImmutableEllipse extends Circle {
float otherDiameter();
}
ImmutableCircle notReallyACircle = new ImmutableEllipse();
assert notReallyACircle.area() == π * (notReallyACircle.diameter() / 2) ^ 2
Wait, why is this diagram wrong?
Types are not just sets of values; they are sets of values, plus the operations that are allowed on those values.
Liskov is all about the properties of the elements, not the elements themselves. I.e. Liskov is all about the contract.