CS 320 : Functional
Programming in Ocaml
(based on slides from David Walker, Princeton, Lukasz Ziarek, Buffalo and myself.)
Marco Gaboardi MSC 116 gaboardi@bu.edu
Announcements
• We are setting up GradeScope this week … and before the deadline of the first programming assignment.
• First programming assignment is due Friday, February 7, no later than 11:59 pm.
In the previous classes…
Type Soundness
“Well typed programs do not go wrong” Programming languages with this property have
sound type systems. They are called safe languages. Safe languages are generally immune to buffer overrun
vulnerabiliRes, uniniRalized pointer vulnerabiliRes, etc., etc. (but not immune to all bugs!)
Safe languages: ML, Java, Python, … Unsafe languages: C, C++, Pascal
38
Another Example
subsDtute 2 for x
29
let x = 2 in
let y = x + x in y*x
Moral: Let operates by subs&tu&ng computed values for variables
let y = 2 + 2 in y*2
–>
–>
subsDtute 4 for y
let y = 4 in y*2
4*2
8
–> –>
let keyword
Defining funcDons
36
let add_one (x:int) : int = 1 + x
funcDon name
type of result
type of argument
expression
that computes value produced by funcDon
argument name
Note: recursive funcDons with begin with “let rec”
45
Rule for type-checking funcDons
General Rule:
A -> B -> C
same as:
A -> (B -> C)
If a funcDon f : T1 -> T2 and an argument e : T1 then f e : T2
Example:
add : int -> (int -> int)
3 + 4 : int
add (3 + 4) : int -> int
Tuples
• To use a tuple, we extract its components
• General case:
53
let (id1, id2, …, idn) = e1 in e2
• An example:
let (x,y) = (2,4) in x + x + y
Unit • Unit is the tuple with zero fields!
() : unit
• the unit value is written with an pair of parens
• there are no other values with this type!
Unit • Unit is the tuple with zero fields!
() : unit
• the unit value is written with an pair of parens
• there are no other values with this type!
• Why is the unit type and value useful?
• Every expression has a type:
(print_string “hello world\n”) : ???
77
Unit • Unit is the tuple with zero fields!
() : unit
• the unit value is wriZen with an pair of parens
• there are no other values with this type!
• Why is the unit type and value useful?
• Every expression has a type:
(print_string “hello world\n”) : unit
• Expressions executed for their effect return the unit value
20
•
Wri,ng Func,ons Over Typed Data
Steps to wri,ng func,ons over typed data:
1. Write down the func,on 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 iden,fying repeated paLerns
•
For op,on types:
when the input has type t op,on, deconstruct with:
when the output has type t op,on, construct with:
match … with
| None -> …
| Some s -> …
Some (…)
None
Learning Goals for today
• Optiontypes
• I/OinOCaml
• Inductivedatatypes Lists
Options
3
Op,ons
A value v has type t op,on if it is either: – the value None, or
– a value Some v’, and v’ has type t
Op,ons can signal there is no useful result to the computa,on
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
4
a (x1, y1)
b c
type point = float * float
let slope (p1:point) (p2:point) : float =
(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
deconstruct tuple
(x2, y2)
Slope between two points
6
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
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
???
else
???
we need an op,on type as the result type
(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 Can have type float op,on
(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
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
Some ((y2 -. y1) /. xd)
else
None
(x2, y2)
13
How do we use an op,on?
slope : point -> point -> float option
returns a float op,on
14
How do we use an op,on?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit =
15
How do we use an op,on?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit =
slope p1 p2
returns a float op,on;
to print we must discover if it is None or Some
16
How do we use an op,on?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit =
match slope p1 p2 with
How do we use an op,on?
17
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit =
match slope p1 p2 with
Some s ->
| None ->
There are two possibili,es
Ver,cal bar separates possibili,es
18
How do we use an op,on?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit =
match slope p1 p2 with
Some s ->
| None ->
The “Some s” paLern includes the variable s The object between | and -> is called a paLern
19
How do we use an op,on?
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”
20
•
Wri,ng Func,ons Over Typed Data
Steps to wri,ng func,ons over typed data:
1. Write down the func,on 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 iden,fying repeated paLerns
•
For op,on types:
when the input has type t op,on, deconstruct with:
when the output has type t op,on, construct with:
match … with
| None -> …
| Some s -> …
Some (…)
None
TopHat Q1-Q5
Input/Output on files in OCaml
Input and Output Channels
The normal way of opening a file in OCaml returns a channel. There are two kinds of channels:
• channels that write to a file: type out_channel
• channels that read from a file: type in_channel
Four operations that will be useful are:
• Open input file: open_in: string -> in_channel
• Open out file: open_out: string -> out_channel
• Close input file: close_in: in_channel -> unit
• Close input file: close_out: out_channel -> unit
If you want to use a channel, you can use let, as usual.
Discarding an expression
Often we may need to discard an expression
• This happens often with unit, when it is returned and we don’t need it.
An easy way to discard an expression is by using let with a variable that does not appear in the body:
let x = printf “%s/n” str in 3+2
In this case, we can also use underscore to avoid giving a name to this variable:
let _ = printf “%s/n” str in 3+2
This is often abbreviated in ocaml using a semicolon:
printf “%s/n” str; 3+2
Reading a line
let read_line (inc:in_channel) : string option = match input_line inc with
| l -> Some l
| exception End_of_file -> None
Writing a line
Printf.fprintf ouc “%s\n” str
The types need to match
An example – copying one line:
let ic=open_in “tmp.in’’ in
let oc=open_out “tmp.ou’’ in
let l=read_line ic in
let _ = match l with
Some s -> Printf.fprintf oc “%s/n’’ s in
|None -> ()
let _= close_in ic in
let _= close_out oc in()
TopHat Q6-Q7
Inductive Thinking
34
Induc,ve Programming and Proving
An induc&ve data type T is a data type defined by:
– a collec,on of base cases
• that don’t refer to T
– a collec,on of induc,ve cases that build new values of type T from
pre-exis,ng data of type T
• the pre-exis,ng data is guarateed to be smaller than the new values
Programming principle:
– solve programming problem for base cases
– solve programming problem for induc,ve cases by calling func,on
recursively (induc,vely) on smaller data value Proving principle:
– prove program sa,sfies property P for base cases
– prove induc,ve cases sa,sfy property P assuming induc,ve calls on smaller data values sa,sfy property P
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)
36
Induc,ve Case
Base Case
37
Lists are Induc,ve 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 alterna,ve syntax (“syntac,c 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
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) :: [ ] : ?? (2::[])::(5::6 ::[])::[] :?? [ [2]; [5; 6] ] : ??
39
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 ::[])::[] :intlistlist
[ [2]; [5; 6] ] : int list list
(Remember that the 3rd example is an abbrevia,on for the 2nd)
40
41
Another Example
• What type does this have?
[ 2 ] :: [ 3 ]
Another Example
• What type does this have?
[ 2 ] :: [ 3 ]
42
int list
int list
# [2] :: [3];;
Error: This expression has type int but an
#
expression was expected of type
int list
43
Another Example
• What type does this have?
[ 2 ] :: [ 3 ]
int list
int list
• Give me a simple fix that makes the expression type check?
44
Another Example
• What type does this have?
[ 2 ] :: [ 3 ]
int list
int list
• Give me a simple fix that makes the expression type check? Either: 2 :: [3] :intlist
Or: [ 2 ] :: [ [ 3 ] ] : int list list
45
Analyzing Lists
• Just like op,ons, there are two possibili,es when deconstruc,ng 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 op,ons, there are two possibili,es when deconstruc,ng lists. Hence we use a match with two branches
46
(* 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
47
Analyzing Lists
• Just like op,ons, there are two possibili,es when deconstruc,ng 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 func,on isn’t recursive — we only extracted a small , fixed amount of informa,on from the list — the first element
48
A more interes,ng 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]
*)
49
A more interes,ng 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 interes,ng 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 interes,ng example
52
(* 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
53
A more interes,ng 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 interes,ng example
54
(* 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
55
A more interes,ng 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 Construc,ng a Func,on
(1) Think about how to break down the input in to cases:
56
let rec prods (xs : (int*int) list) : int list =
match xs with
|[]-> …
| (x,y) :: tl -> …
This assump&on is called the Induc&on Hypothesis. You’ll use 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 …
57
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
*)
(Give it a try.)
58
Another example: zip
let rec zip (xs : int list) (ys : int list)
: (int * int) list option =
59
Another example: zip
let rec zip (xs : int list) (ys : int list)
: (int * int) list option =
match (xs, ys) with
60
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’) ->
61
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’) ->
62
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
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’
is this ok?
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’) -> (x, y) :: zip xs’ ys’
No! zip returns a list op,on, not a list!
We need to match it and decide if it is Some or None.
Another example: zip
65
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?
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’) ->
(match zip xs’ ys’ with
None -> None
| Some zs -> Some ((x,y) :: zs))
Another example: zip
67
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.
PaLern matching proceeds in order.
68
A bad list example
let rec sum (xs : int list) : int =
match xs with
| hd::tl -> hd + sum tl
A bad list example
69
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 =
TopHat Q7-Q16