02157

Functional
Program-
ming

02157 Functional Programming Michael R. Ha

Lecture 1: Introduction and Getting Started

Michael R. Hansen

1 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 02157
Functional
Program-
ming

Michael R. Ha
WELCOME to
02157 Functional Programming

Teacher: Michael R. Hansen

DTU Informatics, mrh@[Link]

Teaching assistant: Phan Anh Dung, PhD Student.

Søren Olofsson, master’s student
Both at DTU Informatics

Homepage: [Link]/courses/02157

2 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Today: Friday, September 7.

02157
Functional
Program-
ming

Michael R. Ha
• Introduction to functional programming and F#
(341.23 — here)
• about 9:15 – lecture notes can be bought here.
• Make your first programs in the databar
(341 Rooms: 015 and 019 — E-databar)
• Introduction to lists in F#
(341.23 — here)
• Computations with polynomials in F#
(341 Rooms: 015 and 019 — E-databar)

By noon you have solved a non-trivial problem using F#

3 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Today: Friday, September 7.

02157
Functional
Program-
ming

Michael R. Ha
• Introduction to functional programming and F#
(341.23 — here)
• about 9:15 – lecture notes can be bought here.
• Make your first programs in the databar
(341 Rooms: 015 and 019 — E-databar)
• Introduction to lists in F#
(341.23 — here)
• Computations with polynomials in F#
(341 Rooms: 015 and 019 — E-databar)

By noon you have solved a non-trivial problem using F#

4 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Practical Matters

02157
Functional
Program-
ming
• Textbook: Functional Programming using F#, Chapters 1-7, 9.
Michael R. Ha
by Michael R. Hansen and Hans Rischel.
Can be bought at the reception of DTU Informatics. Price 100 kr.
Published by Cambridge University Press the coming winter.

• F# is an open-source functional language integrated in the

Visual Studio development platform and with access to all
features in the .NET program library. The language is also
supported on Linux and MAC systems using the Mono platform.

• We use F# on the Windows platform in the E-databar.

• Look at homepage concerning installations for your own PC

(Windows, Linux or Mac).

5 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Practical Matters

02157
Functional
Program-
ming
• Textbook: Functional Programming using F#, Chapters 1-7, 9.
Michael R. Ha
by Michael R. Hansen and Hans Rischel.
Can be bought at the reception of DTU Informatics. Price 100 kr.
Published by Cambridge University Press the coming winter.

• F# is an open-source functional language integrated in the

Visual Studio development platform and with access to all
features in the .NET program library. The language is also
supported on Linux and MAC systems using the Mono platform.

• We use F# on the Windows platform in the E-databar.

• Look at homepage concerning installations for your own PC

(Windows, Linux or Mac).

6 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Practical Matters

02157
Functional
Program-
ming
• Textbook: Functional Programming using F#, Chapters 1-7, 9.
Michael R. Ha
by Michael R. Hansen and Hans Rischel.
Can be bought at the reception of DTU Informatics. Price 100 kr.
Published by Cambridge University Press the coming winter.

• F# is an open-source functional language integrated in the

Visual Studio development platform and with access to all
features in the .NET program library. The language is also
supported on Linux and MAC systems using the Mono platform.

• We use F# on the Windows platform in the E-databar.

• Look at homepage concerning installations for your own PC

(Windows, Linux or Mac).

7 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Practical Matters

02157
Functional
Program-
ming
• Textbook: Functional Programming using F#, Chapters 1-7, 9.
Michael R. Ha
by Michael R. Hansen and Hans Rischel.
Can be bought at the reception of DTU Informatics. Price 100 kr.
Published by Cambridge University Press the coming winter.

• F# is an open-source functional language integrated in the

Visual Studio development platform and with access to all
features in the .NET program library. The language is also
supported on Linux and MAC systems using the Mono platform.

• We use F# on the Windows platform in the E-databar.

• Look at homepage concerning installations for your own PC

(Windows, Linux or Mac).

8 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Imperative models

02157
Functional
Program-
ming

Michael R. Ha
• Imperative models of computations are expressed in terms of
states and sequences of state-changing operations

Example:

i := 0;
s := 0;
while i < length(A)
do s := s+A[i];
i := i+1
od

An imperative model describes how a solution is obtained

9 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Imperative models

02157
Functional
Program-
ming

Michael R. Ha
• Imperative models of computations are expressed in terms of
states and sequences of state-changing operations

Example:

i := 0;
s := 0;
while i < length(A)
do s := s+A[i];
i := i+1
od

An imperative model describes how a solution is obtained

10 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Object-oriented models

02157
Functional
Program-
ming

Michael R. Ha

• An object is characterized by a state and an interface specifying

a collection of state-changing operations.
• Object-oriented models of computations are expressed in terms
of a collection of objects which exchange messages by using
interface operations.

Object-oriented models add structure to imperative models

An object-oriented model describes how a solution is obtained

11 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Object-oriented models

02157
Functional
Program-
ming

Michael R. Ha

• An object is characterized by a state and an interface specifying

a collection of state-changing operations.
• Object-oriented models of computations are expressed in terms
of a collection of objects which exchange messages by using
interface operations.

Object-oriented models add structure to imperative models

An object-oriented model describes how a solution is obtained

12 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Declarative models

In declarative models focus is on what a solution is. 02157

Functional
Program-
ming
• Logical programming (02156 Logical Systems and Logical Michael R. Ha
Programming)
• Programs are (typically) expressed in a fragment of first-order logic.
The formulas have a standard meaning, as well as a procedural
interpretation based on logical inferences.

• Functional programming
• A program is expressed as a mathematical function
f :A→B
and function applications guide computations.

Some advantages
• fast prototyping based on abstract concepts
• more advanced applications are within reach
• Supplement modelling and problem solving techniques
• Execute in parallel on multi-core platforms
F# is as efficient as C#
13 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Declarative models

In declarative models focus is on what a solution is. 02157

Functional
Program-
ming
• Logical programming (02156 Logical Systems and Logical Michael R. Ha
Programming)
• Programs are (typically) expressed in a fragment of first-order logic.
The formulas have a standard meaning, as well as a procedural
interpretation based on logical inferences.

• Functional programming
• A program is expressed as a mathematical function
f :A→B
and function applications guide computations.

Some advantages
• fast prototyping based on abstract concepts
• more advanced applications are within reach
• Supplement modelling and problem solving techniques
• Execute in parallel on multi-core platforms
F# is as efficient as C#
14 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Declarative models

In declarative models focus is on what a solution is. 02157

Functional
Program-
ming
• Logical programming (02156 Logical Systems and Logical Michael R. Ha
Programming)
• Programs are (typically) expressed in a fragment of first-order logic.
The formulas have a standard meaning, as well as a procedural
interpretation based on logical inferences.

• Functional programming
• A program is expressed as a mathematical function
f :A→B
and function applications guide computations.

Some advantages
• fast prototyping based on abstract concepts
• more advanced applications are within reach
• Supplement modelling and problem solving techniques
• Execute in parallel on multi-core platforms
F# is as efficient as C#
15 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Some functional programming background

02157
Functional
In functional programming, the model of computation is the Program-
ming
application of functions to arguments. no side-effects Michael R. Ha

• Introduction of λ-calculus around 1930 by Church and Kleene

when investigating function definition, function application,
recursion and computable functions. For example, f (x) = x + 2
is represented by λx.x + 2.

• Introduction of the type-less functional-like programming

language LISP was developed by McCarthy in the late 1950s.

• Introduction of the ”variable-free” programming language FP

(Backus 1977), by providing a rich collection of functionals
(combining forms for functions).

• Introduction of functional languages with a strong type system

like ML (by Milner) and Miranda (by Turner) in the 1970s.

16 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Some functional programming background

02157
Functional
In functional programming, the model of computation is the Program-
ming
application of functions to arguments. no side-effects Michael R. Ha

• Introduction of λ-calculus around 1930 by Church and Kleene

when investigating function definition, function application,
recursion and computable functions. For example, f (x) = x + 2
is represented by λx.x + 2.

• Introduction of the type-less functional-like programming

language LISP was developed by McCarthy in the late 1950s.

• Introduction of the ”variable-free” programming language FP

(Backus 1977), by providing a rich collection of functionals
(combining forms for functions).

• Introduction of functional languages with a strong type system

like ML (by Milner) and Miranda (by Turner) in the 1970s.

17 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Some functional programming background

02157
Functional
In functional programming, the model of computation is the Program-
ming
application of functions to arguments. no side-effects Michael R. Ha

• Introduction of λ-calculus around 1930 by Church and Kleene

when investigating function definition, function application,
recursion and computable functions. For example, f (x) = x + 2
is represented by λx.x + 2.

• Introduction of the type-less functional-like programming

language LISP was developed by McCarthy in the late 1950s.

• Introduction of the ”variable-free” programming language FP

(Backus 1977), by providing a rich collection of functionals
(combining forms for functions).

• Introduction of functional languages with a strong type system

like ML (by Milner) and Miranda (by Turner) in the 1970s.

18 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Some functional programming background

02157
Functional
In functional programming, the model of computation is the Program-
ming
application of functions to arguments. no side-effects Michael R. Ha

• Introduction of λ-calculus around 1930 by Church and Kleene

when investigating function definition, function application,
recursion and computable functions. For example, f (x) = x + 2
is represented by λx.x + 2.

• Introduction of the type-less functional-like programming

language LISP was developed by McCarthy in the late 1950s.

• Introduction of the ”variable-free” programming language FP

(Backus 1977), by providing a rich collection of functionals
(combining forms for functions).

• Introduction of functional languages with a strong type system

like ML (by Milner) and Miranda (by Turner) in the 1970s.

19 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Some background of the “SML-family”

02157
• Standard Meta Language (SML) was originally designed for Functional
Program-
theorem proving ming

Logic for Computable Functions (Edinburgh LCF) Michael R. Ha

Gordon, Milner, Wadsworth (1977)

• High quality compilers, e.g. Standard ML of New Jersey and

Moscow ML, based on a formal semantics
Milner, Tofte, Harper, MacQueen 1990 & 1997

• SML-like systems (SML, OCAML, F#, . . .) have now applications

far away from its origins
Compilers, Artificial Intelligence, Web-applications, Financial
sector, . . .

• F# is now integrated in the .net environment

• Declarative aspects are sneaking into more ”main stream

languages”

• Often used to teach high-level programming concepts

20 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Some background of the “SML-family”

02157
• Standard Meta Language (SML) was originally designed for Functional
Program-
theorem proving ming

Logic for Computable Functions (Edinburgh LCF) Michael R. Ha

Gordon, Milner, Wadsworth (1977)

• High quality compilers, e.g. Standard ML of New Jersey and

Moscow ML, based on a formal semantics
Milner, Tofte, Harper, MacQueen 1990 & 1997

• SML-like systems (SML, OCAML, F#, . . .) have now applications

far away from its origins
Compilers, Artificial Intelligence, Web-applications, Financial
sector, . . .

• F# is now integrated in the .net environment

• Declarative aspects are sneaking into more ”main stream

languages”

• Often used to teach high-level programming concepts

21 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Some background of the “SML-family”

02157
• Standard Meta Language (SML) was originally designed for Functional
Program-
theorem proving ming

Logic for Computable Functions (Edinburgh LCF) Michael R. Ha

Gordon, Milner, Wadsworth (1977)

• High quality compilers, e.g. Standard ML of New Jersey and

Moscow ML, based on a formal semantics
Milner, Tofte, Harper, MacQueen 1990 & 1997

• SML-like systems (SML, OCAML, F#, . . .) have now applications

far away from its origins
Compilers, Artificial Intelligence, Web-applications, Financial
sector, . . .

• F# is now integrated in the .net environment

• Declarative aspects are sneaking into more ”main stream

languages”

• Often used to teach high-level programming concepts

22 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Some background of the “SML-family”

02157
• Standard Meta Language (SML) was originally designed for Functional
Program-
theorem proving ming

Logic for Computable Functions (Edinburgh LCF) Michael R. Ha

Gordon, Milner, Wadsworth (1977)

• High quality compilers, e.g. Standard ML of New Jersey and

Moscow ML, based on a formal semantics
Milner, Tofte, Harper, MacQueen 1990 & 1997

• SML-like systems (SML, OCAML, F#, . . .) have now applications

far away from its origins
Compilers, Artificial Intelligence, Web-applications, Financial
sector, . . .

• F# is now integrated in the .net environment

• Declarative aspects are sneaking into more ”main stream

languages”

• Often used to teach high-level programming concepts

23 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Some background of the “SML-family”

02157
• Standard Meta Language (SML) was originally designed for Functional
Program-
theorem proving ming

Logic for Computable Functions (Edinburgh LCF) Michael R. Ha

Gordon, Milner, Wadsworth (1977)

• High quality compilers, e.g. Standard ML of New Jersey and

Moscow ML, based on a formal semantics
Milner, Tofte, Harper, MacQueen 1990 & 1997

• SML-like systems (SML, OCAML, F#, . . .) have now applications

far away from its origins
Compilers, Artificial Intelligence, Web-applications, Financial
sector, . . .

• F# is now integrated in the .net environment

• Declarative aspects are sneaking into more ”main stream

languages”

• Often used to teach high-level programming concepts

24 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Some background of the “SML-family”

02157
• Standard Meta Language (SML) was originally designed for Functional
Program-
theorem proving ming

Logic for Computable Functions (Edinburgh LCF) Michael R. Ha

Gordon, Milner, Wadsworth (1977)

• High quality compilers, e.g. Standard ML of New Jersey and

Moscow ML, based on a formal semantics
Milner, Tofte, Harper, MacQueen 1990 & 1997

• SML-like systems (SML, OCAML, F#, . . .) have now applications

far away from its origins
Compilers, Artificial Intelligence, Web-applications, Financial
sector, . . .

• F# is now integrated in the .net environment

• Declarative aspects are sneaking into more ”main stream

languages”

• Often used to teach high-level programming concepts

25 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Overview of the course

02157
Functional
Program-
• Functional programming concepts and techniques ming

• A model-based programming approach using a functional Michael R. Ha

language with a strong type system.

• Program correctness, including structural induction and
well-founded induction

Fun with a variety of applications, such as

• a library for piecewise linear curves – with applications
• a Sudoko solver
• an interpreter for a simple programming language
• a lambda-calculus interpreter
• a model checker for CTL – a temporal logic
• ...

Homepage for the course: [Link]/courses/02157

26 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Overview of the course

02157
Functional
Program-
• Functional programming concepts and techniques ming

• A model-based programming approach using a functional Michael R. Ha

language with a strong type system.

• Program correctness, including structural induction and
well-founded induction

Fun with a variety of applications, such as

• a library for piecewise linear curves – with applications
• a Sudoko solver
• an interpreter for a simple programming language
• a lambda-calculus interpreter
• a model checker for CTL – a temporal logic
• ...

Homepage for the course: [Link]/courses/02157

27 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Overview of the course

02157
Functional
Program-
• Functional programming concepts and techniques ming

• A model-based programming approach using a functional Michael R. Ha

language with a strong type system.

• Program correctness, including structural induction and
well-founded induction

Fun with a variety of applications, such as

• a library for piecewise linear curves – with applications
• a Sudoko solver
• an interpreter for a simple programming language
• a lambda-calculus interpreter
• a model checker for CTL – a temporal logic
• ...

Homepage for the course: [Link]/courses/02157

28 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 A major goal

02157
Functional
Teach abstraction (not a concrete programming language) Program-
ming
• Modelling
Michael R. Ha
• Design
• Programming

Why?
More complex problems can be solved in an succinct, elegant and
understandable manner

How?
Solving a broad class of problems showing the applicability of the
theory, concepts, techniques and tools.

Functional programming techniques once mastered are useful for the

design of programs in other programming paradigms as well.

29 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 A major goal

02157
Functional
Teach abstraction (not a concrete programming language) Program-
ming
• Modelling
Michael R. Ha
• Design
• Programming

Why?
More complex problems can be solved in an succinct, elegant and
understandable manner

How?
Solving a broad class of problems showing the applicability of the
theory, concepts, techniques and tools.

Functional programming techniques once mastered are useful for the

design of programs in other programming paradigms as well.

30 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 A major goal

02157
Functional
Teach abstraction (not a concrete programming language) Program-
ming
• Modelling
Michael R. Ha
• Design
• Programming

Why?
More complex problems can be solved in an succinct, elegant and
understandable manner

How?
Solving a broad class of problems showing the applicability of the
theory, concepts, techniques and tools.

Functional programming techniques once mastered are useful for the

design of programs in other programming paradigms as well.

31 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 A major goal

02157
Functional
Teach abstraction (not a concrete programming language) Program-
ming
• Modelling
Michael R. Ha
• Design
• Programming

Why?
More complex problems can be solved in an succinct, elegant and
understandable manner

How?
Solving a broad class of problems showing the applicability of the
theory, concepts, techniques and tools.

Functional programming techniques once mastered are useful for the

design of programs in other programming paradigms as well.

32 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 F# supports

02157
Functional
Program-
ming
• Functions as first class citizens Michael R. Ha

• Structured values like lists, trees, . . .

• Strong and flexible type discipline, including

type inference and polymorphism

• Imperative and object-oriented programming

assignments, loops, arrays, objects, Input/Output, etc.

Programming as a modelling discipline

• High-level programming, declarative programming, executable
declarative specifications B, Z, VDM, RAISE
• Fast time-to-market

33 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 F# supports

02157
Functional
Program-
ming
• Functions as first class citizens Michael R. Ha

• Structured values like lists, trees, . . .

• Strong and flexible type discipline, including

type inference and polymorphism

• Imperative and object-oriented programming

assignments, loops, arrays, objects, Input/Output, etc.

Programming as a modelling discipline

• High-level programming, declarative programming, executable
declarative specifications B, Z, VDM, RAISE
• Fast time-to-market

34 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 F# supports

02157
Functional
Program-
ming
• Functions as first class citizens Michael R. Ha

• Structured values like lists, trees, . . .

• Strong and flexible type discipline, including

type inference and polymorphism

• Imperative and object-oriented programming

assignments, loops, arrays, objects, Input/Output, etc.

Programming as a modelling discipline

• High-level programming, declarative programming, executable
declarative specifications B, Z, VDM, RAISE
• Fast time-to-market

35 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 F# supports

02157
Functional
Program-
ming
• Functions as first class citizens Michael R. Ha

• Structured values like lists, trees, . . .

• Strong and flexible type discipline, including

type inference and polymorphism

• Imperative and object-oriented programming

assignments, loops, arrays, objects, Input/Output, etc.

Programming as a modelling discipline

• High-level programming, declarative programming, executable
declarative specifications B, Z, VDM, RAISE
• Fast time-to-market

36 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 F# supports

02157
Functional
Program-
ming
• Functions as first class citizens Michael R. Ha

• Structured values like lists, trees, . . .

• Strong and flexible type discipline, including

type inference and polymorphism

• Imperative and object-oriented programming

assignments, loops, arrays, objects, Input/Output, etc.

Programming as a modelling discipline

• High-level programming, declarative programming, executable
declarative specifications B, Z, VDM, RAISE
• Fast time-to-market

37 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Course context

02157
Functional
Prerequisites for 02157: Programming in an Program-
imperative/object-oriented language, discrete mathematics, ming

algorithms and data structure, as obtained, for example, from the Michael R. Ha

bachelor programme in Software Technology.

Successor course of 02157:

02257 Applied functional programming
3-weeks period January
An extension of 02157 that aims at an effective use of functional
programming in connection with courses and projects at the [Link].
programme in computer science and engineering, and in industrial
applications.
• Computer science applications. Interpreter for a programming
language, for example.
• “Practical applications”. Involving a database, for example.
• Functional pearls. Monadic parsing, for example.

38 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Course context

02157
Functional
Prerequisites for 02157: Programming in an Program-
imperative/object-oriented language, discrete mathematics, ming

algorithms and data structure, as obtained, for example, from the Michael R. Ha

bachelor programme in Software Technology.

Successor course of 02157:

02257 Applied functional programming
3-weeks period January
An extension of 02157 that aims at an effective use of functional
programming in connection with courses and projects at the [Link].
programme in computer science and engineering, and in industrial
applications.
• Computer science applications. Interpreter for a programming
language, for example.
• “Practical applications”. Involving a database, for example.
• Functional pearls. Monadic parsing, for example.

39 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Overview of Getting Started

02157
Functional
Program-
Main functional ingredients of F#: ming

• The interactive environment Michael R. Ha

• Values, expressions, types, patterns

• Declarations of values and recursive functions
• Binding, environment and evaluation
• Type inference

GOAL: By the end of this first part you have constructed succinct,
elegant and understandable F# programs, e.g. for
Pn
• sum(m, n) = i=m i

• Fibonacci numbers (F0 = 0, F1 = 1, Fn = Fn−1 + Fn−2 )

 
n
• Binomial coefficients
k

40 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Overview of Getting Started

02157
Functional
Program-
Main functional ingredients of F#: ming

• The interactive environment Michael R. Ha

• Values, expressions, types, patterns

• Declarations of values and recursive functions
• Binding, environment and evaluation
• Type inference

GOAL: By the end of this first part you have constructed succinct,
elegant and understandable F# programs, e.g. for
Pn
• sum(m, n) = i=m i

• Fibonacci numbers (F0 = 0, F1 = 1, Fn = Fn−1 + Fn−2 )

 
n
• Binomial coefficients
k

41 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 The Interactive Environment

02157
Functional
Program-
ming

2*3 + 4;; ⇐ Input to the F# system Michael R. Ha

val it : int = 10 ⇐ Answer from the F# system

• The keyword val indicates a value is computed

• The integer 10 is the computed value
• int is the type of the computed value
• The identifier it names the (last) computed value

The notion binding explains which entities are named by identifiers.

it 7→ 10 reads: “it is bound to 10”

42 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 The Interactive Environment

02157
Functional
Program-
ming

2*3 + 4;; ⇐ Input to the F# system Michael R. Ha

val it : int = 10 ⇐ Answer from the F# system

• The keyword val indicates a value is computed

• The integer 10 is the computed value
• int is the type of the computed value
• The identifier it names the (last) computed value

The notion binding explains which entities are named by identifiers.

it 7→ 10 reads: “it is bound to 10”

43 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 The Interactive Environment

02157
Functional
Program-
ming

2*3 + 4;; ⇐ Input to the F# system Michael R. Ha

val it : int = 10 ⇐ Answer from the F# system

• The keyword val indicates a value is computed

• The integer 10 is the computed value
• int is the type of the computed value
• The identifier it names the (last) computed value

The notion binding explains which entities are named by identifiers.

it 7→ 10 reads: “it is bound to 10”

44 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 The Interactive Environment

02157
Functional
Program-
ming

2*3 + 4;; ⇐ Input to the F# system Michael R. Ha

val it : int = 10 ⇐ Answer from the F# system

• The keyword val indicates a value is computed

• The integer 10 is the computed value
• int is the type of the computed value
• The identifier it names the (last) computed value

The notion binding explains which entities are named by identifiers.

it 7→ 10 reads: “it is bound to 10”

45 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Value Declarations

02157
Functional
Program-
ming
A value declaration has the form: let identifier = expression
Michael R. Ha

let price = 25 * 5;; ⇐ A declaration as input

val price : int = 125 ⇐ Answer from the F# system

The effect of a declaration is a binding: price 7→ 125

Bound identifiers can be used in expressions and declarations, e.g.

let newPrice = 2*price;; A collection of bindings

val newPrice : int = 250  
price 7→ 125
 newPrice 7→ 250 
newPrice > 500;;
it 7→ false
val it : bool = false
is called an environment

46 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Value Declarations

02157
Functional
Program-
ming
A value declaration has the form: let identifier = expression
Michael R. Ha

let price = 25 * 5;; ⇐ A declaration as input

val price : int = 125 ⇐ Answer from the F# system

The effect of a declaration is a binding: price 7→ 125

Bound identifiers can be used in expressions and declarations, e.g.

let newPrice = 2*price;; A collection of bindings

val newPrice : int = 250  
price 7→ 125
 newPrice 7→ 250 
newPrice > 500;;
it 7→ false
val it : bool = false
is called an environment

47 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Value Declarations

02157
Functional
Program-
ming
A value declaration has the form: let identifier = expression
Michael R. Ha

let price = 25 * 5;; ⇐ A declaration as input

val price : int = 125 ⇐ Answer from the F# system

The effect of a declaration is a binding: price 7→ 125

Bound identifiers can be used in expressions and declarations, e.g.

let newPrice = 2*price;; A collection of bindings

val newPrice : int = 250  
price 7→ 125
 newPrice 7→ 250 
newPrice > 500;;
it 7→ false
val it : bool = false
is called an environment

48 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Function Declarations 1: let f x = e

02157
Functional
Declaration of the circle area function: Program-
ming
let circleArea r = [Link] * r * r;; Michael R. Ha

• [Link] is a program library

• PI is an identifier (with type float) for π in [Link]

The type is automatically inferred in the answer:

val circleArea : float -> float

Applications of the function:

circleArea 1.0;; (* this is a comment *)
val it : float = 3.141592654

circleArea(3.2);; // A comment: optional brackets

val it : float = 32.16990877

49 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Function Declarations 1: let f x = e

02157
Functional
Declaration of the circle area function: Program-
ming
let circleArea r = [Link] * r * r;; Michael R. Ha

• [Link] is a program library

• PI is an identifier (with type float) for π in [Link]

The type is automatically inferred in the answer:

val circleArea : float -> float

Applications of the function:

circleArea 1.0;; (* this is a comment *)
val it : float = 3.141592654

circleArea(3.2);; // A comment: optional brackets

val it : float = 32.16990877

50 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Function Declarations 1: let f x = e

02157
Functional
Declaration of the circle area function: Program-
ming
let circleArea r = [Link] * r * r;; Michael R. Ha

• [Link] is a program library

• PI is an identifier (with type float) for π in [Link]

The type is automatically inferred in the answer:

val circleArea : float -> float

Applications of the function:

circleArea 1.0;; (* this is a comment *)
val it : float = 3.141592654

circleArea(3.2);; // A comment: optional brackets

val it : float = 32.16990877

51 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Anonymous functions: by example (1)

An anonymous function computing the number of days in a month: 02157

Functional
Program-
function ming
| 1 -> 31 // January Michael R. Ha
| 2 -> 28 // February // not a leap year
| 3 -> 31 // March
| 4 -> 30 // April
| 5 -> 31 // May
| 6 -> 30 // June
| 7 -> 31 // July
| 8 -> 31 // August
| 9 -> 30 // September
| 10 -> 31 // October
| 11 -> 30 // November
| 12 -> 31;;// December
... warning ... Incomplete pattern matches ...
val it : int -> int = <fun:clo@17-2>
it 2;;
val it : int = 28
A function expression with a pattern for every month
52 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Anonymous functions: by example (1)

An anonymous function computing the number of days in a month: 02157

Functional
Program-
function ming
| 1 -> 31 // January Michael R. Ha
| 2 -> 28 // February // not a leap year
| 3 -> 31 // March
| 4 -> 30 // April
| 5 -> 31 // May
| 6 -> 30 // June
| 7 -> 31 // July
| 8 -> 31 // August
| 9 -> 30 // September
| 10 -> 31 // October
| 11 -> 30 // November
| 12 -> 31;;// December
... warning ... Incomplete pattern matches ...
val it : int -> int = <fun:clo@17-2>
it 2;;
val it : int = 28
A function expression with a pattern for every month
53 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Anonymous functions: by example (1)

An anonymous function computing the number of days in a month: 02157

Functional
Program-
function ming
| 1 -> 31 // January Michael R. Ha
| 2 -> 28 // February // not a leap year
| 3 -> 31 // March
| 4 -> 30 // April
| 5 -> 31 // May
| 6 -> 30 // June
| 7 -> 31 // July
| 8 -> 31 // August
| 9 -> 30 // September
| 10 -> 31 // October
| 11 -> 30 // November
| 12 -> 31;;// December
... warning ... Incomplete pattern matches ...
val it : int -> int = <fun:clo@17-2>
it 2;;
val it : int = 28
A function expression with a pattern for every month
54 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Anonymous functions: by example (2)

02157
Functional
Program-
One wildcard pattern can cover many similar cases: ming

Michael R. Ha
function
| 2 -> 28 // February
| 4 -> 30 // April
| 6 -> 30 // June
| 9 -> 30 // September
| 11 -> 30 // November
| _ -> 31;;// All other months

An even more succinct definition can be given using an or-pattern:

function
| 2 -> 28 // February
| 4|6|9|11 -> 30 // April, June, September, November
| _ -> 31 // All other months
;;

55 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Anonymous functions: by example (2)

02157
Functional
Program-
One wildcard pattern can cover many similar cases: ming

Michael R. Ha
function
| 2 -> 28 // February
| 4 -> 30 // April
| 6 -> 30 // June
| 9 -> 30 // September
| 11 -> 30 // November
| _ -> 31;;// All other months

An even more succinct definition can be given using an or-pattern:

function
| 2 -> 28 // February
| 4|6|9|11 -> 30 // April, June, September, November
| _ -> 31 // All other months
;;

56 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Recursion. Example n! = 1 · 2 · . . . · n, n ≥ 0

02157
Functional
Program-
ming

Michael R. Ha
Mathematical definition: recursion formula
0! = 1 (i)
n! = n · (n − 1)!, for n > 0 (ii)

Computation:
3!
= 3 · (3 − 1)! (ii)
= 3 · 2 · (2 − 1)! (ii)
= 3 · 2 · 1 · (1 − 1)! (ii)
= 3·2·1·1 (i)
= 6

57 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Recursion. Example n! = 1 · 2 · . . . · n, n ≥ 0

02157
Functional
Program-
ming

Michael R. Ha
Mathematical definition: recursion formula
0! = 1 (i)
n! = n · (n − 1)!, for n > 0 (ii)

Computation:
3!
= 3 · (3 − 1)! (ii)
= 3 · 2 · (2 − 1)! (ii)
= 3 · 2 · 1 · (1 − 1)! (ii)
= 3·2·1·1 (i)
= 6

58 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Recursive declaration. Example n!

02157
Functional
Program-
ming
Function declaration:
Michael R. Ha

let rec fact = function

| 0 -> 1 (* i *)
| n -> n * fact(n-1);; (* ii *)
val fact : int -> int
Evaluation:
fact(3)
3 ∗ fact(3 − 1) (ii) [n 7→ 3]
3 ∗ 2 ∗ fact(2 − 1) (ii) [n 7→ 2]
3 ∗ 2 ∗ 1 ∗ fact(1 − 1) (ii) [n 7→ 1]
3∗2∗1∗1 (i) [n 7→ 0]
6

e1 e2 reads: e1 evaluates to e2

59 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Recursive declaration. Example n!

02157
Functional
Program-
ming
Function declaration:
Michael R. Ha

let rec fact = function

| 0 -> 1 (* i *)
| n -> n * fact(n-1);; (* ii *)
val fact : int -> int
Evaluation:
fact(3)
3 ∗ fact(3 − 1) (ii) [n 7→ 3]
3 ∗ 2 ∗ fact(2 − 1) (ii) [n 7→ 2]
3 ∗ 2 ∗ 1 ∗ fact(1 − 1) (ii) [n 7→ 1]
3∗2∗1∗1 (i) [n 7→ 0]
6

e1 e2 reads: e1 evaluates to e2

60 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Recursive declaration. Example n!

02157
Functional
Program-
ming
Function declaration:
Michael R. Ha

let rec fact = function

| 0 -> 1 (* i *)
| n -> n * fact(n-1);; (* ii *)
val fact : int -> int
Evaluation:
fact(3)
3 ∗ fact(3 − 1) (ii) [n 7→ 3]
3 ∗ 2 ∗ fact(2 − 1) (ii) [n 7→ 2]
3 ∗ 2 ∗ 1 ∗ fact(1 − 1) (ii) [n 7→ 1]
3∗2∗1∗1 (i) [n 7→ 0]
6

e1 e2 reads: e1 evaluates to e2

61 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Recursive declaration. Example n!

02157
Functional
Program-
ming
Function declaration:
Michael R. Ha

let rec fact = function

| 0 -> 1 (* i *)
| n -> n * fact(n-1);; (* ii *)
val fact : int -> int
Evaluation:
fact(3)
3 ∗ fact(3 − 1) (ii) [n 7→ 3]
3 ∗ 2 ∗ fact(2 − 1) (ii) [n 7→ 2]
3 ∗ 2 ∗ 1 ∗ fact(1 − 1) (ii) [n 7→ 1]
3∗2∗1∗1 (i) [n 7→ 0]
6

e1 e2 reads: e1 evaluates to e2

62 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Recursive declaration. Example n!

02157
Functional
Program-
ming
Function declaration:
Michael R. Ha

let rec fact = function

| 0 -> 1 (* i *)
| n -> n * fact(n-1);; (* ii *)
val fact : int -> int
Evaluation:
fact(3)
3 ∗ fact(3 − 1) (ii) [n 7→ 3]
3 ∗ 2 ∗ fact(2 − 1) (ii) [n 7→ 2]
3 ∗ 2 ∗ 1 ∗ fact(1 − 1) (ii) [n 7→ 1]
3∗2∗1∗1 (i) [n 7→ 0]
6

e1 e2 reads: e1 evaluates to e2

63 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Recursive declaration. Example n!

02157
Functional
Program-
ming
Function declaration:
Michael R. Ha

let rec fact = function

| 0 -> 1 (* i *)
| n -> n * fact(n-1);; (* ii *)
val fact : int -> int
Evaluation:
fact(3)
3 ∗ fact(3 − 1) (ii) [n 7→ 3]
3 ∗ 2 ∗ fact(2 − 1) (ii) [n 7→ 2]
3 ∗ 2 ∗ 1 ∗ fact(1 − 1) (ii) [n 7→ 1]
3∗2∗1∗1 (i) [n 7→ 0]
6

e1 e2 reads: e1 evaluates to e2

64 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Recursion. Example x n = x · . . . · x, n occurrences of x

02157
Mathematical definition: recursion formula Functional
Program-

x0 = 1 (1) ming

xn x · x n−1 ,
Michael R. Ha
= for n > 0 (2)

Function declaration:
let rec power = function
| ( ,0) -> 1.0 (* 1 *)
| (x,n) -> x * power(x,n-1) (* 2 *)

Patterns:
( , 0) matches any pair of the form (x, 0).
The wildcard pattern matches any value.
(x, n) matches any pair (u, i) yielding the bindings

x 7→ u, n 7→ i

65 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Recursion. Example x n = x · . . . · x, n occurrences of x

02157
Mathematical definition: recursion formula Functional
Program-

x0 = 1 (1) ming

xn x · x n−1 ,
Michael R. Ha
= for n > 0 (2)

Function declaration:
let rec power = function
| ( ,0) -> 1.0 (* 1 *)
| (x,n) -> x * power(x,n-1) (* 2 *)

Patterns:
( , 0) matches any pair of the form (x, 0).
The wildcard pattern matches any value.
(x, n) matches any pair (u, i) yielding the bindings

x 7→ u, n 7→ i

66 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Recursion. Example x n = x · . . . · x, n occurrences of x

02157
Mathematical definition: recursion formula Functional
Program-

x0 = 1 (1) ming

xn x · x n−1 ,
Michael R. Ha
= for n > 0 (2)

Function declaration:
let rec power = function
| ( ,0) -> 1.0 (* 1 *)
| (x,n) -> x * power(x,n-1) (* 2 *)

Patterns:
( , 0) matches any pair of the form (x, 0).
The wildcard pattern matches any value.
(x, n) matches any pair (u, i) yielding the bindings

x 7→ u, n 7→ i

67 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Evaluation. Example: power(4.0, 2)

02157
Functional
Program-
ming
Function declaration: Michael R. Ha

let rec power = function

| ( ,0) -> 1.0 (* 1 *)
| (x,n) -> x * power(x,n-1) (* 2 *)

Evaluation:
power(4.0, 2)
4.0 ∗ power(4.0, 2 − 1) Clause 2, [x 7→ 4.0, n 7→ 2]
4.0 ∗ power(4.0, 1)
4.0 ∗ (4.0 ∗ power(4.0, 1 − 1)) Clause 2, [x 7→ 4.0, n 7→ 1]
4.0 ∗ (4.0 ∗ power(4.0, 0))
4.0 ∗ (4.0 ∗ 1) Clause 1
16.0

68 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 If-then-else expressions

02157
Form: Functional
Program-
if b then e1 else e2 ming

Michael R. Ha

Evaluation rules:
if true then e1 else e2 e1
if false then e1 else e2 e2

Alternative declarations:
let rec fact n = if n=0 then 1
else n * fact(n-1);

let rec power(x,n) = if n=0 then 1.0

else x * power(x,n-1);

Use of patterns usually gives more understandable programs

69 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 If-then-else expressions

02157
Form: Functional
Program-
if b then e1 else e2 ming

Michael R. Ha

Evaluation rules:
if true then e1 else e2 e1
if false then e1 else e2 e2

Alternative declarations:
let rec fact n = if n=0 then 1
else n * fact(n-1);

let rec power(x,n) = if n=0 then 1.0

else x * power(x,n-1);

Use of patterns usually gives more understandable programs

70 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 If-then-else expressions

02157
Form: Functional
Program-
if b then e1 else e2 ming

Michael R. Ha

Evaluation rules:
if true then e1 else e2 e1
if false then e1 else e2 e2

Alternative declarations:
let rec fact n = if n=0 then 1
else n * fact(n-1);

let rec power(x,n) = if n=0 then 1.0

else x * power(x,n-1);

Use of patterns usually gives more understandable programs

71 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Booleans

02157
Functional
Program-
Type name bool ming

Michael R. Ha
Values false, true

Operator Type not true = false

not bool -> bool negation not false = true

Expressions

e1 && e2 “conjunction e1 ∧ e2 ”
e1 || e2 “disjunction e1 ∨ e2 ”

1<2 || 5/0 = 1
— are lazily evaluated, e.g.
true

Precedence: && has higher than ||

72 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Booleans

02157
Functional
Program-
Type name bool ming

Michael R. Ha
Values false, true

Operator Type not true = false

not bool -> bool negation not false = true

Expressions

e1 && e2 “conjunction e1 ∧ e2 ”
e1 || e2 “disjunction e1 ∨ e2 ”

1<2 || 5/0 = 1
— are lazily evaluated, e.g.
true

Precedence: && has higher than ||

73 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Booleans

02157
Functional
Program-
Type name bool ming

Michael R. Ha
Values false, true

Operator Type not true = false

not bool -> bool negation not false = true

Expressions

e1 && e2 “conjunction e1 ∧ e2 ”
e1 || e2 “disjunction e1 ∨ e2 ”

1<2 || 5/0 = 1
— are lazily evaluated, e.g.
true

Precedence: && has higher than ||

74 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Strings

02157
Functional
Program-
Type name string ming

Michael R. Ha
Values "abcd", " ", "", "123\"321" (escape sequence for ")

Operator Type
[Link] string -> int length of string
+ string*string -> string concatenation
= < <= ... string*string -> bool comparisons
string obj -> string conversions

Examples

- "auto" < "car"; - [Link]("abc"ˆ"def");

> val it = true : bool > val it = 6 : int

- "abc"+"de"; - string(6+18);
> val it = "abcde": string > val it = "24": string

75 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Strings

02157
Functional
Program-
Type name string ming

Michael R. Ha
Values "abcd", " ", "", "123\"321" (escape sequence for ")

Operator Type
[Link] string -> int length of string
+ string*string -> string concatenation
= < <= ... string*string -> bool comparisons
string obj -> string conversions

Examples

- "auto" < "car"; - [Link]("abc"ˆ"def");

> val it = true : bool > val it = 6 : int

- "abc"+"de"; - string(6+18);
> val it = "abcde": string > val it = "24": string

76 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Strings

02157
Functional
Program-
Type name string ming

Michael R. Ha
Values "abcd", " ", "", "123\"321" (escape sequence for ")

Operator Type
[Link] string -> int length of string
+ string*string -> string concatenation
= < <= ... string*string -> bool comparisons
string obj -> string conversions

Examples

- "auto" < "car"; - [Link]("abc"ˆ"def");

> val it = true : bool > val it = 6 : int

- "abc"+"de"; - string(6+18);
> val it = "abcde": string > val it = "24": string

77 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Types — every expression has a type e : τ

02157
Functional
Basic types: Program-
ming
type name example of values
Michael R. Ha
Integers int ˜27, 0, 15, 21000
Floats float ˜27.3, 0.0, 48.21
Booleans bool true, false

Pairs:
If e1 : τ1 and e2 : τ2
then (e1 , e2 ) : τ1 ∗τ2 pair (tuple) type constructor

Functions:
if f : τ1 -> τ2 and a : τ1 function type constructor
then f (a) : τ2

Examples:
(4.0, 2): float*int
power: float*int -> float * has higher precedence that ->
power(4.0, 2): float

78 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Types — every expression has a type e : τ

02157
Functional
Basic types: Program-
ming
type name example of values
Michael R. Ha
Integers int ˜27, 0, 15, 21000
Floats float ˜27.3, 0.0, 48.21
Booleans bool true, false

Pairs:
If e1 : τ1 and e2 : τ2
then (e1 , e2 ) : τ1 ∗τ2 pair (tuple) type constructor

Functions:
if f : τ1 -> τ2 and a : τ1 function type constructor
then f (a) : τ2

Examples:
(4.0, 2): float*int
power: float*int -> float * has higher precedence that ->
power(4.0, 2): float

79 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Types — every expression has a type e : τ

02157
Functional
Basic types: Program-
ming
type name example of values
Michael R. Ha
Integers int ˜27, 0, 15, 21000
Floats float ˜27.3, 0.0, 48.21
Booleans bool true, false

Pairs:
If e1 : τ1 and e2 : τ2
then (e1 , e2 ) : τ1 ∗τ2 pair (tuple) type constructor

Functions:
if f : τ1 -> τ2 and a : τ1 function type constructor
then f (a) : τ2

Examples:
(4.0, 2): float*int
power: float*int -> float * has higher precedence that ->
power(4.0, 2): float

80 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Types — every expression has a type e : τ

02157
Functional
Basic types: Program-
ming
type name example of values
Michael R. Ha
Integers int ˜27, 0, 15, 21000
Floats float ˜27.3, 0.0, 48.21
Booleans bool true, false

Pairs:
If e1 : τ1 and e2 : τ2
then (e1 , e2 ) : τ1 ∗τ2 pair (tuple) type constructor

Functions:
if f : τ1 -> τ2 and a : τ1 function type constructor
then f (a) : τ2

Examples:
(4.0, 2): float*int
power: float*int -> float * has higher precedence that ->
power(4.0, 2): float

81 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Type inference: power

02157
Functional
Program-
let rec power = function ming

| (_,0) -> 1.0 (* 1 *) Michael R. Ha

| (x,n) -> x * power(x,n-1) (* 2 *)

• The type of the function must have the form: τ1 * τ2 -> τ3 ,

because argument is a pair.
• τ3 = float because 1.0:float (Clause 1, function value.)
• τ2 = int because 0:int.
• x*power(x,n-1):float, because τ3 = float.
• multiplication can have
int*int -> int or float*float -> float
as types, but no “mixture” of int and float
• Therefore x:float and τ1 =float.

The F# system determines the type float*int -> float

82 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Type inference: power

02157
Functional
Program-
let rec power = function ming

| (_,0) -> 1.0 (* 1 *) Michael R. Ha

| (x,n) -> x * power(x,n-1) (* 2 *)

• The type of the function must have the form: τ1 * τ2 -> τ3 ,

because argument is a pair.
• τ3 = float because 1.0:float (Clause 1, function value.)
• τ2 = int because 0:int.
• x*power(x,n-1):float, because τ3 = float.
• multiplication can have
int*int -> int or float*float -> float
as types, but no “mixture” of int and float
• Therefore x:float and τ1 =float.

The F# system determines the type float*int -> float

83 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Type inference: power

02157
Functional
Program-
let rec power = function ming

| (_,0) -> 1.0 (* 1 *) Michael R. Ha

| (x,n) -> x * power(x,n-1) (* 2 *)

• The type of the function must have the form: τ1 * τ2 -> τ3 ,

because argument is a pair.
• τ3 = float because 1.0:float (Clause 1, function value.)
• τ2 = int because 0:int.
• x*power(x,n-1):float, because τ3 = float.
• multiplication can have
int*int -> int or float*float -> float
as types, but no “mixture” of int and float
• Therefore x:float and τ1 =float.

The F# system determines the type float*int -> float

84 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Type inference: power

02157
Functional
Program-
let rec power = function ming

| (_,0) -> 1.0 (* 1 *) Michael R. Ha

| (x,n) -> x * power(x,n-1) (* 2 *)

• The type of the function must have the form: τ1 * τ2 -> τ3 ,

because argument is a pair.
• τ3 = float because 1.0:float (Clause 1, function value.)
• τ2 = int because 0:int.
• x*power(x,n-1):float, because τ3 = float.
• multiplication can have
int*int -> int or float*float -> float
as types, but no “mixture” of int and float
• Therefore x:float and τ1 =float.

The F# system determines the type float*int -> float

85 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Type inference: power

02157
Functional
Program-
let rec power = function ming

| (_,0) -> 1.0 (* 1 *) Michael R. Ha

| (x,n) -> x * power(x,n-1) (* 2 *)

• The type of the function must have the form: τ1 * τ2 -> τ3 ,

because argument is a pair.
• τ3 = float because 1.0:float (Clause 1, function value.)
• τ2 = int because 0:int.
• x*power(x,n-1):float, because τ3 = float.
• multiplication can have
int*int -> int or float*float -> float
as types, but no “mixture” of int and float
• Therefore x:float and τ1 =float.

The F# system determines the type float*int -> float

86 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Type inference: power

02157
Functional
Program-
let rec power = function ming

| (_,0) -> 1.0 (* 1 *) Michael R. Ha

| (x,n) -> x * power(x,n-1) (* 2 *)

• The type of the function must have the form: τ1 * τ2 -> τ3 ,

because argument is a pair.
• τ3 = float because 1.0:float (Clause 1, function value.)
• τ2 = int because 0:int.
• x*power(x,n-1):float, because τ3 = float.
• multiplication can have
int*int -> int or float*float -> float
as types, but no “mixture” of int and float
• Therefore x:float and τ1 =float.

The F# system determines the type float*int -> float

87 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Type inference: power

02157
Functional
Program-
let rec power = function ming

| (_,0) -> 1.0 (* 1 *) Michael R. Ha

| (x,n) -> x * power(x,n-1) (* 2 *)

• The type of the function must have the form: τ1 * τ2 -> τ3 ,

because argument is a pair.
• τ3 = float because 1.0:float (Clause 1, function value.)
• τ2 = int because 0:int.
• x*power(x,n-1):float, because τ3 = float.
• multiplication can have
int*int -> int or float*float -> float
as types, but no “mixture” of int and float
• Therefore x:float and τ1 =float.

The F# system determines the type float*int -> float

88 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Type inference: power

02157
Functional
Program-
let rec power = function ming

| (_,0) -> 1.0 (* 1 *) Michael R. Ha

| (x,n) -> x * power(x,n-1) (* 2 *)

• The type of the function must have the form: τ1 * τ2 -> τ3 ,

because argument is a pair.
• τ3 = float because 1.0:float (Clause 1, function value.)
• τ2 = int because 0:int.
• x*power(x,n-1):float, because τ3 = float.
• multiplication can have
int*int -> int or float*float -> float
as types, but no “mixture” of int and float
• Therefore x:float and τ1 =float.

The F# system determines the type float*int -> float

89 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Summary

02157
Functional
Program-
ming

Michael R. Ha

• The interactive environment

• Values, expressions, types, patterns
• Declarations of values and recursive functions
• Binding, environment and evaluation
• Type inference

Breath first round through many concepts aiming at program

construction from the first day.

We will go deeper into each of the concepts later in the course.

90 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Summary

02157
Functional
Program-
ming

Michael R. Ha

• The interactive environment

• Values, expressions, types, patterns
• Declarations of values and recursive functions
• Binding, environment and evaluation
• Type inference

Breath first round through many concepts aiming at program

construction from the first day.

We will go deeper into each of the concepts later in the course.

91 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Overview

02157
Functional
Program-
ming

Michael R. Ha

• Lists: values and constructors

• Recursions following the structure of lists

The purpose of this lecture is to give you an (as short as possible)

introduction to lists, so that you can solve a problem which can
illustrate some of F#’s high-level features.

This part is not intended as a comprehensive presentation on lists,

and we will return to the topic again later.

92 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Overview

02157
Functional
Program-
ming

Michael R. Ha

• Lists: values and constructors

• Recursions following the structure of lists

The purpose of this lecture is to give you an (as short as possible)

introduction to lists, so that you can solve a problem which can
illustrate some of F#’s high-level features.

This part is not intended as a comprehensive presentation on lists,

and we will return to the topic again later.

93 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Lists

02157
A list is a finite sequence of elements having the same type: Functional
Program-
ming
[v1 ; . . . ; vn ] ([ ] is called the empty list) Michael R. Ha

[2;3;6];;
val it : int list = [2; 3; 6]

["a"; "ab"; "abc"; ""];;

val it : string list = ["a"; "ab"; "abc"; ""]

[sin; cos];;
val it : (float->float) list = [<fun:...>; <fun:...>]

[(1,true); (3,true)];;
val it : (int * bool) list = [(1, true); (3, true)]

[[]; [1]; [1;2]];;

val it : int list list = [[]; [1]; [1; 2]]

94 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Lists

02157
A list is a finite sequence of elements having the same type: Functional
Program-
ming
[v1 ; . . . ; vn ] ([ ] is called the empty list) Michael R. Ha

[2;3;6];;
val it : int list = [2; 3; 6]

["a"; "ab"; "abc"; ""];;

val it : string list = ["a"; "ab"; "abc"; ""]

[sin; cos];;
val it : (float->float) list = [<fun:...>; <fun:...>]

[(1,true); (3,true)];;
val it : (int * bool) list = [(1, true); (3, true)]

[[]; [1]; [1;2]];;

val it : int list list = [[]; [1]; [1; 2]]

95 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Lists

02157
A list is a finite sequence of elements having the same type: Functional
Program-
ming
[v1 ; . . . ; vn ] ([ ] is called the empty list) Michael R. Ha

[2;3;6];;
val it : int list = [2; 3; 6]

["a"; "ab"; "abc"; ""];;

val it : string list = ["a"; "ab"; "abc"; ""]

[sin; cos];;
val it : (float->float) list = [<fun:...>; <fun:...>]

[(1,true); (3,true)];;
val it : (int * bool) list = [(1, true); (3, true)]

[[]; [1]; [1;2]];;

val it : int list list = [[]; [1]; [1; 2]]

96 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Lists

02157
A list is a finite sequence of elements having the same type: Functional
Program-
ming
[v1 ; . . . ; vn ] ([ ] is called the empty list) Michael R. Ha

[2;3;6];;
val it : int list = [2; 3; 6]

["a"; "ab"; "abc"; ""];;

val it : string list = ["a"; "ab"; "abc"; ""]

[sin; cos];;
val it : (float->float) list = [<fun:...>; <fun:...>]

[(1,true); (3,true)];;
val it : (int * bool) list = [(1, true); (3, true)]

[[]; [1]; [1;2]];;

val it : int list list = [[]; [1]; [1; 2]]

97 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Lists

02157
A list is a finite sequence of elements having the same type: Functional
Program-
ming
[v1 ; . . . ; vn ] ([ ] is called the empty list) Michael R. Ha

[2;3;6];;
val it : int list = [2; 3; 6]

["a"; "ab"; "abc"; ""];;

val it : string list = ["a"; "ab"; "abc"; ""]

[sin; cos];;
val it : (float->float) list = [<fun:...>; <fun:...>]

[(1,true); (3,true)];;
val it : (int * bool) list = [(1, true); (3, true)]

[[]; [1]; [1;2]];;

val it : int list list = [[]; [1]; [1; 2]]

98 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Lists

02157
A list is a finite sequence of elements having the same type: Functional
Program-
ming
[v1 ; . . . ; vn ] ([ ] is called the empty list) Michael R. Ha

[2;3;6];;
val it : int list = [2; 3; 6]

["a"; "ab"; "abc"; ""];;

val it : string list = ["a"; "ab"; "abc"; ""]

[sin; cos];;
val it : (float->float) list = [<fun:...>; <fun:...>]

[(1,true); (3,true)];;
val it : (int * bool) list = [(1, true); (3, true)]

[[]; [1]; [1;2]];;

val it : int list list = [[]; [1]; [1; 2]]

99 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Trees for lists

A non-empty list [x1 , x2 , . . . , xn ], n ≥ 1, consists of 02157

Functional
Program-
• a head x1 and ming

• a tail [x2 , . . . , xn ] Michael R. Ha

::
@
@
@
2 ::
@
@
@
3 :: ::
@ @
@ @
@ @
2 [] 2 []

Graph for [2,3,2] Graph for [2]

100 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Trees for lists

A non-empty list [x1 , x2 , . . . , xn ], n ≥ 1, consists of 02157

Functional
Program-
• a head x1 and ming

• a tail [x2 , . . . , xn ] Michael R. Ha

::
@
@
@
2 ::
@
@
@
3 :: ::
@ @
@ @
@ @
2 [] 2 []

Graph for [2,3,2] Graph for [2]

101 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 List constructors: [] and ::

02157
Lists are generated as follows: Functional
Program-
• the empty list is a list, designated [] ming

Michael R. Ha
• if x is an element and xs is a list,
then so is x :: xs (type consistency)

:: associate to the right, i.e. x1 ::x2 ::xs means x1 ::(x2 ::xs)

::
@
@
@
x1 ::
@
@
@
x2 xs

Graph for x1 ::x2 ::xs

102 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 List constructors: [] and ::

02157
Lists are generated as follows: Functional
Program-
• the empty list is a list, designated [] ming

Michael R. Ha
• if x is an element and xs is a list,
then so is x :: xs (type consistency)

:: associate to the right, i.e. x1 ::x2 ::xs means x1 ::(x2 ::xs)

::
@
@
@
x1 ::
@
@
@
x2 xs

Graph for x1 ::x2 ::xs

103 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Recursion on lists – a simple example

02157
n
X n
X Functional
suml [x1 ,x2 , . . . ,xn ] = xi = x1 + x2 + · · · + xn = x1 + xi Program-
ming
i=1 i=2
Michael R. Ha

Constructors are used in list patterns

let rec suml = function
| [] -> 0
| x::xs -> x + suml xs;;
> val suml : int list -> int

suml [1;2]
1 + suml [2] (x 7→ 1 and xs 7→ [2])
1 + (2 + suml []) (x 7→ 2 and xs 7→ [])
1 + (2 + 0) (the pattern [] matches the value [])
1 + 2
3

Recursion follows the structure of lists

104 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Recursion on lists – a simple example

02157
n
X n
X Functional
suml [x1 ,x2 , . . . ,xn ] = xi = x1 + x2 + · · · + xn = x1 + xi Program-
ming
i=1 i=2
Michael R. Ha

Constructors are used in list patterns

let rec suml = function
| [] -> 0
| x::xs -> x + suml xs;;
> val suml : int list -> int

suml [1;2]
1 + suml [2] (x 7→ 1 and xs 7→ [2])
1 + (2 + suml []) (x 7→ 2 and xs 7→ [])
1 + (2 + 0) (the pattern [] matches the value [])
1 + 2
3

Recursion follows the structure of lists

105 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Recursion on lists – a simple example

02157
n
X n
X Functional
suml [x1 ,x2 , . . . ,xn ] = xi = x1 + x2 + · · · + xn = x1 + xi Program-
ming
i=1 i=2
Michael R. Ha

Constructors are used in list patterns

let rec suml = function
| [] -> 0
| x::xs -> x + suml xs;;
> val suml : int list -> int

suml [1;2]
1 + suml [2] (x 7→ 1 and xs 7→ [2])
1 + (2 + suml []) (x 7→ 2 and xs 7→ [])
1 + (2 + 0) (the pattern [] matches the value [])
1 + 2
3

Recursion follows the structure of lists

106 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Infix functions

It is possible to declare infix functions in F#, i.e. the function symbol 02157
Functional
is between the arguments. Program-
ming

The prefix function on lists is declared as follows: Michael R. Ha

let rec (<=.) xs ys =

match (xs,ys) with
| ([],_) -> true
| (_,[]) -> false
| (x::xs’,y::ys’) -> x=y && xs’ <=. ys’;;

[1;2;3] <=. [1;2];;

val it : bool = false

• The special way of declaring the function (<=.) xs ys makes

<=. an infix operator
• The match (xs,ys) construct allows for branching out on
patterns for (xs,ys)

Suitable use of infix functions can increase readability significantly

107 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Infix functions

It is possible to declare infix functions in F#, i.e. the function symbol 02157
Functional
is between the arguments. Program-
ming

The prefix function on lists is declared as follows: Michael R. Ha

let rec (<=.) xs ys =

match (xs,ys) with
| ([],_) -> true
| (_,[]) -> false
| (x::xs’,y::ys’) -> x=y && xs’ <=. ys’;;

[1;2;3] <=. [1;2];;

val it : bool = false

• The special way of declaring the function (<=.) xs ys makes

<=. an infix operator
• The match (xs,ys) construct allows for branching out on
patterns for (xs,ys)

Suitable use of infix functions can increase readability significantly

108 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Infix functions

It is possible to declare infix functions in F#, i.e. the function symbol 02157
Functional
is between the arguments. Program-
ming

The prefix function on lists is declared as follows: Michael R. Ha

let rec (<=.) xs ys =

match (xs,ys) with
| ([],_) -> true
| (_,[]) -> false
| (x::xs’,y::ys’) -> x=y && xs’ <=. ys’;;

[1;2;3] <=. [1;2];;

val it : bool = false

• The special way of declaring the function (<=.) xs ys makes

<=. an infix operator
• The match (xs,ys) construct allows for branching out on
patterns for (xs,ys)

Suitable use of infix functions can increase readability significantly

109 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Infix functions

It is possible to declare infix functions in F#, i.e. the function symbol 02157
Functional
is between the arguments. Program-
ming

The prefix function on lists is declared as follows: Michael R. Ha

let rec (<=.) xs ys =

match (xs,ys) with
| ([],_) -> true
| (_,[]) -> false
| (x::xs’,y::ys’) -> x=y && xs’ <=. ys’;;

[1;2;3] <=. [1;2];;

val it : bool = false

• The special way of declaring the function (<=.) xs ys makes

<=. an infix operator
• The match (xs,ys) construct allows for branching out on
patterns for (xs,ys)

Suitable use of infix functions can increase readability significantly

110 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Exercises

02157
Functional
Program-
ming

Michael R. Ha

• length xs : the length of the list xs (is a predefined function).

• remove(x, ys) : removes all occurrences of x in the list ys

Have fun with your first non-trivial functional program:

polynomials represented as lists

111 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012
 Exercises

02157
Functional
Program-
ming

Michael R. Ha

• length xs : the length of the list xs (is a predefined function).

• remove(x, ys) : removes all occurrences of x in the list ys

Have fun with your first non-trivial functional program:

polynomials represented as lists

112 DTU Informatics, Technical University of Denmark Lecture 1: Introduction and Getting Started MRH 6/09/2012