1 Lecture 1 <2017-09-12 Tue> 3
1.1 FourmaingoalsofCOMP302 …………….. 4 1.1.1 Howweachievethesegoals …………… 5 1.1.2 GuidingPrinciples ……………….. 5 1.1.3 WhydoIneedtoknowthis…………… 6
1.2 Assignments………………………. 6
1.3 Misc………………………….. 6
Copyright By PowCoder代写 加微信 powcoder
2 Lecture 2 <2017-09-14 Thu> 6
2.1 WhatisOCaml…………………….. 6 2.1.1 Staticallytyped…………………. 6 2.1.2 Functional……………………. 7 2.1.3 ConceptsforToday……………….. 7 2.1.4 OCamldemoinclass………………. 7
3 Lecture 3 <2017-09-15 Fri> 10
3.1 Functions ……………………….. 10 3.1.1 Recursivefunctions……………….. 10 3.1.2 Passingarguments ……………….. 11
3.2 DataTypesandPatternMatching …………… 12 3.2.1 Playingcards ………………….. 12
4 Lecture 4 <2017-09-19 Tue> 13
4.1 Data Types and Pattern Matching Continued . . . . . . . . . 13 4.1.1 Recursivedatatype ………………. 13 4.1.2 ExtractExample ………………… 14
5 Lecture 5 <2017-09-21 Thu> 15 5.1 Lists………………………….. 16 5.2 Execution ……………………….. 17
6 Lecture 6 <2017-09-22 Fri> 17 6.1 Proofs…………………………. 17 6.1.1 Demo:lookup&insert……………… 17 6.1.2 Howtoproveit? ………………… 18
7 Lecture 7 <2017-09-26 Tue> 20
7.1 StructuralInduction ………………….. 20 7.1.1 Examplewithrev………………… 20
7.2 Trees………………………….. 22
8 Lecture 8 <2017-09-28 Thu> 23
8.1 BinaryTree(Inductivedefinition)……………. 23
8.2 Insert …………………………. 23
8.3 Proving ………………………… 25
8.4 Theorem………………………… 25
8.4.1 Proof by structural induction on the tree t . . . . . . . 26
9 Lecture 9 <2017-09-29 Fri> 26 9.1 Higher-orderfunctions …………………. 26 9.1.1 Abstracting over common functionality . . . . . . . . . 27
9.2 Demo …………………………. 27
9.3 Bonus …………………………. 30
10 Lecture 10 <2017-10-03 Tue> 31
11 Lecture 11 <2017-10-05 Thu> 33 11.1Lambda-Calculus……………………. 33 11.2Backtothebeginning …………………. 34 11.3Curry …………………………. 34 11.4Uncurrying ………………………. 35 11.5Demo …………………………. 35 11.6Partialevaluation……………………. 36
12 Lecture 12 <2017-10-06 Fri> 37 12.1Review…………………………. 37 12.2Demo,usinghigherorderfunctions…………… 38
13 Lecture 13 <2017-10-12 Thu> 39 13.1MidtermReview ……………………. 39
14 Lecture 14 <2017-10-13 Fri> 40 14.1Overshadowing …………………….. 40 14.2State………………………….. 40 14.3Demo …………………………. 41
15 Lecture 15 <2017-10-17 Tue> 44 15.1Warmup ……………………….. 44 15.2Demo …………………………. 46
16 Lecture 16 <2017-10-19 Thu> 46 16.1Demo …………………………. 46
17 Lecture 17 <2017-10-20 Fri> 48 17.1Exceptions……………………….. 48 17.1.1 Warm-up ……………………. 48 17.1.2Demo ……………………… 49
18 Lecture 18 <2017-10-24 Tue> 51 18.1Backtracking ……………………… 51
19 Lecture 19 <2017-10-26 Thu> 53 19.1Modules………………………… 53 19.2Signatures(ModuleTypes) ………………. 54 19.3Demo …………………………. 54
20 Lecture 20 <2017-10-27 Fri> 57 20.1MoreonModules……………………. 57 20.2Demo …………………………. 57
21 Lecture 21 <2017-10-31 Tue> 61 21.1Continuations……………………… 61 21.1.1 First-class Support for Continuations . . . . . . . . . . 61 21.1.2 Recipe……………………… 62 21.1.3Demo ……………………… 62
1 Lecture 1 <2017-09-12 Tue>
This course is an introduction to the foundations and paradigms of program-
ming languages.
• 5 assignments, 5% each
• 10% midterm
• 65% final
• You have two late days for the semester (cumulative)
1.1 Four main goals of COMP 302
1. Provide thorough introduction to fundamental concepts in program- ming languages
• Higher-order functions
• State-full vs state-free computation (most languages like Java we’ve seen are state-full)
• Modeling objects and closures
• Exceptions to defer control
• Continuations to defer control
• Polymorphism
• Partial evaluation
• Lazy programming
• Want to explore these concepts so you can recognize them in another language you study at some point
2. Show different ways to reason about programs
• Type checking
– One of the best inventions
– Checks what it expects and will actually tell you where it
expects something
– Program is more likely to be correct now
• Induction
– Proving a program/transformation correct
• Operational semantics
– How a program is executed
• QuickCheck
3. Introduce fundamental principles in programming language design
• Grammars
• Operational semantics and interpreters
• Type checking • Polymorphism • Subtyping
Expose students to a different way of thinking about problems • It’s like going to the gym; it’s good for you!
How we achieve these goals
Functional programming in OCaml
– Equal playing field
∗ No one in the class really knows it, not affected by perfor-
mance in previous classes like 250
– Allows us to explain and model object-oriented and imperative programming
∗ Isolates lots of the concepts individually
– Isolatesconceptssuchasstate-fullvsstate-free,modulesandfunc- tions, etc.
– Statically typed language enforces disciplined programming
∗ Also demonstrates that types are an important maintenance
– Easy to reason about runtime behavior and cost
Guiding Principles
No point in learning a programming language unless it changes how you view programming
Simple and elegant solutions are more effective, but harder to find than the complicated ones, take more time.
– You spend very little time testing OCaml code and more time compiling it
1.1.3 Why do I need to know this
• Science and craft of programming
• Skills you learn will help you become a better programmer
– More productive
– Code easier to maintain and read – Etc.
• Will be needed in some upper level courses – Like compilers, etc.
• It is cool and fun!
• You might even get a job!
1.2 Assignments
• Can do assignments in groups of 2
Lectures won’t be recorded.
Slides may or may not be posted, but there are lecture notes on My- Courses (most essential reading)
Lecture 2 <2017-09-14 Thu> What is OCaml
• Statically typed functional programming language
2.1.1 Statically typed
• Types approximate runtime behavior
• Analyze programs before executing them
• Find a fix bugs before testing
• Tries to rule out bad scenarios
• Very efficient, very good error messages, very good maintenance tool
2.1.2 Functional
• Primary expressions are functions! • Functions are first-class!
– Not only can we return base types like ints, we can return func- tions and pass them as arguments too
– One of the key features of functional languages • Pure vs Not Pure languages
– Haskell is Pure
∗ Doesn’t give you ways to allocate memory or directly modify
– OCaml is impure
∗ Has arrays and consequences and stuff • Call-By-Value vs Lazy
– OCaml is call by value
2.1.3 Concepts for Today
• Writing and executing basic expressions • Learn how to read error messages
2.1.4 OCaml demo in class
• Always have to finish a line with 2 semi colons ;; • Can use interpreter by launching OCaml in shell • Functional good for parallel computing
• Good to reason about these programs
• Strings:
– “Hello”;;
• Booleans: – true;;
– if 0=0 then 1.4 else 2.1 ;;
1. Operators
– Take as input 2 int, return int
• 3.14+1;;→error
• To specify for floating point operators, follow by a dot. Only
works with floating points, no ints – 3.14 +. 2.4 ;;
• Approximate the runtime behaviour
• Types classify expressions according to the value they will com- pute
• Won’t execute right away, will think of types you are returning to see if it’s valid
• if 0=0 then 1.4 else 3 ;;
– Error, after reading 1.4 expects 3 to be float
• if bool then T else T
– Both Ts have to be the same type
• Type checker will allow 1/0;; to run, but will have a runtime exception
– int/int is not enough info to know that your dividing by 0 3. Vars
• letpi=3.14;;
• let (pi : float) = 3.14 ;; • letm=3in
– letn=m*min – let k=m*m in – k*n ;;
4. Binding
• letm=3;;putsitonthestack
• letm=3in…
– m is a local variable now (temporary binding), once you hit ;;, won’t have m anymore
– Garbage collector
• let x (name of a variable) = exp in exp (x is bound to this ex-
• variables are bind to values, not assigned values
– they look in the past! 5. Functions
• letarea=functionr->pi*. r*.r;; – Syntax error
• letarea=functionr->pi*. r*. r;;
• letarear=pi*. r*. r;;
• let a4 = area (2.0);;
• If you redefine pi, like let pi = 6.0 ;;
• area(2.0) will still give you the same thing • The function looks up in the past
pi 6.0 area functionr->p*. r*. r k5 k4
• Can redefine the function though 9
3 Lecture 3 <2017-09-15 Fri>
3.1 Functions
• Functions are values
• Function names establish a binding of the function name to its body
– let area (r:float)=pi*. r *. r ;;
3.1.1 Recursive functions
Recursive functions are declared using the keyword let rec
• letrecfactn=
– ifm=0them1
∗ else n*face(n-1)
• fact 2 needs to be stored on the stack
• fact2->2*fact1
• fact 1 -> 1* fact 0 stored on stack
• Need to remember computation when you come back out of recursion, so need to store on the stack
– What’s the solution to this? How is functional programming effi- cient?
1. Tail-recursive functions A function is said to be “tail-recursive”, if there is nothing to do except return the final value. Since the execution of the function is done, saving its stack frame (i.e. where we remember the work we still in general need to do), is redundant
• Write efficient code
• All recursive functions can be translated into tail-recursive form
2. Ex. Rewrite Factorial
• let rec fact_tr n = – let rec f(n,m) –
∗ if n=0 then ·m
∗ else f(n-1,n*m) – in
• Second parameter to accumulate the results in the base case we simply return its result
• Avoids having to return a value from the recursive call and sub- sequently doing further computation
• Avoids building up a runtime stack to memorize what needs to be done once the recursive call returns a value
• f(2,1) -> fact(1, 2*1) -> fact(0,2)-> 2
• Whoever uses the function does not need to know how the func- tion works, so you can use this more efficient way in the back- ground
• What is the type of fact_tr? fact_tr: int(input) → int(output)
• Type of f? f: int * int (tuple input) → int
– n-tuples don’t need to be of the same type, can have 3 differ- ent types, like int*bool*string
3.1.2 Passing arguments
• ’ means any type, i.e. ’a
• All args at same time
– ’a*’b -> ’c
• One argument at a time
– ’a->’b->’c
– May not have a and b at the same time. Once it has both it will
• We can translate any function from one to the other type, called cur- rying (going all at once to one at a time) and uncurrying (opposite).
– Will see in 2 weeks
Data Types and Pattern Matching
Playing cards
How can we model a collection of cards? Declare a new type together with its elements type suit = Clubs | Spades | Hearts | Diamonds
– Called a user-defined (non-recursive) data type
– Order of declaration does not matter
∗ Like a set
– We call clubs, spades, hearts, diamonds constructors (or con- stants), also called elements of this type
∗ Constructors must begin with a capital letter in OCaml Use pattern matching to analyze elements of a given type.
match
A pattern is either a variable or a . . . • Statements checked in order
1. Comparing suits Write a function dom of type suit*suit -> bool
• dom(s1,s2) = true iff suit s1 beats or is equal to suit s2 relative to the ordering Spades > Hearts > Diamonds > Clubs
• (Spades, _) means Spades and anything
• (s1, s2) -> s1=s2 will return the result of s1=s2
• Compiler gives you warning if it’s not exhaustive and tells you some that aren’t matched
4 Lecture 4 <2017-09-19 Tue>
4.1 Data Types and Pattern Matching Continued
• Type is unordered
• type suit = Clubs | Spades | Hearts | Diamonds
– Order doesn’t matter here, but they must start with capitals • typerank=Two|Three|…
• type card = rank * suit
Whatisahand? Ahandiseitheremptyorifcisacardandhisahand then Hand(c,h). Nothing else is a hand. Hand is a constructor. hand is a type. (capitalization mattersA)
• Recursive user defined data type
• Inductive or recursive definition of a hand
– Add a card to something that is a hand, still a hand
4.1.1 Recursive data type
• type hand = Empty | Hand of card * hand 1. Typing into interpreter
– hand = Empty
• let h1 = Hand ((Ace, Spades),Empty);;
– Want only 1 card, so include empty
– Recursive data type, so it needs another hand in it
• let h2 = Hand ((Queen, Hearts), Hand((Ace,Spades), Empty);; – Recursive
• let h3 = Hand ((Joker, Hearts), h2) ;; – Error, Joker not defined
• type’alist=Nil|Consof’a*’alist
• Hand ((Queen, Hearts), (King, Spades), (Three, Diamonds));;
– Hand has type? card * card * card
– Get an error, because constructor Hand expects 2 arguments
(card+hand)
4.1.2 Extract Example
• Given a hand, extract all cards of a certain suit • extract: suit -> hand -> hand
let rec extract (s:suit) (h:hand) = match h with
| Empty -> Empty (* We are constructing results, not destructing given hand *)
(* Want to extract suit from first card *)
| Hand ( (r0.s0) ,h) ->
(*Make a hand with first card and remaining results of recursive ext*)
if s0 = s then Hand( (r0, s0), extract s h0)
else extract s h0
Hand is “destroyed” through this method, but old hand stays the same, it is not modified.
• Running extract Spades hand5;; will give a new hand with only spades
• Good exercise, write a function that counts how many cards in the hand
• Can we make this thing tail recursive?
let rec extract’ (s:suit) (h:hand) acc = match h with
| Empty -> acc (* Accumulator *)
(* Want to extract suit from first card *)
| Hand ( (r0.s0) ,h) ->
(*Make a hand with first card and remaining results of recursive ext*)
if s0 = s then extract’ s h0 (Hand( (r0, s0), acc))
else extract’ s h0 acc
• extract’ Spades hand5 Empty ;;
• Gives same cards but in the reverse order of extract
• extract Spades hand5 = extract’ Spades hand5 Empty ;;
• Write a function find which when given a rank and a hand, finds the first card in hand of the specified rank and returns its corresponding suit.
What if no card exists?
• Optional Data Type (predefined)
• type ’a option = None | Some of ’a
5 Lecture 5 <2017-09-21 Thu>
(* type mylist = Nil | Cons of ? * list;; *)
(* Polymorphic lists: *)
(* type ’a mylist = Nil | Cons of ’a * ’a my list *)
1 :: [] ;;
1 :: 2 :: 3 :: [] ;;
[1;2;3;4];;
(* These are only homogenous lists though, what if we want floats and ints? *)
(* type if_list = Nil | ICons of int * if_list | FCons of float * if_list *)
(* But here we can’t use List libraries *)
(* So make an element that can be either *)
type elem = I of int | F of float;;
let rec append l1 l2 = match l1 with
| [] -> l2
| x::xs -> x :: append xs l2;;
(* Program execution *)
(* append 1::(2::[]) -> 1 :: append (2::[]) *)
let head l = match l with
| [] -> None
| x :: xs -> Some x;;
(* Write a function rev given a list l of type ’a list returns it’s reverse *)
(* Silly way of doing this *)
let rec rev (l : ’a list) = match l with
| [] -> []
| hd :: tail -> rev (tail) @ [hd];;
(* Could we have written rev(tail) :: hd? No. Why? *)
(* a’ : ’a list, left side has to be one element, right side to be a list *)
(* ’a list @ ’alist *)
(* What is the type of rev? Is it ’a list? -No *)
(* It is ’a list -> ’a list *)
(* Is this a good program? Long running time, use tail recursion *)
let rev_2 (l : ’a list) =
let rec rev_tr l acc = match l with
| [] -> acc
| h::t -> rev_tr t (h::acc)
rev_tr l [];;
(* Exercises:
* Write a function merge: ’a list -> ’a list -> ’a list
which given ordered lists l1 and l2, both of type ’a list,
it returns the sorted combination of both lists
* Write a function split: ’a list -> ’a list * ’a list
which given a list l it splits into two sublists,
(every odd element, every even element)*)
What are lists?
• Nil([]) is a list
• Given an element x and a list l x::l is a list • Nothing else is a list
• []isan′αlist
– Given an element x of type ′α and l of type ′α list
x l is an ′α list (i.e. a list containing elements of type ′α)
• ; are syntactical sugar to separate elements of a list
5.2 Execution
Understand how a program is executed • Operational Semantics
6 Lecture 6 <2017-09-22 Fri>
6.1 Proofs
6.1.1 Demo: lookup & insert
(* Warm up *)
(* Write a function lookup: ’a -> (’a * ’b) list -> ’b option.
Given a key k of type ’a and a list l of key-value pairs,
return the corresponding value v in l (if it exists). *)
(* lookup : ’a -> (’a * ’b) list -> ’b option *)
let rec lookup k l = match l with
| [] -> None
| (k’,v’)::t -> if k=k’ then Some v’ (* If it is the right key, return val*)
else lookup k t;;
(* Write a function insert which
given a key k and a value v and an ordered list l of type (’a * ’b) list
it inserts the key-value pair (k,v) into the list l
preserving the order (ascending keys). *)
(* insert : (’a * ’b) -> (’a * ’b) list -> (’a * ’b) list
insert (k,v) l = l’
Precondition: l is ordered.
Postcondition: l’ is also ordered and we inserted (k,v) at the right position in l*)
(* let rec insert (k,v) l = match l with
* * * * * * *
| [] -> [(k,v)]
(\* k = k’ or k < k’ or k’ < k *\)
| ((k’,v’) as h) :: t ->
if k = k’ then (k,v) :: l
if k’ < k then (k,v) :: l
else h :: insert (k,v) t;;
* let l = [(1,"anne") ; (7,"di")];;
* let l0 = insert (3,"bob") l;;
* insert (3,"tom") l0 ;;
* (\* But now we’ll have 2 entries with the same key *\) *)
(* Undesirable, better to replace the value if its a dictionary*)
let rec insert (k,v) l = match l with
| [] -> [(k,v)]
(* k = k’ or k < k’ or k’ < k *)
| ((k’,v’) as h) :: t ->
if k = k’ then (k,v) :: t (* Replace *)
if k’ < k then (k,v) :: l
else h :: insert (k,v) t;;
(* Personal tail recursive attempt *)
let insert_t (k,v) l =
let rec insert_acc (k,v) l acc = match l with
| [] -> acc @ [(k,v)]
| ((k’,v’) as h) :: t ->
if k = k’ then (k,v) :: t
if k’ < k then (k,v) :: l
else insert_acc (k,v) t (acc @ [h])
• What is the relationship between lookup and insert?
6.1.2 How to prove it?
1. Step 1 We need to understand how programs are executed (operational semantics)
• e ⇓ v expression e evaluates in multiple steps to the value v. (Big-Step)
• e ⇒ e′ expression ee evaluates in one steps to expression e′. (Small-Step (single))
• e =⇒ ∗e′ expression e evaluates in multiple steps to expression e′ (Small-Step (multiple))
For all l, v, k, lookup k (insert k v l) =⇒ ∗ Some v Induction on what?
2. Step 2 P (l) = lookupk (insert(k, v)l) ⇓ Some v
• How to reason inductively about lists? – Analyze their structure!
– The recipe ...
– To prove a property P(l) holds about a list l
∗ Base Case: l = []
· Show P([]) holds
∗ StepCase: l=x::xs
· IH P (xs) (Assume the property P holds for lists smaller
∗ Show P(x :: xs) holds (Show the property P holds for
the original list l)
3. Theorem For all l, v, k, lookup k (insert (k, v)l) =⇒ ∗ Some v
4. Proof Proof by structural inductional on the list l
• Case: l=[]
– lookup k (insert(k,v)[])
By insert program By lookup
– =⇒ lookup k [(k,v)] (same as (k,v)::[]) =⇒ Some v
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com