XKCD
Thinking Inductively
CSI 3120
slides copyright 2017, 2018, 2019, 2020
Author David Walker, updated by Amy Felty
permission granted to reuse these slides for non-commercial educational purposes
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
2
Slope between two points
type point = float * float
let slope (p1:point) (p2:point) : float =
(x1, y1)
(x2, y2)
a
b
c
3
Slope between two points
type point = float * float
let slope (p1:point) (p2:point) : float =
let (x1,y1) = p1 in
let (x2,y2) = p2 in
(x1, y1)
(x2, y2)
a
b
c
deconstruct tuple
4
Slope between two points
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
???
(x1, y1)
(x2, y2)
a
b
c
what can we return?
avoid divide by zero
5
Slope between two points
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
???
(x1, y1)
(x2, y2)
a
b
c
we need an option
type as the result type
6
Slope between two points
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
(x1, y1)
(x2, y2)
a
b
c
7
Slope between two points
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
(x1, y1)
(x2, y2)
a
b
c
Has type float
Can have type float option
8
Slope between two points
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
(x1, y1)
(x2, y2)
a
b
c
Has type float
Can have type float option WRONG: Type mismatch
9
Slope between two points
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
(x1, y1)
(x2, y2)
a
b
c
Has type float
doubly WRONG:
result does not
match declared result
10
Remember the typing rule for if
Returning an optional value from an if statement:
if … then
None : t option
else
Some ( … ) : t option
11
if e1 : bool
and e2 : t and e3 : t (for some type t)
then if e1 then e2 else e3 : t
How do we use an option?
slope : point -> point -> float option
returns a float option
12
How do we use an option?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit =
13
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
14
How do we use an option?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit =
match slope p1 p2 with
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
Some s ->
| None ->
There are two possibilities
Vertical bar separates possibilities
16
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 object between | and -> is called a pattern
The “Some s” pattern includes the variable s
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 ->
print_string (“Slope: ” ^ string_of_float s)
| None ->
print_string “Vertical line.\n”
18
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:
match … with
| None -> …
| Some s -> …
when the input has type t option,
deconstruct with:
when the output has type t option,
construct with:
Some (…) None
19
MORE PATTERN MATCHING
20
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))
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))
;;
(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
22
Recall the Distance Function
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
23
Recall the Distance Function
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)
24
Complex Patterns
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.
we built a pair of pairs
25
Complex Patterns
A pattern must be consistent with the type of the expression
in between match … with
For example, x1 : float, x2 : float, p1 : float * float
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))
;;
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!
27
What’s the best style?
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))
Either of these is reasonably clear and compact.
Code with unnecessary nested matches/lets is particularly ugly to read.
let distance ((x1,y1):point) ((x2,y2):point) : float =
let square x = x *. x in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
28
What’s the best style?
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.
let distance (x1,y1) (x2,y2) =
let square x = x *. x in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
29
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();
;;
33
Other Patterns
• Constant values can be used as patterns
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
34
INDUCTIVE THINKING
35
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
36
LISTS: AN INDUCTIVE DATA TYPE
37
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)
Base Case
Inductive
Case
38
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 :: [ ] has type int list
– is the same as: 2 :: (3 :: (5 :: [ ]))
– “::” is called “cons”
• An alternative syntax (“syntactic sugar” for lists):
– [2; 3; 5]
– But this is just a shorthand for 2 :: 3 :: 5 :: []. If you ever get
confused fall back on the 2 basic constructors: :: and []
39
Typing Lists
• Typing rules for lists:
[ ] may have any list type t list
if e1 : t and e2 : t list
then (e1 :: e2) : t list
(1)
(2)
40
Typing Lists
• Typing rules for lists:
• More examples:
(1 + 2) :: (3 + 4) :: [ ] : ??
(2 :: [ ]) :: (5 :: 6 :: [ ]) :: [ ] : ??
[ [2]; [5; 6] ] : ??
[ ] may have any list type t list
if e1 : t and e2 : t list
then (e1 :: e2) : t list
(1)
(2)
41
Typing Lists
• Typing rules for lists:
• More examples:
(1 + 2) :: (3 + 4) :: [ ] : int list
(2 :: [ ]) :: (5 :: 6 :: [ ]) :: [ ] : (int list) list or just int list list
[ [2]; [5; 6] ] : int list list
(Remember that the 3rd example is an abbreviation for the 2nd)
[ ] may have any list type t list
if e1 : t and e2 : t list
then (e1 :: e2) : t list
(1)
(2)
42
Another Example
• What type does this have?
[ 2 ] :: [ 3 ]
43
Another Example
# [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
44
Another Example
• What type does this have?
[ 2 ] :: [ 3 ]
• What is a simple fix that makes the expression type check?
int list int list
45
Another Example
• What type does this have?
[ 2 ] :: [ 3 ]
• What is a simple fix that makes the expression type check?
Either: 2 :: [ 3 ] : int list
Or: [ 2 ] :: [ [ 3 ] ] : int list list
int list int list
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 =
47
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
| [] ->
| hd :: _ ->
we don’t care about the contents of the
tail of the list so we use the underscore
48
Analyzing Lists
• Just like options, there are two possibilities when
deconstructing lists. Hence we use a match with two branches
• This function isn’t recursive — we only extracted a small , fixed
amount of information from the list — the first element
(* 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
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]
*)
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 =
51
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 ->
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 ->
53
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 -> ?? :: ??
the result type is int list, so we can speculate
that we should create a 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) :: ??
the first element is the product
55
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) :: ??
to complete the job, we must compute
the products for the rest of the list
56
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
57
Three Parts to Constructing a Function
let rec prods (xs : (int*int) list) : int list =
match xs with
| [] -> …
| (x,y) :: tl -> …
(1) Think about how to break down the input into cases:
let rec prods (xs : (int*int) list) : int list =
…
| (x,y) :: tl -> … prods tl …
(2) Assume the recursive call on smaller data is correct.
(3) Use the result of the recursive call to build correct answer.
59
Three Parts to Constructing a Function
let rec prods (xs : (int*int) list) : int list =
match xs with
| [] -> …
| (x,y) :: tl -> …
(1) Think about how to break down the input into cases:
let rec prods (xs : (int*int) list) : int list =
…
| (x,y) :: tl -> … prods tl …
(2) Assume the recursive call on smaller data is correct.
(3) Use the result of the recursive call to build correct answer.
This assumption is called the
Induction Hypothesis. It can
be used it to prove your
program correct.
60
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
*)
61
Another example: zip
let rec zip (xs : int list) (ys : int list)
: (int * int) list option =
62
Another example: zip
let rec zip (xs : int list) (ys : int list)
: (int * int) list option =
match (xs, ys) with
63
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’) ->
64
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’) ->
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’) ->
66
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’) -> (x, y) :: zip xs’ ys’
is this ok?
67
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’) -> (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.
68
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 -> (x,y) :: zs)
Is this ok?
69
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))
70
Another example: zip
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.
71
A bad list example
let rec sum (xs : int list) : int =
match xs with
| hd::tl -> hd + sum tl
72
A bad list example
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 =
73
INSERTION SORT
74
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
75
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
• At each step, take the next item in the array and insert it in
order into the sorted portion of the list
-5 -2 3 -4 10 6 7
sorted unsorted
-5 -4 -2 3 10 6 7
sorted unsorted
76
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
• We’ll factor the algorithm:
– a function to insert into a sorted list
– a sorting function that repeatedly inserts
-5 -2 3 -4 10 6 7
sorted unsorted
list 1: list 2:
77
Insert
(* insert x in to sorted list xs *)
let rec insert (x : int) (xs : int list) : int list =
78
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
79
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
80
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 81 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 82 Insertion Sort type il = int list insert : int -> il -> il
(* insertion sort *)
let rec insert_sort (xs : il) : il =
83
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
84
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
85
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
86
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
87
A SHORT JAVA RANT
88
Definition and Use of Java Pairs
What could go wrong?
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;
}
}
89
A Paucity of Types
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.
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;
}
}
90
How many students in the class have seen an accidental null pointer
exception thrown in their Java code?
From Java Pairs to OCaml Pairs
type java_pair = (int * int) option
In OCaml, if a pair may be null it is a pair option:
91
From Java Pairs to OCaml Pairs
let swap_java_pair (p:java_pair) : java_pair =
let (x,y) = p in
(y,x)
type java_pair = (int * int) option
In OCaml, if a pair may be null it is a pair option:
And if you write code like this:
92
From Java Pairs to OCaml Pairs
let swap_java_pair (p:java_pair) : java_pair =
let (x,y) = p in
(y,x)
type java_pair = (int * int) option
In OCaml, if a pair may be null it is a pair option:
And if you write code 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
You get a helpful error message like this:
93
From Java Pairs to OCaml Pairs
type java_pair = (int * int) option
let swap_java_pair (p:java_pair) : java_pair =
match p with
| Some (x,y) -> Some (y,x)
And what if you were up late trying to finish your
assignment and you accidentally wrote the
following statement?
94
From Java Pairs to OCaml Pairs
type java_pair = (int * int) option
let swap_java_pair (p:java_pair) : java_pair =
match p with
| Some (x,y) -> Some (y,x)
And what if you were up late trying to finish your
assignment and you accidentally wrote the
following statement?
..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
OCaml to the rescue!
95
From Java Pairs to OCaml Pairs
type java_pair = (int * int) option
let swap_java_pair (p:java_pair) : java_pair =
match p with
| Some (x,y) -> Some (y,x)
And what if you were up late trying to finish your
assignment and you accidentally wrote the
following statement?
An easy fix!
let swap_java_pair (p:java_pair) : java_pair =
match p with
| None -> None
| Some (x,y) -> Some (y,x)
96
From Java Pairs to OCaml Pairs
Moreover, your pairs are probably almost never null!
Defensive programming & always checking for null can be
annoying.
97
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”
Once you know OCaml, it is hard to write swap incorrectly
Your bullet-proof code is much simpler than in Java.
type pair = int * int
let swap (p:pair) : pair =
let (x,y) = p in (y,x)
98
Summary of Java Pair Rant
Java has a paucity of types
– There is no type to describe just the pairs
– There is no type to describe just the triples
– There is no type to describe the pairs of pairs
– There is no type …
OCaml has many more types
– use option when things may be null
– do not use option when things are not null
– OCaml types describe data structures more precisely
• programmers have fewer cases to worry about
• entire classes of errors just go away
• type checking and pattern analysis help prevent programmers from
ever forgetting about a case
99
Summary of Java Pair Rant
Java has a paucity of types
– There is no type to describe just the pairs
– There is no type to describe just the triples
– There is no type to describe the pairs of pairs
– There is no type …
OCaml has many more types
– use option when things may be null
– do not use option when things are not null
– ocaml types describe data structures more precisely
• programmers have fewer cases to worry about
• entire classes of errors just go away
• type checking and pattern analysis help prevent programmers from
ever forgetting about a case
SCORE: OCAML 1, JAVA 0
100
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
101
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,
– 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
– so the hackers pwn you!
Summary of C, C++ rant
SCORE:
OCAML 1, JAVA 0, C -1
102