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
What is a Functional Language
A functional language:
• defines programs in a way similar to the one we
useto define mathematical functions,
• avoids the use of mutable states (states that can
change) in describing what a program should do.
In a functional language, the information is maintained by the computation.
Terminology: Expressions, Values, Types
• Expressions are computaCons
– 2 + 3 is a computaCon
• Values are the results of computaCons
– 5 is a value
• Types describe collecCons of values and the computaCons
that generate those values – int is a type
– values of type int include • 0, 1, 2, 3, …, max_int
• -1, -2, …, min_int
47
• Example rules:
(1)
(2) “abc” : string
0 : int
(3) ife1:intande2:int
then e1 + e2 : int
(5) if e1 : string and e2 : string
then e1 ^ e2 : string • Using the rules:
2:intand3:int. Therefore, (2 + 3) : int 5 : int
(4) ife1:intande2:int then e1 * e2 : int
(6)
Type Checking Rules
(and similarly for any other integer constant n) (and similarly for any other string constant “…”)
13
(Byrule 1) (By rule 3) (By rule 1)
if e : int
then string_of_int e : string
• Example rules:
(1)
(2) “abc” : string
0 : int
(3) ife1:intande2:int
FYI: This is a formal proof (4) ife1:intande2:int
then e1 + e2 : int
if e1 : string and e2 : string
(6)
(5)
• Using the rules:
then e1 ^ e2 : string
Type Checking Rules
(and similarly for any other integer constant n) (and similarly for any other string constant “…”)
14
(Byrule 1) (By rule 3) (By rule 1)
that the expression is well-
then e1 * e2 : int typed!
if e : int
then string_of_int e : string
2:intand3:int.
Therefore, (2 + 3) : int
5 : int
Therefore, (2 + 3) * 5 : int (By rule 4 and our previous work)
Notation
We will often use lower case english letters, e,f,g, etc to denote an arbitrary expression. If we write
fe
We mean that we are considering an expression built up as the application of an expression named f to another expression named e
Notation
When we write
fge
We mean that we are considering an expression built up as the application of an expression named f to another expression named g, and the
resulting expression is further applied to an expression named e.
This comes from the fact that application associates to the left, so we read the expression above as:
((f g) e)
TopHat Q1-Q2
Learning Goals for today
• MoreTypeChecking • TypeSafety
• Let-abstraction
• Definingfunctions
• FunctionTypes
• Example rules:
(1)
(2) “abc” : string
0 : int
(3) ife1:intande2:int
then e1 + e2 : int
(5) if e1 : string and e2 : string
then e1 ^ e2 : string • ViolaRng the rules:
“hello” : string 1 : int
1 + “hello” : ??
(4) ife1:intande2:int then e1 * e2 : int
(6)
Type Checking Rules
(and similarly for any other integer constant n) (and similarly for any other string constant “…”)
23
if e : int
then string_of_int e : string
(By rule 2)
(By rule 1)
(NO TYPE! Rule 3 does not apply!)
•
•
ViolaRng the rules:
Type Checking Rules ViolaRng the rules:
24
# “hello” + 1;;
Error: This expression has type string but an
expression was expected of type int
• • •
• • •
The type error message tells you the type that was expected The type error message tells you the type that was expected
and the type that it inferred for your subexpression and the type that it inferred for your subexpression
By the way, this was one of the nonsensical expressions that
By the way, this was one of the nonsensical expressions that
did not evaluate to a value
did not evaluate to a value
It is a good thing that this expression does not type check! It is a good thing that this expression does not type check!
“Well typed programs do not go wrong” Robin Milner, 1978
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
Type Checking Rules • ViolaRng the rules:
25
# “hello” + 1;;
Error: This expression has type string but an
expression was expected of type int
• A possible fix:
# “hello” ^ (string_of_int 1);;
– : string = “hello1”
• One of the keys to becoming a good ML programmer is to understand type error messages.
TopHat Q3-Q7
Abstraction
What is the single most important mathemaDcal concept ever developed in human history?
2
What is the single most important mathemaDcal concept ever developed in human history?
An answer: The mathemaDcal variable
3
What is the single most important mathemaDcal concept ever developed in human history?
An answer: The mathemaDcal variable (runner up: natural numbers/inducDon)
4
5 Why is the mathemaDcal variable so important?
The mathemaDcian says:
“Let x be some integer, we define a polynomial over x …”
6 Why is the mathemaDcal variable so important?
The mathemaDcian says:
“Let x be some integer, we define a polynomial over x …”
What is going on here? The mathemaDcian has separated a defini&on (of x) from its use (in the polynomial).
This is the most primiDve kind of abstrac&on (x is some integer) Abstrac&on is the key to controlling complexity and without it,
modern mathemaDcs, science, and computaDon would not exist. It allows reuse of ideas, theorems … funcDons and programs!
Let-abstraction (or let-binding)
8
AbstracDon
• Good programmers idenDfy repeated paZerns in their code and factor out the repeDDon into meaningful components
• In O’Caml, the most basic technique for factoring your code is to use let expressions
• Instead of wriDng this expression: (2 + 3) * (2 + 3)
AbstracDon & AbbreviaDon
• Good programmers idenDfy repeated paZerns in their code and factor out the repeDDon into meaning components
• In O’Caml, the most basic technique for factoring your code is to use let expressions
• Instead of wriDng this expression: (2 + 3) * (2 + 3)
• We write this one:
9
let x = 2 + 3 in x*x
11
A Few More Let Expressions
let x = 2 in
let squared = x * x in
let cubed = x * squared in
squared * cubed
‘-
let a = “a” in
let b = “b” in
let as = a ^ a ^ a in
let bs = b ^ b ^ b in
as ^ bs
26
10
A Few More Let Expressions
let x = 2 in
let squared = x * x in
let cubed = x * squared in
squared * cubed
Nested let … in creates distinct scopes
‘-
27
12
AbstracDon & AbbreviaDon • Two kinds of let:
if tuesday() then
let x = 2 + 3 in
x+x else
0
let x = 2 + 3
let y = x + 17 / x
let … in … is an expression that
can appear inside any other expression
The scope of x does not extend outside the enclosing “in”
let … without “in” is a top-level declara&on
Variables x and y may be exported; used by other modules
(Don’t need ;; if another let comes next; do need it if the next top-level declaraDon is an expression)
13
Binding Variables to Values
• Each OCaml variable is bound to 1 value
• The value to which a variable is bound to never changes!
let x = 3
let add_three (y:int) : int = y + x
14
Binding Variables to Values
• Each OCaml variable is bound to 1 value
• The value to which a variable is bound to never changes!
It does not ma;er what I write next. add_three will always add 3!
let x = 3
let add_three (y:int) : int = y + x
Binding Variables to Values
• Each OCaml variable is bound to 1 value
• The value a variable is bound to never changes!
15
let x = 3
let add_three (y:int) : int = y + x
let x = 4
let add_four (y:int) : int = y + x
a disDnct variable that “happens to be spelled the same”
Binding Variables to Values
• Since the 2 variables (both happened to be named x) are actually different, unconnected things, we can rename them
16
let x = 3
let add_three (y:int) : int = y + x
let zzz = 4
let add_four (y:int) : int = y + zzz
let add_seven (y:int) : int =
add_three (add_four y)
rename x
to zzz
if you want to, replacing its uses
Binding Variables to Values
• Each OCaml variable is bound to 1 value
• OCaml is a staDcally scoped (or lexically scoped) language
17
let x = 3
let add_three (y:int) : int = y + x
let x = 4
let add_four (y:int) : int = y + x
let add_seven (y:int) : int =
add_three (add_four y)
we can use add_three without worrying about the second definiDon of x
18
How do let expressions operate?
let x = 2 + 1 in x * x
How do let expressions operate?
let x = 2 + 1 in x * x
–>
19
let x = 3 in x * x
20
How do let expressions operate?
let x = 2 + 1 in x * x
–>
–>
subsDtute 3 for x
let x = 3 in x * x
3*3
How do let expressions operate?
21
let x = 2 + 1 in x * x
–>
–>
subsDtute 3 for x
let x = 3 in x * x
–>
3*3
9
How do let expressions operate?
22
let x = 2 + 1 in x * x
–>
–>
subsDtute 3 for x
let x = 3 in x * x
–>
3*3
Note: I write
e1 –> e2
when e1 evaluates to e2 in one step
9
23
Did you see what I did there?
24
Did you see what I did there?
I defined the language in terms of itself: let x = 2 in x + 3 –> 2 + 3
I’m trying to train you to think at a high level of abstracDon.
I didn’t have to men&on low-level abstrac&ons like assembly code or registers or memory layout
25
Another Example
let x = 2 in
let y = x + x in y*x
26
Another Example
subsDtute 2 for x
let x = 2 in
let y = x + x in y*x
let y = 2 + 2 in y*2
–>
27
Another Example
subsDtute 2 for x
let x = 2 in
let y = x + x in y*x
let y = 2 + 2 in y*2
–>
–>
let y = 4 in y*2
28
Another Example
subsDtute 2 for x
let x = 2 in
let y = x + x in y*x
let y = 2 + 2 in y*2
–>
–>
–>
subsDtute 4 for y
let y = 4 in y*2
4*2
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
–> –>
30 What would happen in an imperaDve language?
x = 2;
x += x;
return x*2;
C program:
–>
subsDtute 2 for x
Moral: Let operates by subsDtuDng computed values for variables
x+=2 ??? return x*2;
This principle works in funcDonal languages, not so well in imperaDve languages
Back to Let Expressions … Typing
x granted type of e1 for use in e2
32
let x = e1 in e2
overall expression takes on the type of e2
33
Back to Let Expressions … Typing
x granted type of e1 for use in e2
let x = e1 in e2
overall expression takes on the type of e2
let x = 3 + 4 in
string_of_int x
x has type int
for use inside the let body
overall expression has type string
TopHat Q8-Q13
Functions
35
Defining funcDons
let add_one (x:int) : int = 1 + x
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”
Defining funcDons • Nonrecursive funcDons:
37
let add_one (x:int) : int = 1 + x
let add_two (x:int) : int = add_one (add_one x)
definiDon of add_one must come before use
38
Defining funcDons • Nonrecursive funcDons:
let add_one (x:int) : int = 1 + x
let add_two (x:int) : int = add_one (add_one x)
• With a local definiDon:
local funcDon definiDon hidden from clients
I lep off the types. O’Caml figures them out
Good style: types on top-level definiDons
let add_two’ (x:int) : int =
add_one (add_one x)
let add_one x = 1 + x in
39
Some funcDons:
Types for FuncDons
let add_one (x:int) : int = 1 + x
let add_two (x:int) : int = add_one (add_one x)
let add (x:int) (y:int) : int = x + y
Types for funcDons:
funcDon with two arguments
add_one : int -> int
add_two : int -> int
add : int -> int -> int
Rule for type-checking funcDons
General Rule:
Example:
40
If a funcDon f : T1 -> T2 and an argument e : T1 then f e : T2
add_one : int -> int
3 + 4 : int
add_one (3 + 4) : int
Rule for type-checking funcDons • Recall the type of add:
DefiniDon:
Type:
41
let add (x:int) (y:int) : int = x+y
add : int -> int -> int
42
Rule for type-checking funcDons • Recall the type of add:
DefiniDon:
Type:
Same as:
let add (x:int) (y:int) : int = x+y
add : int -> int -> int
add : int -> (int -> int)
43
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) : ???
44
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) :
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
46
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
(add (3 + 4)) 7 : int
47
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
add (3 + 4) 7 : int
Rule for type-checking funcDons
Example:
48
let munge (b:bool) (x:int) : ?? =
if not b then
string_of_int x
else
“hello” ;;
let y = 17;;
munge (y > 17) : ??
munge true (f (munge false 3)) : ??
f : ??
munge true (g munge) : ??
g : ??
Rule for type-checking funcDons
Example:
49
let munge (b:bool) (x:int) : ?? =
if not b then
string_of_int x
else
“hello” ;;
let y = 17;;
munge (y > 17) : ??
munge true (f (munge false 3)) : ??
f : string -> int
munge true (g munge) : ??
g : (bool -> int -> string) -> int
50
One key thing to remember
• If you have a funcDon f with a type like this:
A -> B -> C -> D -> E -> F
• Then each Dme you add an argument, you can get the type of the result by knocking off the first type in the series
fa1:B->C->D->E->F (ifa1:A)
f a1 a2 : C -> D -> E -> F f a1 a2 a3 : D -> E -> F
f a1 a2 a3 a4 a5 : F
(if a2 : B)
(if a3 : C)
(if a4 : D and a5 : E)
TopHat Q14-Q19
Summary
• MoreTypeChecking • TypeSafety
• Let-abstraction
• Definingfunctions
• FunctionTypes