%\documentclass[handout,9pt,xcolor=dvipsnames,unknownkeysallowed]{beamer}
\documentclass[9pt,xcolor=dvipsnames,unknownkeysallowed]{beamer}

\input{../Common/common}



\subtitle{Lecture 1: Introduction and Getting Started} % (optional)
\date {MRH 26/08/2024}




\begin{document}

\begin{frame}
  \titlepage
%  \begin{tabular}{p{5cm}p{10cm}}
%    &\pgfuseimage{frise}\\
%    \pgfuseimage{dept} &
%  \end{tabular}

\end{frame}



\begin{frame}
\begin{center}\LARGE \color{BlueViolet}  WELCOME to \\
02157 Functional Programming
\end{center}

\bigskip

\begin{itemlist}{XXX}


\item[Teacher:] Michael R.\ Hansen, DTU Compute \qquad 
 \textcolor{BrickRed}{mire@dtu.dk}
\bigskip

\item[Teaching assistants:] \ \\
 

Jonas Dahl Larsen\\
Mathias Spezia\\
Mikael Hjermitslev Hoffmann\\
Oliwia Pindel\\
Shuokai Ma\\
 
\bigskip

\item[Homepage:]
\textcolor{BrickRed}{www.compute.dtu.dk/courses/02157}
\end{itemlist}
	

\end{frame}


\begin{frame}%[containsverbatim]
\frametitle{About functions}

Advanced Engineering Mathematics 1

\begin{itemize}
	\item eNotes: \url{https://01006.compute.dtu.dk/enoter}
\end{itemize}

\pause
\bigskip

%\onslide<2->{
For a function, like
\[\blue 
f(x) = x^2
\]
we often mention its {\darkgreen domain} an {\redbrown range}: 
\[\blue 
f: \mathbb{\darkgreen R} \to \mathbb{\redbrown R} 
\]
%}

\pause
%\onslide<3->{
\medskip

For a {\blue typed functional language} like F\#, a function like:
\begin{alltt}\blue 
	let f x = x ** 2.0;;
\end{alltt}
has an associated type:

\begin{alltt}\blue 
	f:{\darkgreen float} -> {\redbrown float}
\end{alltt}
where {\blue float} is the type of both the domain and 
the range.
%}
\end{frame}



\begin{frame}[fragile]%[containsverbatim]
\frametitle{A Simple  Functional Programming Setting}

A program $\blue f$ is a function 
\[\blue f: Argument \to Result\]	
that takes {\redbrown one argument} and produces {\redbrown one result}.

\pause
\bigskip
Consider 
\begin{alltt}\blue 
let f x = 2*x + 3;;
\end{alltt}

\pause
\bigskip

Every function has a {\redbrown type} specifying types of argument and result:
\begin{alltt}\blue
f: int -> int
\end{alltt}	
\begin{itemize}
	\item argument and result of $\blue \verb|f|$ have type $\blue \verb|int|$ (for integers).
\end{itemize}
 
\pause 
\bigskip 

{\redbrown Computation} is governed by {\redbrown function application} 
\[\begin{array}{lll}
  & \mathtt{\blue f(1+2)} & \\
= & \mathtt{\blue f(3)}   &  \mbox{evaluate argument}\\
= & \mathtt{\blue 2*3+3}  &  \mbox{substitute $\blue 3$ in for  $\blue x$ in  $\blue f$'s body}\\
%= & \mathtt{\blue g(9)}      &  \mbox{evaluate argument}\\
%= & \mathtt{\blue 3*9}    	 & \mbox{substitute 9 in for y in g's body}\\
= & {\blue 9}               &
\end{array}
\]

\pause
\bigskip
%\begin{itemize}
F\# has {\redbrown eager} evaluation: Compute argument before making the call
%\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Context of 02157}

Prerequisites
\begin{itemize}
	\item You have used an editor to create programs
	
	\item You have installed a program on your laptop
	
	\item  You have had (or have in the same semester) a course on Discrete Mathematics
\end{itemize}


\pause
\bigskip

The course is a part of educations leading to the MSc programme in Computer Science and Engineering. 
\begin{itemize}
	\item  candidates contributing to the development of high-quality, advanced software products
\end{itemize}


\pause
\bigskip
It is an aim to contribute to the fundament for educations leading to the MSc education in CS\&E
\pause
\begin{center}\redbrown
	May sound good; but what does it mean?
\end{center}

\end{frame}


\begin{frame}{There is no magic}

It is possible to understand everything:

\begin{itemize}
\item<2-> The syntax (notation) of the programming language

\item<3-> The semantics (meaning) of programs

\item<4-> The evaluation of programs

\item<5-> The properties of programs

\end{itemize}

\bigskip
\pause[6]
Functional programming is a simple setting supporting 
\begin{itemize}
\item declaration of clear, concise programs at a high level of abstraction

\item understanding and analysis of programs
\end{itemize}
due to the basis on mathematical functions (no side-effects)

\end{frame}

\begin{frame}[fragile]%[containsverbatim]
\frametitle{An archetypical example $\color{Blue}n! = 1 \cdot 2 \cdot \ldots \cdot n$, $\color{Blue}n\geq
	0$}

Mathematical definition: \hfill {\darkgreen recursion formula}
\[\color{Blue}
\begin{array}{lclrr}
0 ! & = & 1 & &\ \ \ \ \ \ \ \ \ \ \ \ \ (i)\\
n ! & = & n \cdot (n-1)!, & \mbox{for $n > 0$} & (ii)
\end{array}
\]
\begin{itemize}
	\item $\blue n!$ is defined {\redbrown recursively} in terms of $\blue (n-1)!$ when $\blue n>0$
\end{itemize}
\bigskip
\pause


Computation:
\[\color{Blue}
\begin{array}{llr}
& 3! & \\
= & 3 \cdot (3-1)! & (ii)\\
= & 3 \cdot 2 \cdot (2-1)! & (ii)\\
= & 3 \cdot 2 \cdot  1 \cdot (1-1)! & (ii)\\
= & 3 \cdot 2 \cdot 1 \cdot 1 & (i)\\
= & 6 &
\end{array}
\]

\end{frame}

\begin{frame}[fragile]%[containsverbatim]
\frametitle{Declaring recursive functions:\ \ \color{Blue}$\mathtt{let}\ {\redbrown rec}\ f\, x\ =\ e$}	
\vspace*{-0.4cm}	
\begin{itemize}
%\item $\blue x$ is called the {\em\redbrown formal parameter}
%\item<2-> the defining expression $\blue e$ is called the {\em\redbrown body} of the declaration
\item the function $\blue f$ occurs in the body $\blue e$ of a {\redbrown\em recursive declaration} 
\end{itemize}	

%\begin{frame}{Recursive declaration. Example $\color{Blue}n!$}

\pause
\bigskip

A recursive function declaration:
\begin{alltt}\color{Blue}
let{\redbrown rec}{\darkgreen fact} n = 
    if n=0 then 1                (*  i *)
    else n *{\darkgreen fact}(n-1);;         (* ii *)
\ett{val fact : int -> int}
\end{alltt}


\pause

{\blue Evaluation}:
\[
\begin{array}{llrr}
&  \mathtt{fact(3)} & & \\
\leadsto & \mathtt{3 * fact(3-1)} & (ii)& \onslide<3->{\darkgreen
[\mathtt{n} \mapsto 3]} \\
\leadsto & \mathtt{3 * 2 * fact(2-1)} & (ii)
&\onslide<4->{\darkgreen
[\mathtt{n} \mapsto 2]}\\
\leadsto & \mathtt{3 * 2 * 1 * fact(1-1)} &
(ii)&\onslide<5->{\darkgreen
[\mathtt{n} \mapsto 1]} \\
\leadsto & \mathtt{3 * 2 * 1 * 1} & (i)&\onslide<6->{\darkgreen
[\mathtt{n} \mapsto 0]} \\
\leadsto & \mathtt{6} & &
\end{array}
\]
\hfill %\lilacbox{
\begin{minipage}{7cm}
\[ {\blue e_1\ \leadsto e_2} \qquad \mbox{reads: $e_1$ {\redbrown evaluates to}
	$e_2$}
\]
\end{minipage}
\pause
\bigskip
\begin{itemize}
\item An {\darkgreen environment} is used to bind the formal parameter $\blue n$ to actual parameters $\blue 3, 2, 1, 0$ during evaluation
\end{itemize}
\end{frame}




\begin{frame}{Some functional programming background}


\begin{itemize}
	\item The \textcolor{BrickRed}{$\lambda$-calculus} was introduced
	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
	${\color{BrickRed}\lambda} x. x+2$.
	
	\medskip
	
	\item<2-> The untyped functional-like
	programming language LISP was developed by McCarthy in the late
	1950s.
	
	\medskip
	

	
	\item<3-> Functional languages with a strong type
	system like ML (by Milner) and Miranda (by Turner) were introduced in the 1970s.
	

	
	

	
	
	\medskip
	
	\item<4-> Functional languages (SML, Haskell, OCAML, {\blue F\#}, $\ldots$)  have now
	applications far away from their origin:
	Compilers, Artificial Intelligence,  Web-applications,
	Financial sector, $\ldots$
	%\end{itemlist}
	
		\medskip
	\item<5-> Declarative aspects are now sneaking into "main stream
	languages"
	

	

	
	\medskip
	\item<6-> Functional programming should be a mandatory element of every BSc.\ education in Computer Science according to ACM's and IEEE's curricula recommendations, 2013.
	

	
	
\end{itemize}
\end{frame}

\begin{frame}{Lambda Calculus}

The untyped Lambda Calculus has just three kinds of expressions $\blue e$:
\begin{itemize}
	\item {\darkgreen variables} $\blue x$
	\item {\darkgreen abstractions} $\blue \lambda x.e$
	\item {\darkgreen applications} $\blue e_1\ e_2$
\end{itemize}
\pause

where %an abstraction represents an anonymous function (the function of $x$ given by $e$) and 
\begin{itemize}
	\item $\blue  \lambda x.e$ reads: ``the function of $\blue x$ given by $\blue e$''
\end{itemize}

\pause 
\bigskip

An application like $\blue (\lambda x.e)\ e_2$ may be {\darkgreen evaluated} as follows:
\[\blue 
\begin{array}{lll}
(\lambda x.e)\ e_2 & \leadsto & e_2'
\end{array}
\]
where $\blue e_2'$ is obtained from $\blue e_2$ by 
\begin{itemize}
	\item substituting every free occurrence of $\blue x$ in $\blue e$ by $\blue e_2$
\end{itemize}
\ \hfill {\redbrown like we did in the previous examples}

\pause
\bigskip
No magic: A full explanation can be given in terms of few concepts

\pause
\bigskip
The part of {\blue F\#} we will use is based on {\darkgreen typed lambda calculus}

\end{frame}

\begin{frame}[fragile]%[containsverbatim]
	\frametitle{Overview: Syntactical constructs in ``our part of'' F\# }

\begin{itemize}
	\item Constants: {\blue 0, 1.1, true, ...}
	
	\medskip
	
	\item<2-> Patterns: $\blue x \quad \_  \quad (p_1, \ldots, p_n) \quad p_1\!::\!p_2 \quad p_1 | p_2 \quad p\ \mathtt{when}\ e \quad p\ \mathtt{as}\ x \quad p\!:\!t  \ldots$   
	
	\medskip
	
	\item<3-> Expressions:\\ $\blue x \quad (e_1,\ldots,e_n) \quad e_1\!::\!e_2 \quad e_1 e_2 \quad e_1\! \oplus\! e_2 \quad \mathtt{let}\ p_1 = e_1\ \mathtt{in}\ e_2 \quad e\!:\!t$\\[2mm]
	$\blue \mathtt{if}\ e\ \mathtt{then}\ e_1\  \mathtt{then}\ e_2 \qquad \mathtt{match}\ e\ \mathtt{with}\ clauses$\\[2mm] 
	$\blue \mathtt{fun}\ p_1 \cdots p_n \verb!->! e \qquad \mathtt{function}\ clauses \quad \ldots$   
	
	\medskip
	
	\item<4-> Declarations $\blue \mathtt{let}\ f\  p_1 \ldots p_n = e \quad \mathtt{let\ rec}\ f\  p_1 \ldots p_n = e$, \hfill $\blue n\ge 0$  
	
	\medskip
	
	\item<5-> Types\\ $\blue \mathtt{int}  \quad \blue \mathtt{float}  \quad \mathtt{bool}  \quad \mathtt{string}  \quad 'a  \ldots$\\
	$\blue t_1\!*\!t_2\!*\!\cdots\!*\!t_n  \quad  t\ \mathtt{list}  \quad t_1 \verb|->| t_2 \ldots$  
	
\end{itemize}
\onslide<3->{where the construct $\blue clauses$ has the form:
	\begin{alltt}\blue 
		| p\(\sb{1}\) -> e\(\sb{1}\)
		| \(\ldots\)
		| p\(\sb{n}\) -> e\(\sb{n}\)
	\end{alltt}  
}
\bigskip

\pause[6]
In addition to that
\begin{itemize}
	\item type declarations, precedence and associativity rules, parenthesis around $\blue p$ and $\blue e$ and type correctness
\end{itemize}
\end{frame}


\begin{frame}


%\begin{itemize}
%\item We use functional programming / F\# in an academic context in this course  
%\end{itemize}

%\bigskip
%\pause

Have a look at
%\begin{center}\redbrown
%Functional programming languages, like F\#, are {\redbrown not} toy languages
%\end{center}
\begin{itemize}
\item \url{http://homepages.inf.ed.ac.uk/wadler/realworld/}
\item \url{https://fsharp.org/testimonials/}
\end{itemize}
concerning use of functional programming in the "real world". 



\end{frame}



\begin{frame}
\frametitle{Practical Matters}



\begin{itemize}
	
\item General information:  {\blue \url{http://courses.compute.dtu.dk/02157}}

\bigskip


	
\item<2-> Practical Information:\\
 {\blue \url{http://courses.compute.dtu.dk/02157/PracticalInfo.html}}\\
 \medskip
 {\blue Exam form: Written exam, 4 hour -- no aid allowed}\\
 
\bigskip 
 
\item<3-> Course plan:\\ {\blue \url{http://courses.compute.dtu.dk/02157/plan.html}}



\end{itemize}

\bigskip

\bigskip

\pause[4]
On DTU Learn you can find some material
\begin{itemize}
	\item A brief course introduction
	\item A mini-project on polynomials
	\item Slides
	\item ....
\end{itemize}

\end{frame}


\begin{frame}
\frametitle{Course Infrastructure}
\vspace*{-3mm}

\begin{itemize}
\item Syllabus (see introduction to the course)

\item Weekly lectures

\item Weekly exercise classes with fantastic TAs
\end{itemize}
\ \hfill {\redbrown a flipped classroom model}
\pause
\bigskip

Course design is based on an evenly distributed workload and ``steady progress'' throughout the semester


\pause
\bigskip

Mini-projects: Exercise FP concepts and techniques while
\begin{itemize}
\item telling a coherent story on a specific topic
\item relating FP to neighbouring courses
\item introducing fundamental CS concepts
\end{itemize}

\bigskip
\pause

Nothing is mandatory


\bigskip
\pause

{\darkgreen It is your own responsibility to achieve a good use of Fridays' teaching slot}
\begin{itemize}
\item {\redbrown no online support}
\item {\redbrown no hotline support}
\end{itemize}

\bigskip
\pause
You are always welcome to visit my office: Room 112, Building 322
\end{frame}



\begin{frame}{Overview}

Part 1 Getting Started:
\begin{itemize}
\item The interactive environment

\item Values, expressions, types, patterns

\item Declarations of
  values and recursive functions

\item Binding, environment and evaluation

\item Type inference
\end{itemize}
\ \hfill{\redbrown  Main ingredients of F\#}


\bigskip
\pause

Part 2 Lists:
\begin{itemize}
	
	\item Lists: values and constructors
	
	\item Recursions following the structure of lists
	
	\item Polymorphism
	\end{itemize}
\ \hfill{\redbrown  A value-oriented approach}



\end{frame}


%\input{interactiveEnv}
%\subsection{The interactive environment}
\begin{frame}{The Interactive Environment}
\begin{tabular}{lc}
\begin{minipage}{5cm}
\begin{alltt}2*3 + 4;;\\
    \ett{val it : int = 10}
\end{alltt}
\end{minipage}
& \onslide<2->{
\begin{minipage}{7cm}
\begin{itemize}
\item [$\redbrown \Leftarrow$] Input to the F\# system \item
[$\redbrown \Leftarrow$] Answer from the F\# system
\end{itemize}
\end{minipage}}
\end{tabular}

\bigskip

\onslide<3-> {
\begin{itemize}
\item The {\em\darkgreen keyword} \texttt{val} indicates a value
is computed \item The {\em\darkgreen integer} 10 is the computed
value \item \texttt{int} is the {\em\darkgreen type} of the
computed value \item The {\em\darkgreen identifier} \texttt{it}
names the (last) computed value
\end{itemize}
}

\bigskip

\onslide<4->{The notion {\em\redbrown binding} explains which
entities are named by
  identifiers.
\[ {\darkgreen \mathtt{it} \mapsto 10} \qquad  \mbox{reads: ``\texttt{it} is bound to 10''} \]
}

\end{frame}


%\subsection{Declarations}
\begin{frame}{Value Declarations}
A value declaration has the form:\ {\blue $\mathtt{let}\
\mathit{identifier}\ = \mathit{expression}$}

\bigskip

\begin{tabular}{lc}
\begin{minipage}{6cm}
\begin{alltt}
let price = 25 * 5;;\\[2mm]
\ett{val price : int = 125}
\end{alltt}
\end{minipage}
&
\begin{minipage}{7cm}
\begin{itemize}
\item [$\redbrown \Leftarrow$] A declaration as input \item
[$\redbrown \Leftarrow$] Answer from the F\# system
\end{itemize}
\end{minipage}
\end{tabular}

\bigskip

The effect of a declaration is a binding: \  ${\darkgreen
\mathtt{price}
    \mapsto 125}$

\bigskip
\onslide<2->{Bound identifiers can be used in expressions and
declarations, e.g.}

\begin{tabular}{lr}
\begin{minipage}{6.3cm}
\onslide<2->{
\begin{alltt}
let newPrice = 2*price;;\\
\ett{val newPrice : int = 250}


newPrice > 500;;\\
\ett{val it : bool = false}
\end{alltt}}
\end{minipage}
&
\begin{minipage}{5.1cm}
\onslide<3->{
\ \\[2mm]
{\darkgreen A collection of bindings {\blue
\[\left[
   \begin{array}{lcl} \mathtt{price}& \mapsto& 125\\
                      \mathtt{newPrice} & \mapsto& 250\\
                      \mathtt{it}& \mapsto& \mathrm{false}
   \end{array}
\right]
\]}
is called an {\redbrown environment}}}
\end{minipage}

\end{tabular}

\end{frame}



\begin{frame}[fragile]%[containsverbatim]
	\frametitle{Function Declarations 1:\ \ \color{Blue}$\mathtt{let}\ f\, x\ =\ e$}
\vspace*{-0.5cm}	
\begin{itemize}
	\item $\blue x$ is called the {\em\redbrown formal parameter}
	\item the defining expression $\blue e$ is called the {\em\redbrown body} of the declaration 
\end{itemize}		

\medskip
\pause	

Declaration of the circle area function:
\begin{alltt}\color{Blue}
\ \    let circleArea r = System.Math.PI * r * r;;
\end{alltt}

\medskip

\begin{itemize}
\item \texttt{\color{Blue}System.Math} is a program library \item
\texttt{\color{Blue}PI} is an identifier (with type
\texttt{\color{Blue}float}) for $\color{Blue}\pi$
  in \texttt{\color{Blue}System.Math}
\end{itemize}

\medskip

\onslide<2->{The type is {\redbrown automatically inferred} in the
answer:
\begin{alltt}\color{Blue}
\ \    \ett{val circleArea : {\redbrown float -> float}}
\end{alltt}
}

\bigskip
\onslide<3->{ Applications of the function:
\begin{alltt}\color{Blue}
\ \   circleArea 1.0;;     {\blue (*} {\darkgreen this is a comment} {\blue *)}\\
\ \  \ett{val it : float = 3.141592654}\\
\                                       \\
\ \   circleArea(3.2);;   {\blue //} {\darkgreen A comment: optional brackets}\\
\ \  \ett{val it : float = 32.16990877}
\end{alltt}
 }
 \medskip
\onslide<4->{\texttt{1.0} and \texttt{3.2} are also called {\redbrown\em actual parameters}}

\end{frame}




\begin{frame}%[fragile]
	\frametitle{Patterns}
	
A pattern is composed from {\blue identifiers}, {\blue constants} and the 
{\redbrown wildcard pattern}: 
\texttt{\_} using {\blue constructors} (considered soon)
	
\bigskip	
	
Examples of patterns are: $\blue \mathtt{3.1}, \mathtt{true}, \mathtt{n}, \mathtt{x}, \mathtt{5}, \mathtt{\_}$



\bigskip
\pause

\begin{itemize}
\item A pattern may match a value, and if so it results in an environment with bindings for every identifier in the pattern. 
\item The wildcard pattern $\mathtt{\_}$ matches any value (resulting in no binding)
\end{itemize}

\pause[3] 
\medskip

Examples:
\begin{itemize}
\item<3-> Value $\mathtt{3.1}$ matches pattern $\mathtt{x}$ resulting in environment: $\darkgreen [x \mapsto 3.1 ]$
\item<4-> Value $\mathtt{true}$ matches pattern $\mathtt{true}$ resulting in environment $\darkgreen [\, ]$
\item<5-> The {\redbrown pair} $\mathtt{(1,true)}$ matches pattern $\mathtt{(x,y)}$ resulting in environment $\darkgreen [x \mapsto 1, y \mapsto true]$
\end{itemize}
\end{frame}

\begin{frame}{Match expressions}
	
	
A {\blue match expression} $\redbrown e_m$ has the following form: \quad 
{\blue
\begin{tabular}{l}
$\mathtt{match}\ e\ \mathtt{with}$ \\
$\mathtt{|}\ \mathit{pat_1}  \to  e_1$\\
$\qquad \quad  \vdots $\\
$\mathtt{|}\ \mathit{pat_n}  \to  e_n$
\end{tabular}
}

\bigskip
\pause

A match expression $\redbrown e_m$ is evaluated as follows: 
\bigskip 
\begin{enumerate}
\item evaluate $\blue e$ to a value, say $\blue v$
\item search for the first pattern $\blue \mathit{pat_i}$ matching $\blue v$
\item evaluate $\blue \mathit{e_i}$ in an environment enriched with the bindings from the pattern matching 
\end{enumerate}


\bigskip 
\pause
If no pattern matches $\blue v$, then the evaluation terminates abnormally.

\end{frame}




\begin{frame}[fragile]\frametitle{Example: Match on a pair }

Let $\redbrown e_1$ be given by: \ \
{\blue \begin{tabular}{l}
\verb!match (3+5, 3<5) with!\\
\verb!| (0, _)     -> 0!\\         
\verb!| (n,false)  -> -n!\\
\verb!| (n,_)      -> 2*n!
\end{tabular}}

\pause
\bigskip


Evaluation:
\[\blue
\begin{array}{ll}
&  {\redbrown e_1}  \\
\leadsto & (\mathtt{2 * n}, {\darkgreen [\mathtt{n} \mapsto 8]}) \\
\leadsto & (\mathtt{2 * 8} , {\darkgreen [\mathtt{n} \mapsto 8]})  \\
\leadsto & \mathtt{16}
\end{array}
\]

%\bigskip 
%Environments are occasionally left out leading to more compact evaluations.  


\end{frame}




\begin{frame}[fragile]\frametitle{Example: Match expression in a declaration}
	%\begin{frame}{Recursive declaration. Example $\color{Blue}n!$}
Function declaration:
\begin{alltt}\color{Blue}
let rec fact n = 
   match n with
   | 0 -> 1               (*  i *)
   | n -> n * fact(n-1)   (* ii *)
\ett{val fact : int -> int}
\end{alltt}
	
\pause
	
Evaluation:
	\[
	\begin{array}{llrr}
	&  \mathtt{fact(3)} & & \\
	\leadsto & \mathtt{3 * fact(3-1)} & (ii)& \onslide<3->{\darkgreen
		[\mathtt{n} \mapsto 3]} \\
	\leadsto & \mathtt{3 * 2 * fact(2-1)} & (ii)
	&\onslide<4->{\darkgreen
		[\mathtt{n} \mapsto 2]}\\
	\leadsto & \mathtt{3 * 2 * 1 * fact(1-1)} &
	(ii)&\onslide<5->{\darkgreen
		[\mathtt{n} \mapsto 1]} \\
	\leadsto & \mathtt{3 * 2 * 1 * 1} & (i)&\onslide<6->{\darkgreen
		[\mathtt{n} \mapsto 0]} \\
	\leadsto & \mathtt{6} & &
	\end{array}
	\]

\pause[7]
A match with a {\redbrown when} clause and an {\redbrown exception}:
\begin{alltt}\color{Blue}
let rec fact n = 
   match n with
   | 0           -> 1                  
   | n{\redbrown when n>0}  -> n * fact(n-1)
   | _           ->{\redbrown failwith "Negative argument"}
\end{alltt}
	
	
\end{frame}





\begin{frame}[fragile]%[containsverbatim]
	\frametitle{Recursion. Example $\color{Blue}x^n = x \cdot \ldots \cdot x$, $\color{Blue}n$
		occurrences of $\color{Blue}x$}
	
	\textcolor{BlueViolet}{Mathematical definition}: \hfill
	{\darkgreen recursion formula}
	\[\begin{array}{lclrr}
	x^0  & = & 1 & &\ \ \ \ \ \ \ \ \ \ \ \ \ (1)\\
	x^n  & = & x \cdot x^{n-1}, & \mbox{for $n > 0$} & (2)
	\end{array}
	\]
	
	\pause
	\bigskip
	
	\textcolor{BlueViolet}{Function declaration:}
\begin{alltt}
let rec power(x,n) = 
   match (x,n) with  
   | (\_,0) -> 1.0                (* 1 *)
   | (x,n) -> x * power(x,n-1)   (* 2 *)
\end{alltt}
	
	\pause
	\bigskip
	
	\textcolor{BlueViolet}{Patterns}:
	\begin{description}
		\item[${\blue \mathtt{(\_,0)}}$] matches any {\darkgreen pair} of
		the form $(u,0)$.
		\item[${\blue \mathtt{(x,n)}}$] matches any pair
		$(u,i)$ {\darkgreen yielding} the bindings
		\[\redbrown \mathtt{x} \mapsto u, \mathtt{n} \mapsto i \]
	\end{description}
	
	\pause
	\bigskip
	\begin{center}
		\redbrown 	Can you simplify the program?
	\end{center}

	
\end{frame}



\begin{frame}[fragile]%[containsverbatim]
	\frametitle{Evaluation. Example: \color{BlueViolet}\texttt{power(4.0, 2)}}
	
{\blue Function declaration}:
\begin{alltt}
let rec power(x,n) =
   match (x,n) with 
   | (\_,0) -> 1.0                  (* 1 *)
   | (x,n) -> x * power(x,n-1)     (* 2 *)
\end{alltt}
	
	\medskip
	
	{\blue Evaluation}:
	\[\begin{array}{lll}
	& \mathtt{power(4.0, 2)} & \\
	\leadsto &  \mathtt{4.0 * power(4.0, 2-1)} & \mbox{Clause 2,
		$[\mathtt{x} \mapsto 4.0, \mathtt{n}
		\mapsto 2]$} \\
	\leadsto &  \mathtt{4.0 * power(4.0, 1)} & \\
	\leadsto &  \mathtt{4.0 * (4.0 * power(4.0,1-1))} & \mbox{Clause
		2, $[\mathtt{x} \mapsto 4.0, \mathtt{n}
		\mapsto 1]$}\\
	\leadsto &  \mathtt{4.0 * (4.0 * power(4.0,0))} & \\
	\leadsto &  \mathtt{4.0 * (4.0 * 1)} & \mbox{Clause 1}\\
	\leadsto & 16.0 &
	\end{array}
	\]
\end{frame}




%\subsection{Types}
\begin{frame}{Types --- every expression has a type \color{BlueViolet}$e : \tau$}

Basic types: \ \ \

\begin{tabular}{l|l|l}
   & type name & example of values \\ \hline
Integers & \texttt{int}  & \tttilde 27,\ 0,\ 15,\ 21000\\
Floats    & \texttt{float} & \tttilde 27.3,\ 0.0,\ 48.21\\
Booleans & \texttt{bool} & true,\ false
\end{tabular}

\bigskip \pause

Pairs:\ \ \

\begin{tabular}{lr}
If $e_1: \tau_1$ and $e_2: \tau_2$ & \\
then $(e_1, e_2) : \tau_1 {\blue *} \tau_2$ & \ \ \ \ \ \ \ \ \
{\blue pair (tuple) type constructor}
\end{tabular}

\pause
\bigskip

Functions:\ \

\begin{tabular}{lr} if $f: \mbox{$\tau_1$
\texttt{\blue ->} $\tau_2$}$ and $a: \tau_1$ &
\ \ \ \ {\blue function type constructor}\\
then $f(a) : \tau_2$ &
\end{tabular}

\pause
\bigskip

Examples:

\medskip

\begin{tabular}{lr}
\begin{minipage}{6.2cm}
\texttt{\color{OliveGreen} (4.0, 2): float*int}

\texttt{\color{OliveGreen} power: float*int -> float}

\texttt{\color{OliveGreen} power(4.0, 2): float}
\end{minipage}
& \begin{minipage}{6cm} \redbrown \texttt{*} has higher precedence
that \texttt{->}
\end{minipage}
\end{tabular}
\end{frame}




\begin{frame}[fragile]
  \frametitle{Type inference: \color{BlueViolet}\texttt{power}}

\begin{alltt}\color{BlueViolet}
let rec power (x,n) = 
   match (x,n) with
   | (\_,0) -> 1.0                 (* 1 *)
   | (x,n) -> x * power(x,n-1)    (* 2 *)
\end{alltt}

\medskip

\begin{itemize}
\item<2-> The type of the function must have the form: $\tau_1$
\texttt{*} $\tau_2$ \texttt{->} $\tau_3$, because argument is a
pair.

\item<3-> $\tau_3$ = \texttt{float} because \texttt{1.0:float}\hfill
(Clause 1, function value.)

\item<4-> $\tau_2$ = \texttt{int} because \texttt{0:int}.

\item<5-> \texttt{x*power(x,n-1):float},
  because $\tau_3$ = \texttt{float}.

\item<6-> multiplication can have
\begin{center}
\texttt{int*int -> int}\ \  or\ \  \texttt{float*float -> float}
\end{center}
as types, but no ``mixture'' of \texttt{int} and \texttt{float}

\item<7-> Therefore \texttt{x:float} and $\tau_1$=\texttt{float}.
\end{itemize}

\medskip

\onslide<8->{\redbrown The F\# system determines the type
\texttt{\blue float*int -> float}}

\end{frame}


	
\begin{frame}%[fragile]
\frametitle{A {\redbrown higher-order} version of the power function}


We shall now look at a version of $\blue \mathtt{power}\ x\ n = x^n$ with the type
\begin{alltt}\blue 
power: float ->\ {\redbrown (int -> float)}
\end{alltt}\pause
\begin{itemize}
\item<2-> the argument of power is the base $\blue x$
\item<3-> and $\blue \mathtt{power}\ x$ is the function that maps exponent $\blue n$ to $\blue x^n$ 
\end{itemize}

\bigskip
\pause[4]

The function may be evaluated in {\em\redbrown stages}: 
\begin{alltt}
let pow2 = power 2.0;;\\
\ \\
pow2 3;;\\
\ett{val it : float = 8.0}\\
pow2 4;;\\
\ett{val it : float = 16.0}\\
\end{alltt}

\bigskip
\pause[5]

This {\redbrown higher-order} version of power is declared by
\begin{alltt}\blue
let rec power\ {\redbrown x n} = match n with\\
\ \ \                    | 0  -> 1.0\\
\ \ \                    | \_  -> x * power\ {\redbrown x (n-1)};;
\end{alltt}
\pause
\medskip

\begin{center}
 {\redbrown The value of the function is a function}	
\end{center}
%\pause
%\bigskip
%A {\redbrown curried} version: \hfill  {\darkgreen what is the type?}	
%\begin{alltt}\blue 	
%let rec power x = function
%   | 0          -> 1.0
%   | n{\redbrown when n<0} -> failwith "power: negative exponent"
%   | n          -> x * power x (n-1);;  
%	\end{alltt}	
\end{frame}	



\begin{frame}[fragile]
\frametitle{A expression for anonymous functions}

The function expression
\begin{alltt}\blue
		function
		|\ \(\mathit{pat}\sb{1} \to e\sb{1} \)
		\( \vdots \) 
		|\ \(\mathit{pat}\sb{n} \to e\sb{n} \)      
\end{alltt}
allows you to ``tabulate'' argument-value pairs of a function.

\begin{alltt}
	function
	| 2  -> 28   // February
	| 4  -> 30   // April
	| 6  -> 30   // June
	| 9  -> 30   // September
	| 11 -> 30   // November
	| _  -> 31;; // All other months
	\ett{\blue val it : int -> int = <fun:clo@17-2>}
\end{alltt}
\pause
\begin{alltt}
	it 2;;
	\ett{val it : int = 28}
\end{alltt}
\end{frame}


\begin{frame}%[fragile]
\frametitle{Another  {\redbrown higher-order} version of the power function}

We now have another look at $\blue \mathtt{power}\ x\ n = x^n$ with the type
\begin{alltt}\blue 
	power: float -> (int -> float)
\end{alltt}

\bigskip
\pause

The following declaration explicitly reveals that  $\blue \mathtt{power}\ x$ is a function:
\begin{alltt}\blue
let rec power x =\\ 
\ \ \ function\\
\ \ \ | 0  -> 1.0\\
\ \ \ | n  -> x * power x (n-1);;
\end{alltt}

\end{frame}	


\begin{frame}{Booleans}

{\blue Type name} \texttt{bool}

\medskip

{\blue Values} \texttt{false},\ \ \texttt{true}

\medskip

\begin{tabular}{lr}
	\begin{tabular}{l|l|l}
		{\blue Operator} & {\blue Type} & \\ \hline \texttt{not} &
		\texttt{bool -> bool} & negation
	\end{tabular} %
	\hspace{.7cm}\framebox{\redbrown
		\begin{tabular}{l}
			\texttt{not true = false}\\
			\texttt{not false = true}
		\end{tabular}
	}
\end{tabular}

\pause
\bigskip



{\blue Expressions}
\[ \begin{array}{lll}
e_1\ \mbox{\color{OliveGreen} \&\&}\
e_2 & \quad
& \mbox{\color{OliveGreen} ``conjunction $e_1
	\wedge e_2$''}\\
e_1\ \mbox{\color{OliveGreen} \texttt{||}}\
e_2 & \quad
&\mbox{\color{OliveGreen} ``disjunction $e_1
	\vee e_2$''}
\end{array}
\]

\pause \medskip

{\blue --- are {\redbrown lazily} evaluated, e.g.}\hspace{1cm}
\framebox{\redbrown \begin{tabular}{l}\texttt{1<2 || 5/0 = 1}\\
		$\lto$\ \texttt{true}\end{tabular}}

\bigskip
{\blue Precedence}:\ \  \texttt{\color{OliveGreen} \&\&} has
{\redbrown higher} than \texttt{\color{OliveGreen} ||}
\end{frame}

	
	
\begin{frame}{Summary}
\begin{itemize}
\item The interactive environment

\item Values, expressions, types, patterns

\item Declarations of
  values and recursive functions

\item Binding, environment and evaluation

\item Type inference

\item higher-order functions
\end{itemize}



\end{frame}




\begin{frame}{Part 2: Lists}

\begin{itemize}

\item Lists: values and constructors

\item Recursions following the structure of lists

\item Polymorphism

\end{itemize}

\bigskip

\begin{itemize}
	\item The list concept is a natural, built-in ingredient of functional languages 
\end{itemize}

\end{frame}


\begin{frame}{Lists}
	
	A list is a finite sequence of elements having the same type:
	\[
	{\blue [v_1; \ldots; v_n]} \qquad \mbox{({\blue $[\, ]$} is called
		the empty list)}
	\]
	
	\bigskip
	\pause
	
	\begin{alltt}
		[2;3;6];;\\
		\ett{val it : int list = [2; 3; 6]}
	\end{alltt}
	
	\pause
	
	\begin{alltt}
		["a"; "ab"; "abc"; ""];;\\
		\ett{val it : string list = ["a"; "ab"; "abc"; ""]}
	\end{alltt}
	
	\pause
	
	\begin{alltt}
		[sin; cos];;\\
		\ett{val it : (float->float) list = [<fun:...>; <fun:...>]}
	\end{alltt}
	
	\pause
	
	
	\begin{alltt}
		[(1,true); (3,true)];;\\
		\ett{val it : (int * bool) list = [(1, true); (3, true)]}
	\end{alltt}
	
	\pause
	
	\begin{alltt}
		[[]; [1]; [1;2]];;\\
		\ett{val it : int list list = [[]; [1]; [1; 2]]}
	\end{alltt}
	
\end{frame}
	

\begin{frame}[fragile]
	\frametitle{List constructors}

A non-empty list $\blue [x_1; x_2; \ldots; x_n]$, $n\geq 1$,
consists of
\begin{itemize}
	\item a {\em\redbrown head} $\blue x_1$ and 
	\item a {\em\redbrown
		tail} $\blue [x_2; \ldots; x_n]$
\end{itemize}

\bigskip
\pause

The list type has two constructors:
\begin{itemize}
	\item The empty list $\blue [ ]$
	\item The {\redbrown cons} constructor  $\blue x_1 \verb!::! [x_2; \ldots; x_n] = [x_1; x_2; \ldots; x_n]$
\end{itemize}
-- they are used to {\darkgreen construct} and to {\redbrown decompose} lists





\end{frame}







%\subsection{Recursion on lists}
\begin{frame}[fragile]
	\frametitle{Recursion on lists  -- a simple example}
	\vspace{-.8cm}
	\[
	{\tt suml}\, \verb?[?x_1\verb?;? x_2\verb?;? \ldots
	\verb?;?x_{n}\verb?]? = \sum_{i=1}^{n} x_i = x_1 + x_2 + \cdots +
	x_{n} = x_1 + \sum_{i=2}^{n} x_i
	\]
	
	\pause
	
	\ \hfill {\darkgreen Constructors are used in list patterns}
\begin{alltt}
let rec suml xs = 
   match xs with
   |{\darkgreen []}      -> 0
   |{\darkgreen x::tail} -> x + suml tail;;
\ett{val suml : int list -> int}
\end{alltt}
	
	\pause
	
	\[
	\begin{array}{lll}
	& \verb/suml [1;2]/ &   \\
	\lto & \verb/1 + suml [2]/ &
	{\rm (\verb/x/ \mapsto \verb/1/\
		and\ \verb/tail/ \mapsto \verb/[2]/)}\\
	\lto & \verb/1 + (2 + suml [])/ &
	{\rm (\verb/x/ \mapsto \verb/2/\
		and\ \verb/tail/ \mapsto \verb/[]/)}\\
	\lto & \verb/1 + (2 + 0)/ &
	{\rm (the\ pattern\ {\darkgreen \verb/[]/}\ matches\ the\ value\ \verb/[]/)}\\
	\lto & \verb/1 + 2/ & \\
	\lto  & \verb/3/  &
	\end{array}
	\]
	
	\hfill {\redbrown Recursion follows the structure of lists}
	
\end{frame}



\begin{frame}[fragile]
	\frametitle{A {\redbrown polymorphic} list function (I)}
	
	The function {\blue remove y xs} gives the list obtained from {\blue xs} by deleting every occurrence of $\blue y$, e.g.\ $\blue \verb|remove|\ 2\ [1;2;0;2;7] = [1;0;7]$.
	
	\medskip
	Recursion is following the structure of the list:
	
\begin{alltt}\blue
let rec remove y xs =
   match xs with 
   | []               -> []
   | x::tail when x=y -> remove y tail
   | x::tail          -> x::remove y tail;;	
   \end{alltt}
	
	\pause
	
	List elements can be of {\redbrown any type} that supports {\redbrown equality} 
	%-- $\redbrown \verb|'a|$ is a type variable:
	\begin{alltt} \blue
		remove : {\redbrown 'a} ->{\redbrown 'a} list ->{\redbrown 'a} list when{\redbrown'a : equality}
	\end{alltt}

\pause

\begin{itemize}
\item {\redbrown \verb-'a-} is a {\blue\em type variable}
\item {\redbrown'a : equality} is a type constraint
\end{itemize}

\pause\bigskip
\begin{center}
The F\# system infers the  {\darkgreen most general type} for {\blue remove} 
\end{center}

\end{frame}


\begin{frame}[fragile]
\frametitle{A {\redbrown polymorphic} list function (II)}
\begin{itemize}
	\item A type containing type variables is called a {\redbrown polymorphic type}
	\item The remove function is called a {\redbrown polymorphic function}.
\end{itemize}
\vspace*{-.6cm}
\begin{alltt} \blue
	remove : 'a -> 'a list -> 'a list when 'a : equality
\end{alltt}


The function has {\redbrown many forms}, one for each instantiation of {\blue 'a}:

\pause
\medskip



Instantiating {\blue \verb|'a|} with {\blue \verb|int|}:
\begin{alltt}\blue
remove 2 [1; 2; 0; 2; 7];;  
\ett{val it : int list = [1; 0; 7]}
\end{alltt}
	
\pause
\bigskip
	
Instantiating {\blue \verb|'a|} with {\blue \verb|int list|}:	
\begin{alltt}\blue
remove [2] [[2;1]; [2]; [0;1]; [2]; [5;6;7]];;  
\ett{val it : int list list = [[2; 1]; [0; 1]; [5; 6; 7]]}
\end{alltt}	

\pause 
\bigskip
Notice that \verb|->| {\redbrown associates to the right}: 
\begin{alltt}\blue 
'a -> 'a list -> 'a list  means 'a -> ('a list -> 'a list)
\end{alltt}

\end{frame}


\begin{frame}[fragile]
	\frametitle{Exploiting {\darkgreen structured} patterns: the {\blue isPrefix} function}
	
	The function $\blue \verb|isPrefix|\ xs\ ys$ tests whether the list $\blue xs$ is a prefix of the list 
	$\blue ys$, for example:
	\[\blue
	\begin{array}{lcl}
	\verb|isPrefix|\ [1;2;3]\ [1;2;3;8;9] & = & \mathrm{true}\\
	\verb|isPrefix|\ [1;2;3]\ [1;2;8;3;9] & = & \mathrm{false}\\ 
	\end{array}\]
	
	\pause
	\bigskip
	
The function is declared as follows:
	
\begin{alltt}\blue
let rec isPrefix xs ys =
   match (xs,ys) with
   | ([],_)              -> true
   | (_,[])              -> false
   | (x::xtail,y::ytail) -> x=y && isPrefix xtail ytail;;
		
isPrefix [1;2;3] [1;2];;
\ett{val it : bool = false}
	\end{alltt}
	
	\medskip
	\pause
	A each clause expresses succinctly a natural property:
	\begin{itemize}
		
		\item<4-> The empty list is a prefix of any list
		
		\item<5-> A non-empty list is not a prefix of the empty list
		
		\item<6-> A non-empty list (...) is a prefix of another non-empty list (...) if ...
	\end{itemize}
	
%	\bigskip
%	\pause[4]
%	
%	\textcolor{BrickRed}{Suitable use of infix functions can increase
%		readability significantly}
	
\end{frame}

\begin{frame}%[fragile]
	\frametitle{Summary}
	
	\begin{itemize}
		\item Lists
		\item<2-> Polymorphism
		\item<3-> Constructors (:: and [] for lists)
		\item<4-> Patterns
		\item<5-> Recursion on the structure of lists
		\item<6-> Constructors used in {\blue patterns} to {\redbrown decompose} structured values
		\item<7-> Constructors used in {\blue expressions} to {\redbrown compose} structured values
	\end{itemize}	
	
\bigskip
\pause[8]	
	
Blackboard exercises
\begin{itemize}
\item $\blue \mathtt{memberOf}\ x\ ys$ is true iff $\blue x$ occurs in the list $\blue ys$

\item $\blue \mathtt{insert}(x, ys)$ is the {\em ordered list} obtained from the {\em ordered list} $\blue ys$ by insertion of $\blue x$
%
\item  $\blue \mathtt{sort}(xs)$ gives a ordered version of $\blue xs$ 
\end{itemize}
	
\end{frame}	

\end{document}

