程序代写代做代考 ocaml Java go C data structure CS 320 : Review of functional Programming in Ocaml

CS 320 : Review of functional Programming in Ocaml
Marco Gaboardi MSC 116 gaboardi@bu.edu

Announcements
• Thesecondtheoryhomeworkisisduetoday.
• Wewillpostthethirdprogrammingassignmentlaterthis week.

Plan for today
• QuickreviewofI/Oonfiles. • Reviewofpartialapplication • Reviewofpolymorphism
• Programequivalence
• ReviewofFunctionalProgrammingpart • IntrotoPart2

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.

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_input.txt” in let oc=open_out “tmp_output.txt” in let l=read_line ic in
let _ = match l with
None -> ()
| Some s -> Printf.fprintf oc “%s\n” s in
let _= close_in ic in let _= close_out oc in ()

Functions

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 : ??

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)

Some examples
let f x = [x ^ “str”]
let foo g n = if n = “Hello” then [“1”] else (g n)
let partial = foo f partial “str”

Some examples
let h = fun x -> fun y-> [x + y]
let rec foo1 n g =
if n = 1
then [[1]]
else (g n n) :: foo1 (n-1) g
let partial = fun x -> foo1 x h partial 10

Polymorphism

Type of the undecorated map?
let rec map f xs =
match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl)
map : (‘a -> ‘b) -> ‘a list -> ‘b list
66

How about reduce?
let rec reduce (f:’a -> ‘b -> ‘b) (u:’b) (xs: ‘a list) : ‘b = match xs with
| [] -> u
| hd::tl -> f hd (reduce f u tl)
What’s the most general type of reduce?
(‘a -> ‘b -> ‘b) -> ‘b -> ‘a list -> ‘b
91

Are these expressions well typed? What is their type?
let foo x y g = Some [g x (y+1)] let foo f x y = f x y
let foo1 f x y = let foo2 f x y = let foo3 f x y = let foo4 f x y = let foo5 f = f f
f x y in foo1 (fun u w -> u+w+1)
f x y in foo2 (fun u w -> (u,w))
f (x y)
f (x y) in fun f -> foo4 f (fun x -> x)

Program equivalence

Are these two programs equivalent?
let rec foo1 l = match l with
| [] -> []
| hd::tl -> hd :: (foo1 tl)
let rec foo2 l = match l with
| [] -> []
| hd::tl -> hd :: (foo2 tl)

Are these two programs equivalent?
let rec foo1 l a = match l with
| [] -> [] ✘ | hd::tl -> hd :: (foo1 tl)
let rec foo2 l = match l with
| [] -> []
| hd::tl -> hd :: (foo2 tl)

Are these two programs equivalent?
let rec foo1 l = match l with
| [] -> [1] ✘ | hd::tl -> hd :: (foo1 tl)
let rec foo2 l = match l with
| [] -> []
| hd::tl -> hd :: (foo2 tl)

When are two programs equivalent? Two programs are (operationally) equivalent if and
only if:
• theyhavethesametype
• foreverypossibleinputtheyreturnthesameoutput
Here we are assuming that the only way to interact with a program is through its inputs. This is true for pure functional languages, it requires more care for languages with side-effects.

TopHat Q1-Q4

Reasoning about definitions

Reasoning About DefiniKons
We can factor this program
let square_all ys = match ys with
| [] -> []
| hd::tl -> (square hd)::(square_all tl)
into this program:
let square_all = map square assuming we already have a definiKon of map
46

Reasoning About DefiniKons
let square_all = map square
Goal: Rewrite definiKons so my program is simpler, easier to
understand, more concise, …
QuesAon: What are the reasoning principles for rewriKng programs without breaking them? For reasoning about the behavior of programs? About the equivalence of two programs?
I want some rules that never fail.
let square_all ys = match ys with
| [] -> []
| hd::tl -> (square hd)::(square_all tl)
47

Rewrite 1 (FuncKon de-sugaring):
Simple EquaKonal Reasoning
let f x = body
==
let f = (fun x -> body)
Rewrite 2 (SubsKtuKon):
(fun x -> … x …) arg
Rewrite 3 (Eta-expansion):
if f has a funcKon type
if arg is a value or, when executed,
will always terminate without effect and produce a value
roughly: all occurrences of x replaced by arg (though geSng this exactly right is shockingly difficult)
chose name x wisely so it does not shadow other names used in def
==
… arg …
let f = def
==
let f x = (def) x

Eta-expansion is an example of Leibniz’s law
Go}ried Wilhelm von Leibniz German Philosopher
1646 – 1716
Leibniz’s law:
If every predicate possessed by x is also possessed by y and vice versa, then enKKes x and y are idenKcal. Frequently invoked in modern logic and philosophy.
Rewrite 3 (Eta-expansion):
let f = def
if f has a funcKon type
chose name x wisely so it does not shadow other names used in def
==
let f = fun x -> (def)x

EliminaKng the Sugar in Map
let rec map f xs =
match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl)
50

EliminaKng the Sugar in Map
let rec map f xs =
match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl)
let rec map = (fun f ->
(fun xs ->
match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl)))
51

let rec map = (fun f ->
Consider square_all
(fun xs ->
match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl)))
let square_all = map square
52

SubsKtute map definiKon into square_all
let rec map = (fun f ->
(fun xs ->
match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl)))
let square_all = (fun f ->
(fun xs ->
match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl)
)
) square
53

let rec map = (fun f ->
let square_all = (
(fun xs ->
match xs with
| [] -> []
argument square subsKtuted for parameter f
SubsKtute Square
(fun xs ->
match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl)))
| hd::tl -> (square hd)::(map square tl)
)
56

let rec map = (fun f ->
let square_all ys =
(fun xs ->
match xs with
| [] -> []
add argument
via eta-expansion
Expanding map square
(fun xs ->
match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl)))
| hd::tl -> (square hd)::(map square tl)
) ys
57

let rec map = (fun f ->
Expanding map square
(fun xs ->
match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl)))
let square_all ys =
match ys with
| [] -> []
| hd::tl -> (square hd)::(map square tl)
subsKtute again (argument ys for
parameter xs)
58

So Far
let rec map f xs = match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl)
let square_all xs = map square xs
proof by simple rewriKng unrolls definiKon once
let square_all ys = match ys with
| [] -> []
| hd::tl -> (square hd)::(map square tl)
59

Next Step
let rec map f xs = match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl)
let square_all xs = map square xs
proof by simple rewriKng unrolls definiKon once
proof
by
inducAon
eliminates
recursive
funcKon
map
let square_all ys = match ys with
| [] -> []
| hd::tl -> (square hd)::(map square tl) ;;
let square_all ys = match ys with
| [] -> []
| hd::tl -> (square hd)::(square_all tl)
60

We saw this:
Summary
let rec map f xs = match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl);;
let square_all ys = map square
Is equivalent to this:
let square_all ys = match ys with
| [] -> []
| hd::tl -> (square hd)::(map square tl)
Morals of the story:
(1) OCaml’s hot (higher-order, typed) funcKons capture recursion paRerns (2) we can figure out what is going on by equaAonal reasoning.
(3) … but we typically need to do proofs by inducAon to reason about recursive (inducKve) funcKons
61

TopHat Q5-Q8

Why study functional programming?
1. Learning a different style of programming teach you that programming transcends programming in a language/style
2. Functional languages predict the future (several concepts adopted in other languages)
3. Functional languages are more and more used in industry
4. Functional languages help writing correct code (types, function encapsulation, equational reasoning, etc.)
Copyright Nate Foster

Thinking Functionally
In imperative languages like Java or C, you get most work done by changing something
Commands modify or change the state – in this case an existing data structure (pair)
In functional languages you get most work done by
temp = pair.x;
pair.x = pair.y;
pair.y = temp;
producing something new
let
(x,y) = pair
in (y,x)
Copyright David Walker
Commands analyze an existing data (pair) and produce a new data (y,x)

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

Factoring Code in OCaml
A higher-order funcKon captures the recursion paRern:
let rec map (f:int->int) (xs:int list) : int list = match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl);;We can use an
Uses of the funcKon:
anonymous
funcKon instead.
Originally, Church wrote this funcKon using λ instead of fun: (λx. x+1) or (λx. x*x)
let inc_all xs = map (fun x -> x + 1) xs let square_all xs = map (fun y -> y * y) xs
27

More on Anonymous FuncKons FuncKon declaraKons:
are syntacAc sugar for:
In other words, funcAons are values we can bind to a variable, just like 3 or “moo” or true.
FuncKons are 2nd class no more!
let square x = x*x
let add x y = x+y
let square = (fun x -> x*x)
let add = (fun x y -> x+y)
38

Curried FuncKons
Currying: verb. gerund or present parAciple (1) to prepare or flavor with hot-tasKng spices
(2) to encode a mulK-argument funcKon using nested, higher-order funcKons.
(1)
fun x -> (fun y -> x+y)(* curried *) fun x y -> x + y (* curried *) fun (x,y) -> x+y (* uncurried *)
(2)
40

u
u

let rec fold_right (f: ‘a -> ‘b -> ‘b) (xs: ‘a list) (z: ‘b) : ‘b = match xs with
[] -> z
| hd::tl -> f hd (fold_right f tl z)
# fold_right (+) [1;2;3;4;5] 0

let rec fold_left l (f: ‘b -> ‘a -> ‘b) (z: ‘b) (xs: ‘a list) : ‘b = match xs with
[] -> z
| hd::tl -> fold_left f (f z hd) tl
# fold_left (+) 0 [1;2;3;4;5]

Data types
• OCaml provides a general mechanism called a data type for defining new data structures that consist of many alternaFves
type my_bool = Tru | Fal
• CreaFng values:
34
type color = Blue | Yellow | Green | Red
let b1 : my_bool = Tru
let b2 : my_bool = Fal
let c1 : color = Yellow
let c2 : color = Red
use constructors to create values

56
InducFve data types
• We can use data types to define inducFve data
• A binary tree is:
– a Leaf containing no data
– a Node containing a key, a value, a leP subtree and a right subtree
type key = string
type value = int
type tree =
Leaf
| Node of key * value * tree * tree

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 of the undecorated map?
let rec map f xs =
match xs with
| [] -> []
| hd::tl -> (f hd)::(map f tl)
map : (‘a -> ‘b) -> ‘a list -> ‘b list
Read as:
• for any types ‘a and ‘b,
• if you give map a funcKon from ‘a to ‘b,
• it will return a funcKon
– which when given a list of ‘a values – returns a list of ‘b values.
We owen use greek leRers like α or β to represent type variables.
67

TopHat Q9-Q21

Related Posts