Programming Languages and Paradigms
School of Computer Science Mc Montreal, Canada
These course notes have been developed by Prof. B. Pientka for COMP302:Programming Lan- guages and Paradigms. DO NOT DISTRIBUTE OUTSIDE THIS CLASS WITHOUT EXPLICIT PER- MISSION. Instructor generated course materials (e.g., handouts, notes, summaries, homeworks, exam questions, etc.) are protected by law and may not be copied or distributed in any form or in any medium without explicit permission of the instructor. Note that infringements of copyright can be subject to follow up by the University under the Code of Student Conduct and Disciplinary Procedures.
Copyright By PowCoder代写 加微信 powcoder
Copyright 2017
1 Basic Concepts 7 1.1 Expressions,Names,Values,andTypes……………… 8 1.2 Variables,Bindings,andFunctions ……………….. 11 1.3 DatatypesandPatternMatching…………………. 13
2 Induction 15 2.1 Mathematicalinduction …………………….. 15 2.2 Completeinduction……………………….. 17 2.3 Structuralinduction ………………………. 18 2.4 Generalizingthestatement …………………… 20 2.5 Conclusion …………………………… 22
3 Higher-Order Functions 25
3.1 PassingFunctions………………………… 26
3.1.1 Example1:Integral …………………… 28
3.1.2 Example2:Halfintervalmethod …………….. 29
3.1.3 Combining Higher-order Functions with Recursive Data-Types . 30
3.2 ReturningFunctions ………………………. 31 3.2.1 Example1:Curryinganduncurrying . . . . . . . . . . . . . . . 31 3.2.2 Example2:Derivative ………………….. 33 3.2.3 Example3:Smoothing………………….. 33 3.2.4 Example 4: Partial evaluation and staged computation . . . . . 33 3.2.5 Example5:Codegeneration……………….. 37
4 References 39 4.1 Binding,Scope …………………………. 39 4.2 ReferenceCells …………………………. 40 4.3 Observation…………………………… 42 4.4 Programmingwellwithreferences ……………….. 43
3 c B. Pientka – Fall 2017
4.4.1 Mutabledatastructures …………………. 44
4.4.2 Destructiveappendandreverse……………… 45
4.5 Closures,ReferencesandObjects ………………… 47
4.6 OtherCommonMutableData-structures …………….. 48
5 Exceptions 51 5.1 It’sallaboutcontrol ………………………. 52
6 Modules 55
6.1 BasicIdea……………………………. 55
6.2 Keepingthingsabstract… ……………………. 57
6.3 Usingabbreviationsformodulenames ……………… 58
6.4 Carefulwithopen ………………………… 58
6.5 Using modules to model currency and bank-client operations . . . . . 59
6.5.1 Modellingdifferentcurrencies………………. 59 6.5.2 Modellingclientandbankoperations. . . . . . . . . . . . . . . 61 6.5.3 Amorerealisticmodelforbankaccounts. . . . . . . . . . . . . 62
7 Fun with functions: Continuations 65
7.1 Atail-recursiveappendfunction…………………. 65
7.2 Controlwithcontinuations……………………. 68
7.2.1 Findingelementinatree ………………… 68 7.2.2 Regularexpressionmatcher ……………….. 69
8 Sometimes it’s good to be lazy 73 8.1 Defininginfiniteobjectsviaobservations . . . . . . . . . . . . . . . . . 75 8.2 Createastreamof1’s ……………………… 76 8.3 Mapfunctiononstreams…………………….. 77 8.4 Writingrecursiveprogramsaboutinfinitedata . . . . . . . . . . . . . . 77 8.5 Addingtwostreams ………………………. 77 8.6 Filter………………………………. 78 8.7 PowerandIntegrateseries……………………. 78 8.8 Fibonacci ……………………………. 79 8.9 SieveofEratosthenes………………………. 80 8.10Lazyfinitelists …………………………. 81 8.11Summary ……………………………. 82
9 Basic Principles of Programming Languages: syntax and semantics of a language 83 9.1 Whataresyntacticallylegalexpressions? . . . . . . . . . . . . . . . . . 84
9.2 Howdoweevaluateanexpression?……………….. 86
9.3 How do we know the definition of evaluation is sensible? . . . .
9.4 Howcanwedescribewell-typedexpressions? . . . . . . . . . .
9.5 Growing the language: variables, let-expressions and functions
9.5.1 Syntaxforvariablesandlet-expressions . . . . . . . . .
9.5.2 Freevariablesandsubstitutions……………… 92 9.5.3 Evaluationoflet-expressions ………………. 94 9.5.4 FunctionsandFunctionapplication. . . . . . . . . . . . . . . . 95
10 Types 99 10.1BasicTypes …………………………… 99 10.2Typingfortuplesandprojections …………………101 10.3 Typingforvariablesandlet-expressions . . . . . . . . . . . . . . . . . 101 10.4 Typingforfunctionsandfunctionapplication . . . . . . . . . . . . . . 103 10.5 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 10.6Propertiesoftypesystems …………………….105
10.7 Polymorphism and type inference . . . . . . . . . . . . . . . . . . . . . 106
10.8 Type variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
10.8.1Twoviewsoftypevariables ………………..107
10.9Typeinference ………………………….109 10.9.1Constraintgeneration …………………..109 10.9.2Solvingtypingconstraints …………………111 10.9.3Typeinferenceinpractice …………………112 10.10PolymorphismandLet-expressions ………………..112
11 Subtyping – An introduction 117
5 c B. Pientka – Fall 2017
…. 88 . . . . 89 …. 91 . . . . 91
6 c B. Pientka – Fall 2017
Basic Concepts in Functional Programming
OCaml is a statically typed functional programming language. What does this mean? – In functional programming languages we write programs using expressions, in par- ticular functions. These functions compute a result by manipulating and analyzing values recursively. OCaml as many ML-like languages (such as SML, Haskell, F#, etc.) facilitates defining recursive data structures and programming functions via pattern matching to analyze them. This often leads to elegant, compact programs. Functional programming is often associated with effect-free programming, i.e. there is no explicit memory allocated or stored, there are no exceptions that would divert the control flow. Functional languages that do not support effects are often called pure. OCaml supports both exception handling as well as state-full computation and hence is an impure functional language.
Functional languages compute a result (i.e. a boolean, an integer, a list, etc.). This is in contrast to procedural or imperative languages where we write methods or procedure; we typically update some state by assigning values to variables or fields, and we observe the result as an effect, i.e. we print the result on standard output or we read and lookup the state and value of a given variable. We will contrast these two approaches more later in the course.
What does statically typed mean? – Types approximate the runtime behaviour of an expression statically, i.e. before running and executing the program. We can also say “Types classify expressions by their values”. Basic types are integers, booleans, floating point numbers, strings or characters. But we can in fact also reason about functions by relating the input and output of a function. And we can then check whether functions are used with the correct types of input and reason about the correct use of the results they compute. Static type checking is a surprisingly effective
7 c B. Pientka – Fall 2017
Chapter 1: Basic Concepts 1.1 Expressions, Names, Values, and Types
technique. It is quick (i.e. for most programs it is polynomial). It can be re-run every time the program changes. It gives precise error messages where the problem might lie and how it might be fixed.
Type checking is conservative. It examines the code statically purely based on its syntactic structure checking whether the given program is meaningful, i.e. its evaluation does something sensible. There are programs which the type checker rejects, although nothing would go wrong during evaluation. But more importantly, if the type checker succeeds, the we are guaranteed that the execution of the program does not lead to a core dump or crash.
Statically typed functional languages like OCaml (but also Java, ML, Haskell, Scala for example) are often called type-safe, i.e. they guarantee that if a program is well-typed, then its execution does not go wrong, i.e. either it produces a value, or it aborts gracefully by raising a runtime exception, or it continues to always steps to a well-defined state. This is a very strong guarantee. As a consequence, typed func- tional programs do not simply crash because of trying to access a null pointer, trying to access a field in an array that is out of bound or trying to write over and beyond a given buffer (buffer overrun). In fact, the heartbleed bug in 2014 is a classic example of a type error and could have been easily avoided.
Let’s begin slowly. We begin using OCaml’s interactive toplevel, aka a read-eval- print loop, that we can use to play around. To start simply type ocaml in a terminal:
[bpientka][taiko][~]$ ocaml
OCaml version 4.02.1
1.1 Expressions, Names, Values, and Types
The most basic expressions are numbers, strings, and booleans.
We can now type expressions followed by ;; to evaluate them.
– : int = 3
– : int = 2
# 3 + 2 ;;
– : int = 5
8 c B. Pientka – Fall 2017
Chapter 1: Basic Concepts 1.1 Expressions, Names, Values, and Types
OCaml says that 3 is an integer and it evaluates to 3. More interestingly, we can ask what the value of the expression 3 + 2 is and OCaml will return 5 and tell us that its type is int.
As you can see, the format of the toplevel output is
If we do not bind the value resulting from evaluating an expression to a name, OCaml will simply write _ instead. We often want to introduce a name to be able to subsequently refer to it. We come back to the issue of binding a little later.
We can not only compute with integers, but also for example with floating point numbers.
– : float = 3.14
# 5.0 /. 2.0;;
– : float = 2.5
# 3.2 +. 4.5;;
– : float = 7.7
Note that we have a different set of operators to compute with floating point numbers. All arithmetic operators have as a postfix a dot. You might wonder whether it is possible to simply say 5 3.2+. The answer is no as you can see below.
# 5 + 3.2;;
Characters 4-7:
5 + 3.2;; ^^^
Error: This expression has type float but an expression was expected of type
Arithmetic operators are not overloaded in OCaml. Overloading operators requires that during runtime we must decide what function (or method) to choose base on the type of the arguments. This requires that we keep types around during runtime and it can be expensive. OCaml does not keep any types around during runtime – this is unlike languages such as Java. In OCaml (as in many functional languages) types are purely used for statically reasoning about the code and optimizing the compilation of the code.
9 c B. Pientka – Fall 2017
Chapter 1: Basic Concepts 1.1 Expressions, Names, Values, and Types
The example illustrate another benefit of types: precise error messages. The type checker tells us that the problem seems to be in the right argument which is passed to the operator for addition.
OCaml has other standard base types such as strings, characters, or booleans.
# “comp302”;;
– : string = “comp302”
– : char = ’a’
– : bool = true
– : bool = false
# true || false ;;
– : bool = true
# true && false;;
– : bool = false
Here we have used boolean operators || (for disjunction) and && (for conjunc- tion). We can also use if-expressions.
# if 0 = 0 then 1.0 else 2.2;;
– : float = 1.
As we mentioned type checking is conservative. Hence there are programs that would produce a value, but the type checker rejects them. This happens for example in the program below:
Characters 23-28:
if 0 = 0 then 1.0 else “AAA”;;
Error: This expression has type string but an expression was expected of type
Clearly the guard 0 = 0 is always true and we would never reach the string ’’AAA’’. We can also say the second branch is dead code. While this is obvious when our guard is of the form 0 = 0, in general this is hard to detect statically. In
10 c B. Pientka – Fall 2017
Chapter 1: Basic Concepts 1.2 Variables, Bindings, and Functions
principle, the guard could be a very complicated call to a function which always hap- pens to produce true for a given input. The type checker makes no assumption about the actual value a guard has, but only verifies that the guard would evaluate to a boolean. Hence the type checker does not know what branch will be taken during runtime and it must check that both branches produce the same kind of value. Why? – Because the if-expression may be part of a larger expression. Reasoning about the type of expressions is compositional.
# (if 0 = 0 then 1.0 else 2.2) +. 3.3;;
– : float = 4.3
As mentioned earlier, if the type checker accepts the program, executing it ei- ther yields a value or the program is aborted gracefully, if it reaches a state that is identified as a run-time error. An example of such a run-time error is division by zero.
Exception: Division_by_zero.
Attempting to divide 3 by 0 will pass the type checker, because the type checker simply checks whether the two arguments given to the division operator are integers. This is the case. During runtime we note that we are dividing by zero, and the evaluator raises a built-in exception Division-by-zero.
1.2 Variables, Bindings, and Functions
A central concept in a programming language are variables and the scope of vari- ables. In OCaml we can declare a variable at the top-level (i.e. a global declaration) using a let-expression of the form let
# let pi = 3.14;;
val pi : float = 3.14
Here pi is the name of the variable and we bind to the name the value 3.14. Note, because OCaml is a call-by-value language, we bind values to variable names – not expressions. For example as a result of evaluating the following expression, we bind the variable name x to the value 9.
11 c B. Pientka – Fall 2017
Chapter 1: Basic Concepts 1.2 Variables, Bindings, and Functions
# let x = 3 * 3;;
val x : int = 9
A variable binding is not an assignment. We simply establish a relation between a name and a value. There is no state being allocated and this association or relation cannot be updated or changed. Once the relationship is done it is fixed. We can only overshadow a given binding, not update it.
# let x = 42;;
val x : int = 42
For example by establishing again a binding between the variable name x and the value 42, we now have two bindings for x on the binding stack. The last binding we pushed onto that stack bind x to 42. When we look up the value of a variable, we look it up in the stack and we pick the one that was establish most recently, i.e. the binding that is at the top. The earlier binding is overshadowed.
A garbage collector might decide to remove the earlier binding for efficiency rea- sons, it determines there is no other code that still uses it.
We can also introduce scoped variable bindings or local bindings as illustrated in the following example.
# let m = 3 in
let n = m * m in
let k = m * m in
The
12 c B. Pientka – Fall 2017
– : int = 81
We use a let-expression that has the following structure:
let
Chapter 1: Basic Concepts 1.3 Datatypes and Pattern Matching
We also say the scope of the variable
How do global and local bindings interact? – Local bindings are only temporary. Hence, they may overshadow temporarily a given global binding. Here is an example:
# let k = 4;;
val k : int = 4
# let k = 3 in k * k ;;
– : int = 9
– : int = 4
When we evaluate the body k * k in the second let-expression, we have two bindings for the name k: the first one bound k to 4; the second one and the most recent one that is on top of the binding stack says x is bound to 3. When we evaluate k * k, we look up the most recent binding for k and obtain 3. Hence we return the value 9. When we then ask what is the value of k we obtain 4, as the local binding between k and 3 was removed from the binding stack. This clearly illustrates that variables bindings are not updated – once they are made they persist.
[Explanation about functions and tail recursion to be added]
1.3 Datatypes and Pattern Matching
Often it is useful to define a collection of elements or objects and not encode all data we are working with using our base types of integers, floats or strings. For example, we might want to model a simple card game. As a first step, we want to define the suit and rank present in the game. In OCaml, we define a finite, unordered collection of elements using a (non-recursive) data type definition. Here we define a new type suit that contains the elements Clubs, Spades, Hearts, and Diamonds.
1 type suit = Clubs | Spades | Hearts | Diamonds
We also say Clubs, Spades, Hearts, and Diamonds inhabit the type suit. Often, we simply say Clubs, Spades, Hearts, and Diamonds is of type suit.
When we define a collection of elements the order does not matter. Further, OCaml requires that each element begins with a capital letter.
Elements of a given type are defined by constructors, i.e. constants that allow us to construct elements of a given type. In our previous definition of our type suit we have four constructors, namely Clubs, Spades, Hearts, and Diamonds.
13 c B. Pientka – Fall 2017
1 2 3 4 5 6
Chapter 1: Basic Concepts 1.3 Datatypes and Pattern Matching
How do we write programs about elements of type suit? – The answer is pattern matching using a match-expression.
match
|
|
|
We call the expression that we analyze the scrutinee. Patterns characterize the shape of values the scrutinee might have by considering the type of the scrutinee. Let’s make this more precise by looking at an example. We want to write a function dom that takes in a pair s1 and s2 of suit. If s beats of is equal to suit s2 we return true – otherwise we return false. We will use the following ordering on suits:
Spades ¿ Hearts ¿ Diamonds ¿ Clubs The type of the function dom is suit * suit -> bool.
let rec dom (s1, s2) = match (s1, s2) with
| (Spades, _)
| (Hearts, Diamonds) | (Hearts, Clubs)
| (Diamonds, Clubs) | (s1, s2)
-> true ->s1= s2
Please read the datatypes.ml and trees.ml for a longer and more detail ed description of the examples discussed in class.
14 c B. Pientka – Fall 2017
As an example, let us consider the following program power.
15 c B. Pientka – Fall 2017
Chapter 2 Induction
“On theories such as these we cannot rely. Proof we need. Proof!” Yoda, Jedi Master
In this chapter, we will briefly discuss how to prove properties about ML programs using induction. Proofs by induction are ubiquitous in the theory of programming languages, as in most of computer science. Many of these proofs are based on one of the following principles: mathematical induction and structural induction. In this chapter we will discuss these most common induction principles.
2.1 Mathematical induction
Mathematical induction is the simplest form of induction. When we try to prove a pro
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com