Thinking Inductively
CSI 3120
Amy Felty University of Ottawa
slides copyright 2017, 2018, 2019, 2020 Author David Walker, updated by Amy Felty permission granted to reuse these slides for non-commercial educational purposes
2
Options
A value v has type t option if it is either: – the value None, or
– a value Some v’, and v’ has type t
Options can signal there is no useful result to the computation
Example: we look up a value in a hash table using a key.
– If the key is present, return Some v where v is the associated value – If the key is not present, we return None
Slope between two points
3
a (x1, y1)
b c
type point = float * float
let slope (p1:point) (p2:point) : float =
(x2, y2)
Slope between two points
4
a (x1, y1)
b c
type point = float * float
let slope (p1:point) (p2:point) : float = let (x1,y1) = p1 in
let (x2,y2) = p2 in
deconstruct tuple
(x2, y2)
Slope between two points
5
a (x1, y1)
b c
type point = float * float
let slope (p1:point) (p2:point) : float = let (x1,y1) = p1 in
let (x2,y2) = p2 in
let xd = x2 -. x1 in
if xd != 0.0 then (y2 -. y1) /. xd
else ???
avoid divide by zero what can we return?
(x2, y2)
Slope between two points
6
a (x1, y1)
b c
type point = float * float
let slope (p1:point) (p2:point) : float option = let (x1,y1) = p1 in
let (x2,y2) = p2 in
let xd = x2 -. x1 in
if xd != 0.0 then
???
else
???
we need an option type as the result type
(x2, y2)
Slope between two points
7
a (x1, y1)
b c
type point = float * float
let slope (p1:point) (p2:point) : float option = let (x1,y1) = p1 in
let (x2,y2) = p2 in
let xd = x2 -. x1 in
if xd != 0.0 then
Some ((y2 -. y1) /. xd)
else
None
(x2, y2)
Slope between two points
8
a (x1, y1)
b c
type point = float * float
let slope (p1:point) (p2:point) : float option = let (x1,y1) = p1 in
let (x2,y2) = p2 in
let xd = x2 -. x1 in
if xd != 0.0 then
(y2 -. y1) /. xd
else
None
Has type float Can have type float option
(x2, y2)
Slope between two points
9
a (x1, y1)
b c
type point = float * float
let slope (p1:point) (p2:point) : float option = let (x1,y1) = p1 in
let (x2,y2) = p2 in
let xd = x2 -. x1 in
if xd != 0.0 then
(y2 -. y1) /. xd
else
None
Has type float
WRONG: Type mismatch
Can have type float option
(x2, y2)
Slope between two points
10
a (x1, y1)
b c
type point = float * float
let slope (p1:point) (p2:point) : float option = let (x1,y1) = p1 in
let (x2,y2) = p2 in
let xd = x2 -. x1 in
if xd != 0.0 then
(y2 -. y1) /. xd
else
None
doubly WRONG: result does not match declared result
Has type float
(x2, y2)
Remember the typing rule for if
11
if e1 : bool
and e2 : t and e3 : t (for some type t) then if e1 then e2 else e3 : t
Returning an optional value from an if statement:
if … then
None : t option
else
Some ( … ) : t option
12
How do we use an option?
slope : point -> point -> float option
returns a float option
13
How do we use an option?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit =
14
How do we use an option?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit = slope p1 p2
returns a float option;
to print we must discover if it is None or Some
15
How do we use an option?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit = match slope p1 p2 with
How do we use an option?
16
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit = match slope p1 p2 with
Some s ->
| None ->
There are two possibilities
Vertical bar separates possibilities
17
How do we use an option?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit = match slope p1 p2 with
Some s ->
| None ->
The “Some s” pattern includes the variable s The object between | and -> is called a pattern
18
How do we use an option?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit = match slope p1 p2 with
Some s ->
print_string (“Slope: ” ^ string_of_float s)
| None ->
print_string “Vertical line.\n”
19
•
Writing Functions Over Typed Data
Steps to writing functions over typed data:
1. Write down the function and argument names
2. Write down argument and result types
3. Write down some examples (in a comment)
4. Deconstruct input data structures
5. Build new output values
6. Clean up by identifying repeated patterns
For option types:
when the input has type t option, deconstruct with:
•
when the output has type t option, construct with:
match … with
| None -> …
| Some s -> …
Some (…)
None
MORE PATTERN MATCHING
20
21
Recall the Distance Function
type point = float * float
let distance (p1:point) (p2:point) : float = let square x = x *. x in
let (x1,y1) = p1 in
let (x2,y2) = p2 in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
Recall the Distance Function
22
type point = float * float
let distance (p1:point) (p2:point) : float = let square x = x *. x in
let (x1,y1) = p1 in
let (x2,y2) = p2 in
sqrt (square (x2 -. x1) +. square (y2 -. y1)) ;;
(x2, y2) is an example of a pattern – a pattern for tuples.
So let declarations can contain patterns just like match statements
The difference is that a match allows you to consider multiple different data shapes
Recall the Distance Function
23
type point = float * float
let distance (p1:point) (p2:point) : float = let square x = x *. x in
match p1 with
| (x1,y1) ->
;;
let (x2,y2) = p2 in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
There is only 1 possibility when matching a pair
Recall the Distance Function
24
type point = float * float
let distance (p1:point) (p2:point) : float = let square x = x *. x in
match p1 with
| (x1,y1) ->
match p2 with
| (x2,y2) ->
;;
sqrt (square (x2 -. x1) +. square (y2 -. y1))
We can nest one match expression inside another.
(We can nest any expression inside any other, if the expressions have the right types)
Complex Patterns
we built a pair of pairs
25
type point = float * float
let distance (p1:point) (p2:point) : float = let square x = x *. x in
match (p1, p2) with
| ((x1,y1), (x2, y2)) ->
sqrt (square (x2 -. x1) +. square (y2 -. y1)) ;;
Pattern for a pair of pairs: ((variable, variable), (variable, variable)) All the variable names in the pattern must be different.
Complex Patterns
26
type point = float * float
let distance (p1:point) (p2:point) : float = let square x = x *. x in
match (p1, p2) with
| ((x1,y1), (x2, y2)) ->
sqrt (square (x2 -. x1) +. square (y2 -. y1)) ;;
A pattern must be consistent with the type of the expression in between match … with
For example, x1 : float, x2 : float, p1 : float * float
27
Pattern-matching in function parameters
type point = float * float
let distance ((x1,y1):point) ((x2,y2):point) : float = let square x = x *. x in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
;;
Function parameters are patterns too!
What’s the best style?
28
let distance (p1:point) (p2:point) : float = let square x = x *. x in
let (x1,y1) = p1 in
let (x2,y2) = p2 in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
let distance ((x1,y1):point) ((x2,y2):point) : float = let square x = x *. x in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
Either of these is reasonably clear and compact.
Code with unnecessary nested matches/lets is particularly ugly to read.
29
What’s the best style?
let distance (x1,y1) (x2,y2) =
let square x = x *. x in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
Note that the types for tuples plus the tuple patterns are a little ugly/verbose, and they can be inferred from the operators used such as `+.’ … but for now in class, use the explicit type annotations.
30
Other Patterns
type point = float * float
(* returns a nearby point in the graph if one exists *)
nearby : graph -> point -> point option
let printer (g:graph) (p:point) : unit =
match nearby g p with
| None -> print_string “could not find one\n” | Some (x,y) ->
print_float x; print_string “, “; print_float y; print_newline();
;;
Other Patterns • Constant values can be used as patterns
31
let small_prime (n:int) : bool = match n with
| 2 -> true
| 3 -> true
| 5 -> true
| _ -> false ;;
let iffy (b:bool) : int = match b with
| true -> 0
| false -> 1
;;
the underscore pattern matches anything
it is the “don’t care” pattern
INDUCTIVE THINKING
32
33
Inductive Programming and Proving An inductive data type T is a data type defined by:
– a collection of base cases • that don’t refer to T
– a collection of inductive cases that build new values of type T from pre-existing data of type T
• the pre-existing data is guaranteed to be smaller than the new values Programming principle:
– solve programming problem for base cases
– solve programming problem for inductive cases by calling function
recursively (inductively) on smaller data value Proving principle:
– prove program satisfies property P for base cases
– prove inductive cases satisfy property P assuming inductive calls on smaller data values satisfy property P
LISTS: AN INDUCTIVE DATA TYPE
34
Lists are Recursive Data
• In OCaml, a list value is:
– [ ] (the empty list)
– v :: vs (a value v followed by a shorter list of values vs)
35
Inductive Case
Base Case
36
Lists are Inductive Data
• In OCaml, a list value is:
– [ ] (the empty list)
– v :: vs (a value v followed by a shorter list of values vs)
• An example:
– 2::3::5::[]hastypeintlist
– isthesameas: 2::(3::(5::[])) – “::” is called “cons”
• An alternative syntax (“syntactic sugar” for lists):
– [2; 3; 5]
– Butthisisjustashorthandfor2::3::5::[]. Ifyoueverget confused fall back on the 2 basic constructors: :: and []
Typing Lists • Typing rules for lists:
(1) [ ] may have any list type t list
(2)
then (e1 :: e2) : t list
ife1:tand e2:tlist
37
Typing Lists • Typing rules for lists:
(1) [ ] may have any list type t list
(2)
then (e1 :: e2) : t list
ife1:tand e2:tlist • More examples:
(1 + 2) :: (3 + 4) :: [ ] (2::[])::(5::6 ::[])::[] [ [2]; [5; 6] ]
: ?? :?? : ??
38
Typing Lists • Typing rules for lists:
(1) [ ] may have any list type t list
(2)
then (e1 :: e2) : t list
ife1:tand e2:tlist • More examples:
(1 + 2) :: (3 + 4) :: [ ] : int list
(2::[])::(5::6 ::[])::[] :(intlist)list orjust intlistlist
[ [2]; [5; 6] ] : int list list
(Remember that the 3rd example is an abbreviation for the 2nd)
39
40
Another Example
• What type does this have?
[ 2 ] :: [ 3 ]
• What type does this have?
[ 2 ] :: [ 3 ]
int list
int list
Another Example
41
# [2] :: [3];;
Error: This expression has type int but an
#
expression was expected of type int list
• What type does this have?
[ 2 ] :: [ 3 ]
int list
int list
42
Another Example
• What is a simple fix that makes the expression type check?
• What type does this have?
[ 2 ] :: [ 3 ]
int list
int list
43
Another Example
• What is a simple fix that makes the expression type check? Either: 2 :: [3] :intlist
Or: [ 2 ] :: [ [ 3 ] ] : int list list
44
Analyzing Lists
• Just like options, there are two possibilities when deconstructing lists. Hence we use a match with two branches
(* return Some v, if v is the first list element; return None, if the list is empty *)
let head (xs : int list) : int option =
Analyzing Lists
• Just like options, there are two possibilities when deconstructing lists. Hence we use a match with two branches
45
(* return Some v, if v is the first list element; return None, if the list is empty *)
let head (xs : int list) : int option = match xs with
| [] ->
| hd :: _ ->
we don’t care about the contents of the tail of the list so we use the underscore
46
Analyzing Lists
• Just like options, there are two possibilities when deconstructing lists. Hence we use a match with two branches
(* return Some v, if v is the first list element; return None, if the list is empty *)
let head (xs : int list) : int option = match xs with
| [] -> None
| hd :: _ -> Some hd
• This function isn’t recursive — we only extracted a small , fixed amount of information from the list — the first element
47
A more interesting example
(* Given a list of pairs of integers, produce the list of products of the pairs
prods [(2,3); (4,7); (5,2)] == [6; 28; 10] *)
48
A more interesting example
(* Given a list of pairs of integers, produce the list of products of the pairs
prods [(2,3); (4,7); (5,2)] == [6; 28; 10] *)
let rec prods (xs : (int * int) list) : int list =
49
A more interesting example
(* Given a list of pairs of integers, produce the list of products of the pairs
prods [(2,3); (4,7); (5,2)] == [6; 28; 10] *)
let rec prods (xs : (int * int) list) : int list = match xs with
| [] ->
| (x,y) :: tl ->
50
A more interesting example
(* Given a list of pairs of integers, produce the list of products of the pairs
prods [(2,3); (4,7); (5,2)] == [6; 28; 10] *)
let rec prods (xs : (int * int) list) : int list = match xs with
| [] -> []
| (x,y) :: tl ->
A more interesting example
51
(* Given a list of pairs of integers, produce the list of products of the pairs
prods [(2,3); (4,7); (5,2)] == [6; 28; 10] *)
let rec prods (xs : (int * int) list) : int list = match xs with
| [] -> []
| (x,y) :: tl -> ?? :: ??
the result type is int list, so we can speculate that we should create a list
52
A more interesting example
(* Given a list of pairs of integers, produce the list of products of the pairs
prods [(2,3); (4,7); (5,2)] == [6; 28; 10] *)
let rec prods (xs : (int * int) list) : int list = match xs with
| [] -> []
| (x,y) :: tl -> (x * y) :: ??
the first element is the product
A more interesting example
53
(* Given a list of pairs of integers, produce the list of products of the pairs
prods [(2,3); (4,7); (5,2)] == [6; 28; 10] *)
let rec prods (xs : (int * int) list) : int list = match xs with
| [] -> []
| (x,y) :: tl -> (x * y) :: ??
to complete the job, we must compute the products for the rest of the list
54
A more interesting example
(* Given a list of pairs of integers, produce the list of products of the pairs
prods [(2,3); (4,7); (5,2)] == [6; 28; 10] *)
let rec prods (xs : (int * int) list) : int list = match xs with
| [] -> []
| (x,y) :: tl -> (x * y) :: prods tl
Three Parts to Constructing a Function
(1) Think about how to break down the input into cases:
55
let rec prods (xs : (int*int) list) : int list =
match xs with
| [] -> …
| (x,y) :: tl -> …
This assumption is called the Induction Hypothesis. It can be used it to prove your program correct.
(2) Assume the recursive call on smaller data is correct.
(3) Use the result of the recursive call to build correct answer.
let rec prods (xs : (int*int) list) : int list = …
| (x,y) :: tl -> … prods tl …
56
Another example: zip
(* Given two lists of integers,
return None if the lists are different lengths otherwise stitch the lists together to create
Some of a list of pairs
zip [2; 3] [4; 5] == Some [(2,4); (3,5)] zip [5; 3] [4] == None
zip [4; 5; 6] [8; 9; 10; 11; 12] == None
*)
57
Another example: zip
let rec zip (xs : int list) (ys : int list) : (int * int) list option =
58
Another example: zip
let rec zip (xs : int list) (ys : int list) : (int * int) list option =
match (xs, ys) with
59
Another example: zip
let rec zip (xs : int list) (ys : int list) : (int * int) list option =
match (xs, ys) with | ([], []) ->
| ([], y::ys’) ->
| (x::xs’, []) ->
| (x::xs’, y::ys’) ->
60
Another example: zip
let rec zip (xs : int list) (ys : int list) : (int * int) list option =
match (xs, ys) with
| ([], []) -> Some [] | ([], y::ys’) ->
| (x::xs’, []) ->
| (x::xs’, y::ys’) ->
61
Another example: zip
let rec zip (xs : int list) (ys : int list) : (int * int) list option =
match (xs, ys) with
| ([], []) -> Some [] | ([], y::ys’) -> None | (x::xs’, []) -> None | (x::xs’, y::ys’) ->
Another example: zip
62
let rec zip (xs : int list) (ys : int list) : (int * int) list option =
match (xs, ys) with
| ([], []) -> Some []
| ([], y::ys’) -> None
| (x::xs’, []) -> None
| (x::xs’, y::ys’) -> (x, y) :: zip xs’ ys’
is this ok?
Another example: zip
63
let rec zip (xs : int list) (ys : int list) : (int * int) list option =
match (xs, ys) with
| ([], []) -> Some []
| ([], y::ys’) -> None
| (x::xs’, []) -> None
| (x::xs’, y::ys’) -> (x, y) :: zip xs’ ys’
No! zip returns a list option, not a list!
We need to match it and decide if it is Some or None.
Another example: zip
64
let rec zip (xs : int list) (ys : int list) : (int * int) list option =
match (xs, ys) with
| ([], []) -> Some [] | ([], y::ys’) -> None | (x::xs’, []) -> None | (x::xs’, y::ys’) ->
(match zip xs’ ys’ with None -> None
| Some zs -> (x,y) :: zs)
Is this ok?
65
Another example: zip
let rec zip (xs : int list) (ys : int list) : (int * int) list option =
match (xs, ys) with
| ([], []) -> Some [] | ([], y::ys’) -> None | (x::xs’, []) -> None | (x::xs’, y::ys’) ->
(match zip xs’ ys’ with None -> None
| Some zs -> Some ((x,y) :: zs))
Another example: zip
66
let rec zip (xs : int list) (ys : int list) : (int * int) list option =
match (xs, ys) with
| ([], []) -> Some [] | (x::xs’, y::ys’) ->
(match zip xs’ ys’ with None -> None
| Some zs -> Some ((x,y) :: zs)) | (_, _) -> None
Clean up.
Reorganize the cases.
Pattern matching proceeds in order.
67
A bad list example
let rec sum (xs : int list) : int = match xs with
| hd::tl -> hd + sum tl
A bad list example
68
let rec sum (xs : int list) : int = match xs with
| hd::tl -> hd + sum tl
# Characters 39-78: ..match xs with
hd :: tl -> hd + sum tl..
Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: [] val sum : int list -> int =
INSERTION SORT
69
70
Recall Insertion Sort
• At any point during the insertion sort:
– some initial segment of the array will be sorted
– the rest of the array will be in the same (unsorted) order as it was originally
-5
-2
3
-4
10
6
7
sorted
unsorted
71
Recall Insertion Sort
• At any point during the insertion sort:
– some initial segment of the array will be sorted
– the rest of the array will be in the same (unsorted) order as it was originally
-5
-2
3
-4
10
6
7
sorted
unsorted
• At each step, take the next item in the array and insert it in order into the sorted portion of the list
-5
-4
-2
3
10
6
7
sorted
unsorted
Insertion Sort With Lists
• The algorithm is similar, except instead of one array, we will
maintain two lists, a sorted list and an unsorted list
list 1:
sorted
list 2:
72
-5
-2
3
-4
10
6
7
• We’ll factor the algorithm:
– a function to insert into a sorted list
– a sorting function that repeatedly inserts
unsorted
73
Insert
(* insert x in to sorted list xs *)
let rec insert (x : int) (xs : int list) : int list =
74
Insert
(* insert x in to sorted list xs *)
let rec insert (x : int) (xs : int list) : int list =
match xs with | [] ->
| hd :: tl ->
a familiar pattern:
analyze the list by cases
75
Insert
(* insert x in to sorted list xs *)
let rec insert (x : int) (xs : int list) : int list = match xs with
| [] -> [x]
| hd :: tl ->
insert x into the empty list
76
Insert
(* insert x in to sorted list xs *)
let rec insert (x : int) (xs : int list) : int list = match xs with
| [] -> [x]
| hd :: tl ->
if hd < x then
hd :: insert x tl
build a new list with:
• hd at the beginning
• the result of inserting x in to
the tail of the list afterwards
77
Insert
(* insert x in to sorted list xs *)
let rec insert (x : int) (xs : int list) : int list = match xs with
| [] -> [x]
| hd :: tl ->
if hd < x then
hd :: insert x tl
else
x :: xs
put x on the front of the list, the rest of the list follows
78
Insertion Sort
type il = int list insert : int -> il -> il
(* insertion sort *)
let rec insert_sort (xs : il) : il =
79
Insertion Sort
type il = int list insert : int -> il -> il
(* insertion sort *)
let rec insert_sort (xs : il) : il =
let rec aux (sorted : il) (unsorted : il) : il =
in
80
Insertion Sort
type il = int list insert : int -> il -> il
(* insertion sort *)
let rec insert_sort (xs : il) : il =
let rec aux (sorted : il) (unsorted : il) : il =
in
aux [] xs
81
Insertion Sort
type il = int list insert : int -> il -> il
(* insertion sort *)
let rec insert_sort (xs : il) : il =
let rec aux (sorted : il) (unsorted : il) : il =
match unsorted with | [] ->
| hd :: tl ->
in
aux [] xs
82
Insertion Sort
type il = int list insert : int -> il -> il
(* insertion sort *)
let rec insert_sort (xs : il) : il =
let rec aux (sorted : il) (unsorted : il) : il = match unsorted with
| [] -> sorted
| hd :: tl -> aux (insert hd sorted) tl
in
aux [] xs
A SHORT JAVA RANT
83
Definition and Use of Java Pairs
84
public class Pair {
public int x;
public int y;
public Pair (int a, int b) {
x = a;
y = b; }
}
public class User {
public Pair swap (Pair p1) {
Pair p2 =
new Pair(p1.y, p1.x);
return p2;
} }
What could go wrong?
A Paucity of Types
85
public class Pair {
public int x;
public int y;
public Pair (int a, int b) {
x = a;
y = b; }
}
public class User {
public Pair swap (Pair p1) {
Pair p2 =
new Pair(p1.y, p1.x);
return p2;
} }
The input p1 to swap may be null and we forgot to check. Java has no way to define a pair data structure that is just a pair.
How many students in the class have seen an accidental null pointer exception thrown in their Java code?
From Java Pairs to OCaml Pairs
In OCaml, if a pair may be null it is a pair option:
type java_pair = (int * int) option
86
From Java Pairs to OCaml Pairs
In OCaml, if a pair may be null it is a pair option:
And if you write code like this:
87
type java_pair = (int * int) option
let swap_java_pair (p:java_pair) : java_pair =
let (x,y) = p in
(y,x)
88
From Java Pairs to OCaml Pairs
In OCaml, if a pair may be null it is a pair option:
And if you write code like this:
type java_pair = (int * int) option
let swap_java_pair (p:java_pair) : java_pair =
let (x,y) = p in
(y,x)
You get a helpful error message like this:
# … Characters 91-92:
let (x,y) = p in (y,x);;
^
Error: This expression has type java_pair = (int * int) option
but an expression was expected of type ‘a * ‘b
From Java Pairs to OCaml Pairs
type java_pair = (int * int) option
And what if you were up late trying to finish your assignment and you accidentally wrote the following statement?
89
let swap_java_pair (p:java_pair) : java_pair =
match p with
| Some (x,y) -> Some (y,x)
90
From Java Pairs to OCaml Pairs
type java_pair = (int * int) option
And what if you were up late trying to finish your assignment and you accidentally wrote the following statement?
let swap_java_pair (p:java_pair) : java_pair =
match p with
| Some (x,y) -> Some (y,x)
OCaml to the rescue!
..match p with
| Some (x,y) -> Some (y,x)
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
None
91
From Java Pairs to OCaml Pairs
type java_pair = (int * int) option
And what if you were up late trying to finish your assignment and you accidentally wrote the following statement?
let swap_java_pair (p:java_pair) : java_pair =
match p with
| Some (x,y) -> Some (y,x)
An easy fix!
let swap_java_pair (p:java_pair) : java_pair =
match p with
| None -> None
| Some (x,y) -> Some (y,x)
92
From Java Pairs to OCaml Pairs
Moreover, your pairs are probably almost never null!
Defensive programming & always checking for null can be annoying.
93
From Java Pairs to OCaml Pairs
There just isn’t always some “good thing” for a function to do when it receives a bad input, like a null pointer
In OCaml, all these issues disappear when you use the proper type for a pair and that type contains no “extra junk”
type pair = int * int
Once you know OCaml, it is hard to write swap incorrectly Your bullet-proof code is much simpler than in Java.
let swap (p:pair) : pair =
let (x,y) = p in (y,x)
94
Summary of Java Pair Rant
Java has a paucity of types
– Thereisnotypetodescribejustthepairs
– Thereisnotypetodescribejustthetriples
– Thereisnotypetodescribethepairsofpairs – Thereisnotype…
OCaml has many more types
– useoptionwhenthingsmaybenull
– donotuseoptionwhenthingsarenotnull
– OCamltypesdescribedatastructuresmoreprecisely
• programmershavefewercasestoworryabout
• entireclassesoferrorsjustgoaway
• typecheckingandpatternanalysishelppreventprogrammersfrom ever forgetting about a case
95
Summary of Java Pair Rant
Java has a paucity of types
– Thereisnotypetodescribejustthepairs
– Thereisnotypetodescribejustthetriples
– Thereisnotypetodescribethepairsofpairs – Thereisnotype…
OCaml has many more types
SCORE: OCAML 1, JAVA 0
– useoptionwhenthingsmaybenull
– donotuseoptionwhenthingsarenotnull
– ocamltypesdescribedatastructuresmoreprecisely
• programmershavefewercasestoworryabout
• entireclassesoferrorsjustgoaway
• typecheckingandpatternanalysishelppreventprogrammersfrom ever forgetting about a case
96
C, C++ Rant
Java has a paucity of types
– but at least when you forget something,
it throws an exception instead of silently going off the rails!
If you forget to check for null pointer in a C program,
– no type-check error at compile time
– no exception at run time
– it might crash right away (that would be best), or
– it might permit a buffer-overrun (or similar) vulnerability
97
Summary of C, C++ rant
Java has a paucity of types
– but at least when you forget something,
it throws an exception instead of silently going off the trolley!
If you forget to check for null pointer in a C program,
SCORE:
– no type-check error at compile time
– no excep O
C
A
M
L
1
,
JAVA 0, C -1
tio
n
at
run
ti
m
e
– it might crash right away (that would be best), or
– it might permit a buffer-overrun (or similar) vulnerability – so the hackers pwn you!