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

\input{../Common/common}



\subtitle{Lecture 2: Functions, Types and Lists} % (optional)
\date {MRH 10/09/2024}


%\beamerdefaultoverlayspecification{<+->}

\begin{document}

\begin{frame}
  \titlepage


\end{frame}

\begin{frame}{Outline}

\begin{itemize}	
    \item Functional decomposition
\end{itemize}	
\ \hfill {\darkgreen short break}

\bigskip

\begin{itemize}	
\item Functions as "first-class citizens"
	
\begin{itemize}	\item Anonymous functions
\end{itemize}
\end{itemize}
\ \hfill {\darkgreen short break}	
	
\bigskip	
	
\begin{itemize}	\item Types, type inference and overloading


\begin{itemize}    
\item Tuples and equality and comparison constraints 
\end{itemize}
\end{itemize}		

\ \hfill {\darkgreen short break}	

\bigskip

\begin{itemize}
	\item Let expressions and lists 
\end{itemize}	

\end{frame}



\begin{frame}
\begin{center}\redbrown\Large
On functional decomposition
\end{center}
\end{frame}



\begin{frame}{Functional decomposition}
A simple technique when solving a complex problem is
\begin{itemize}
	\item to partition it into smaller well-defined parts and, thereafter, 
	\item to compose these parts to solve the original problem.
\end{itemize}	


\pause
\bigskip

The main goal is that a program is constructed by 
\begin{itemize}
\item  combining simple well-understood pieces
\end{itemize}

\pause
\bigskip

\begin{center}\redbrown 
	Invent useful helper functions
\end{center}
\end{frame}


\begin{frame}[fragile]
\frametitle{Functional decomposition: Example 1}

Sorting a list: $\blue \verb|sort: 'a list -> 'a list when 'a : comparison|$. 

\bigskip 
\pause

Insertion in an ordered list is easy:
\begin{alltt}\blue 
(* insert:'a -> 'a list -> 'a list when 'a : comparison *)\pause
let rec insert x ys = 
   match ys with 
   | []               -> [x]
   | y::_ when x <= y -> x::ys
   | y::ytail         -> y::insert x ytail  	
\end{alltt}
 
\pause 
\bigskip

Insertion sort can now easily be implemented:
\begin{alltt}\blue 	
let rec sort xs = 
    match xs with 
    | []       -> []
    | x::xtail -> insert x (sort xtail) 
\end{alltt}


\pause 
\bigskip
\begin{itemize}
\item small comprehensible programs
\end{itemize}

\pause 

Notice: {\redbrown there are better sorting algorithms than insertion sort}


\end{frame}




\begin{frame}[fragile]
\frametitle{Functional decomposition: Example 2}

Consider multiplication of polynomials:
\[
\begin{array}{ll}
0 \cdot Q(x)    & = 0 \\
\multicolumn{2}{l}{
	(a_0 + a_1 \cdot x + ... + a_n \cdot x^n) \cdot Q(x)} \\
& =  a_0 \cdot Q(x) +
x \cdot \left( (a_1 + a_2 \cdot x + ... + a_n\cdot x^{n - 1})
\cdot Q(x) \right)
\end{array}
\]

\bigskip
\pause
Invent suitable auxiliary functions
\begin{itemize}
\item<2->  $a_0{\blue \cdot} Q(x)$ \hfill {\darkgreen $\verb|mulC: int -> Poly -> Poly|$ }

\item<3-> ${\blue x \cdot} ( \ldots )$ \hfill {\darkgreen $\verb|mulX: Poly -> Poly|$ }

\item<4->  $a_0 \cdot Q(x){\blue +}
x \cdot ( \ldots )$  \hfill {\darkgreen $\verb|add: Poly -> Poly -> Poly|$ }
\end{itemize}	


\bigskip
\pause[5]
\begin{center}\redbrown 
	That makes the task of declaring multiplication easier
\end{center}

\end{frame}





\begin{frame}[fragile]\frametitle{Invent helper function(s): Blackboard exercise}

Declare a function $\blue\verb?sumProd: int list -> int*int?$:\\[1cm]


{\blue \begin{tabular}{lcl}
		\multicolumn{3}{l}{
			{\tt sumProd}\ {\tt [}$x_0${\tt ;}$x_1${\tt ;} $\ldots${\tt ;}$x_{n-1}${\tt ]}
		} \\
		& = &
		{\tt (} $x_0$ {\tt +} $x_1$ {\tt +} $\ldots$ {\tt +} $x_{n-1}$ {\tt ,}
		$x_0$ {\tt *} $x_1$ {\tt *} $\ldots$ {\tt *} $x_{n-1}$ {\tt )} \\
		{\tt sumProd []} &=& {\tt (0,1)}
\end{tabular}}

\end{frame}


\begin{frame}
\begin{center}\redbrown\Large
	On functions as first-class citizens 
\end{center}
\end{frame}


\begin{frame}%[fragile]
\frametitle{Functions as {\darkgreen "first-class citizens"}}
	
	\begin{itemize}
		\item functions can be passed as arguments to functions
		\item functions can be returned as values of functions
	\end{itemize}	
	\pause
	like any other kind of value.
	

	
	\pause\bigskip
	
	\begin{center}\redbrown
		There is nothing special about functions in functional languages
	\end{center}
	
	\bigskip
	\pause

A function that takes a function as argument or produces a function as result is also called a {\blue higher-order function}.

\bigskip
\pause

Higher-order functions are {\redbrown useful}
\begin{itemize}
\item succinct code
\item highly parameterized programs 
\item Program libraries typically contain many such functions 
\end{itemize}
\end{frame}	



\begin{frame}[fragile]
\frametitle{An example}

Suppose that we have a cube with side length $\blue s$,
containing a liquid with density $\blue \rho$. The weight of the liquid is then
given by $\blue \rho \cdot s^3$:

\begin{alltt}\blue
	let weight ro s = ro * s ** 3.0;;
	\ett{val weight : float -> float -> float}
\end{alltt}

\pause

We can make {\em\redbrown partial evaluations} to define functions for
computing the weight of a cube of either water or methanol:
\begin{alltt}\blue
	let waterWeight = weight 1000.0;;
	\ett{val waterWeight : (float -> float)}
	
	waterWeight 2.0;;
	\ett{val it : float = 8000.0}
\end{alltt}

\pause

\begin{alltt}\blue
	let methanolWeight = weight 786.5 ;;
	\ett{val methanolWeight : (float -> float)}
	
	methanolWeight 2.0;;
	\ett{val it : float = 6292.0}
\end{alltt}

\medskip
\pause
\begin{center}\redbrown The formula {$\blue \rho \cdot s^3$} is represented {\darkgreen just once} in the program \end{center}
\end{frame}



\begin{frame}[fragile]\frametitle{Currying and Uncurrying}

The process of turning a function on pairs (tuples) into a higher-order function is called {\blue currying}. The opposite process is called {\blue uncurrying}.

\bigskip
\pause

Consider declarations:
\begin{alltt}\blue
let wC ro s = ro * s ** 3.0;;
\ett{val wC : float -> float -> float}

let wUC(ro, s) = ro * s ** 3.0;;
\ett{val wUC : ro:float * s:float -> float}
\end{alltt}

\begin{itemize}
\item {\blue \verb|wC|} is the curried version of {\blue \verb|wUC|}

\item {\blue \verb|wUC|} is the uncurried version of {\blue \verb|wC|}
\end{itemize}

\bigskip
\pause
Have a look at exercise HR 2.13: 
\begin{itemize}
\item declare functions for curring and uncurring.
\end{itemize}
\begin{alltt}\blue
curry:   ('a * 'b -> 'c) -> 'a -> 'b -> 'c
uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c	
\end{alltt}
\end{frame}



\begin{frame}[fragile]
\frametitle{A well-known example: function composition}%A function for which the argument and value are functions}

Function composition: {\redbrown $(f \circ g)(x) = f(g(x))$}

\bigskip

%If $\blue f: A \to B$ and $\blue g: C \to A$, then $\blue f \circ g : C \to B$

%\medskip
For example, if $\blue f(y) = y+3$ and $\blue g(x) = x^2$, then $\blue (f \circ\ g)(z) = z^2 +3$.

\bigskip
\pause

The {\darkgreen infix} operator {\redbrown \verb-<<-} in F{\#} denotes function composition:
\begin{alltt}\blue
	let f y = y+3;;        
	
	let g x = x*x;;        
	
	let h = f << g;;       // h = (f o g)
	\ett{val h : int -> int}
	
	h 4;;                  // h(4) = (f o g)(4)
	\ett{val it : int = 19}
\end{alltt}

\begin{itemize}
\item An infix operator appears between the arguments
\end{itemize}
%\medskip

%\pause \ \hfill {\redbrown Declaration of  (\verb!<<!) ?}

%\medskip

%\pause \ \hfill {\redbrown Type of (\verb!<<!) ?}

\end{frame}


\begin{frame}[fragile]
\frametitle{Infix functions}

The prefix version $\blue (\oplus)$ of an infix operator $\blue \oplus$ is a {\redbrown curried function},
that is, higher-order function where argument are supplied one by one

\bigskip

For example:
\begin{alltt}\blue
(<<);;
\ett{val it : (('a -> 'b) -> ('c -> 'a) -> 'c -> 'b)}
\end{alltt}

\begin{itemize}
\item<2-> The argument is a function $\blue \verb|'a -> 'b|$
\item<3-> The value is a function   $\blue \verb|('c -> 'a) -> 'c -> 'b|$
\end{itemize}

\pause[4]
\bigskip

Declaration \hfill{\redbrown \verb|<<| is a built-in function}
\begin{alltt}\blue 
let (<<) f g x = f(g x);;	
\end{alltt}

\pause[5]
\bigskip

 
Infix operators are written as strings of special characters including
{\blue
\begin{verbatim}
   !  %  &  *  +  -  /  <  =  >  ?  @  ^  \  ~
\end{verbatim}}
Consult F\# specification for complete rules.

\end{frame}



\begin{frame}[fragile]{The built-in infix function \texttt{\blue @} }

{\blue List.append} is a higher-order function from the $\blue\verb|List|$ library:

\begin{itemize}
	\item $\blue \mathtt{List.append}\, [x_0; \ldots; x_{n-1}]\, [y_0; \ldots; x_{m-1}]  =$\\
	\qquad  $\blue [x_0; \ldots; x_{n-1}; y_0; \ldots; x_{m-1}]$
\end{itemize}
\bigskip
\pause 
There is a convenient infix notation for $\blue \verb|List.append|\, xs\, ys$ in F\#:
\begin{center}\blue	
	$xs\, \verb|@|\, ys$
\end{center}

\bigskip
\pause 
The declaration of $\blue (\verb|@|)\ xs\ ys$ follows the structure of $\blue xs$: 

\begin{alltt}\blue
let rec{\redbrown (@)} xs ys = 
    match xs with 
    | []       -> ys
    | x::xtail -> x::(xtail{\redbrown @} ys);;
\ett{val ( @ ) : 'a list -> 'a list -> 'a list}
\pause
	
[["a"]; ["ab";"abc"; ""]; []] @ [["x"]; ["xy"; "xyz"]];; 
\ett{val it : string list list =}
\ett{    [["a"]; ["ab"; "abc"; ""]; []; ["x"]; ["xy"; "xyz"]]}
\end{alltt}

\end{frame}


\begin{frame}
\begin{center}\redbrown\Large
	On anonymous functions
\end{center}
\end{frame}



\begin{frame}[fragile]
\frametitle{Function expressions}

There are two kinds of expression for {\blue anonymous functions}

\bigskip
\begin{itemize}
	\item One originates from {\redbrown abstraction} $\redbrown \lambda x. e$ in the lambda calculus: 
\begin{alltt}\blue 
fun x \( \to e \)
\end{alltt}
reads: ``the function of $\blue x$ given by $\blue e$''.

 
\bigskip 
\pause

\item The other support pattern matching:
\begin{alltt}\blue
function
|\ \(\mathit{pat}\sb{1} \to e\sb{1} \)
      \( \vdots \) 
|\ \(\mathit{pat}\sb{n} \to e\sb{n} \)      
\end{alltt}
\end{itemize}

\bigskip
\noindent
\begin{center}\redbrown 
You can write functions without naming them	
\end{center}
\end{frame}




\begin{frame}[fragile]
\frametitle{Anonymous functions: Example 1}

An expressions denoting the circle-area function
\begin{alltt}\blue
	fun r -> System.Math.PI * r * r ;;
	\ett{val it : float -> float = <fun:clo@10-1>}
	
	it 2.0 ;;
	\ett{val it : float = 12.56637061}
\end{alltt}

\end{frame}

\begin{frame}[fragile]
\frametitle{Anonymous functions: Example 2}	
An anonymous function computing the number of days in a month:
\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{Anonymous functions: Example 3}

Function expressions with general patterns, e.g.\

\begin{alltt}\blue
function
| 2        -> 28  // February
|4|6|9|11  -> 30  // April, June, September, November
| _        -> 31  // All other months
;;
\end{alltt}

\pause
\medskip

Exploits an {\redbrown or pattern} in the second clause
\end{frame}




\begin{frame}[fragile]
\frametitle{Simple functions expressions with {\em\redbrown currying}}

The expression 
\[\blue
\mathtt{fun}\ x\ y\ \cdots\ z\ \to e
\]
has the same meaning as
\[\blue
\mathtt{fun}\ x \to (\mathtt{fun}\ y \to ( \cdots\ (\mathtt{fun}\ z \to e) \cdots ))
\]
\pause
It denotes a function with type
\[\blue 
t_x \to (t_y \to  (\cdots (t_z \to t_e) \cdots ))\ \mbox{where $x:t_x, y:t_y, z:t_z$ and $e:t_e$} 
\]

\medskip
\pause

For example: The function below takes an integer as argument and returns a function of type {\redbrown \verb!int -> int!} as value:
\begin{alltt}\blue
fun x y -> x + x*y;;
\ett{val it : int -> {\redbrown int -> int} = <fun:clo@2-1>}
\end{alltt}

\pause

\begin{alltt}\blue
let f = it 2;;
\ett{val f : ({\redbrown int -> int})}
\end{alltt}
\pause

\begin{alltt}\blue
f 3;;
\ett{val it : int = 8}
\end{alltt}

\end{frame}



\begin{frame}

\begin{center}\Large\redbrown
	On types, type inference and overloading
\end{center}


\end{frame}




\begin{frame}{Types and type checking}

Purposes:
\begin{itemize}
\item Modelling, readability: types are used to indicate the intention behind a program

\bigskip

\item<2-> Safety, efficiency: "Well-typed programs do not go wrong"\\ 
\ \hfill Robin Milner

\begin{itemize}
	\item<3-> Catch errors at compile time
	
	\medskip
	
	\item<4-> Checks of types are not needed at runtime
\end{itemize}
\end{itemize}

\bigskip\pause[5]

A type checker is an algorithm used at an early phase in the compiler to reject programs containing type errors.


\bigskip\pause[6]

Type inference is an algorithm to automatically calculate types of expressions without use of explicit type annotations.

\end{frame}

\begin{frame}{Fundamental type-checking problem}
\vspace*{-12mm}
\begin{center}\redbrown 
	All non-trivial semantic properties of programs are undecidable
\end{center}
\ \hfill {\darkgreen Rice's theorem}

\bigskip
\pause
Example: $\blue p$ terminates on all its input

\pause
\bigskip 

Cannot be checked for programs belonging to Turing-powerful languages

\pause\bigskip

Consequence: A type-checking algorithm provides an {\darkgreen approximation}:

\bigskip

\begin{tikzpicture}
\filldraw[color=red!60, fill=red!40, very thick](10,0) circle (1.5);
\filldraw[color=blue!60, fill=blue!40, very thick](10,0) circle (1);
\draw[color=green!60, fill=green!40, very thick](10,0) circle (0.7);
\filldraw[red] (4.75,1.2) node{ill-typed, bad programs};
\filldraw[blue] (4.85,0.70) node{ill-typed, good programs};
\filldraw[green] (5,0.0) node{well-typed, good programs};
%\filldraw[color=red!60, fill=red!40, very thick](10,0) circle (1.5);
\end{tikzpicture}
\end{frame}


\begin{frame}[fragile]\frametitle{Type inference}

%The F\# compiler automatically infers types for every expression in a program. 
%
%\pause 
%\bigskip

The type system of F\# allows for {\blue polymorphic types}, that is, types with many forms. Polymorphic types are expressed using type variables {\redbrown 'a, 'b, 'c, .... } 

\pause 
\bigskip

The {\em\redbrown most general type} or {\em\redbrown principal type} is inferred by the system. 

\medskip

Examples:
\begin{alltt}\blue
let id x = x      
\ett{val id : 'a -> 'a}

let pair x y = (x,y)	
\ett{val pair : 'a -> 'b -> 'a * 'b}
\end{alltt}
  
\pause\bigskip
The inferred types are most general in the sense that all other types for {\blue id} and {\blue pair} are {\redbrown instances} of the inferred types.  \\
%\ \hfill {\redbrown applications of the functions?}

\pause\bigskip
By the type of a function, we (usually) mean the most general type \\
\medskip\pause
\ \hfill {\blue Remark: identity function {\redbrown id} is a built-in function }

\end{frame}



\begin{frame}[fragile]\frametitle{Polymorphic type inference -- informally}
\vspace{-3mm}
Given a declaration, for example, 
\begin{alltt}\blue
let rec (@) xs ys = 
   match xs with 
   | []       -> ys                   {\redbrown (* C 1 *)}
   | x::xtail -> x::(xtail @ ys);;    {\redbrown (* C 2 *)}
\end{alltt}

\begin{itemize}
\item<2-> Guess types for the arguments of $\blue \verb!(@)!$:\  {\blue $xs:\mathit{'u}$}  and {\blue $ys: \mathit{'v}$} 

\medskip

\item<3->  Add type constraints based on the body of the declaration: 
\begin{enumerate}
\item {\blue \verb-[]-: 'a list} and {\blue 'u = 'a list}, where {\blue 'a} is a fresh type variable     \hfill {\redbrown C 1}\ 

\medskip

\item<4-> {\blue x: 'a,\ xtail: 'a list,\ (xtail \verb|@| ys): 'a list,\ x::(xtail \verb|@| ys): 'a list}   \hfill {\redbrown C 2} \\
exploiting the type of {\blue \verb|::|}

\medskip

\item<5-> {\blue ys : 'a list}, {\blue 'v = 'a list}     \hfill {\redbrown C 1,2}\\ 
{\blue ys} must have the same type as  {\blue x::(xtail \verb|@| ys)}
\end{enumerate} 
\end{itemize}
\pause[6]
Every sub-expression is now {\redbrown consistently} typed.

\bigskip
\pause[6]

The {\redbrown most general type} or {\redbrown principle type} of {\blue (\verb-@-)} is:
\begin{alltt}
'a list -> 'a list -> 'a list
\end{alltt}
\bigskip\pause[7]
\begin{itemize}
\item First inference algorithm for ML {\darkgreen DamasMilner82}
\item A nice introduction and F\# implementation:  {\darkgreen Sestoft12}	
\end{itemize} 
\end{frame}



\begin{frame}{Parametric and ad-hoc polymorphism - Strachey 1967}

\begin{itemize}
\item Parametric polymorphism:\\ 
-- a function can be written so that it handles values identically independent on their types 
\end{itemize}
\ \hfill {\redbrown preserving type safety}


\pause
For example, the same code for append can be used for integer lists, list of pairs, list of ... 

\bigskip
\pause

\begin{itemize}
	\item Ad-hoc polymorphism/overloading:\\ 
	-- a function has different implementations depending on the type of arguments
\end{itemize}
For example, + can be used on integers, floating-points values, strings, ...


\end{frame}




\begin{frame}{Overloaded Operators and Type inference}

{\blue A squaring function on integers:}
\medskip

\begin{tabular}{l|l|l}
	Declaration & Type & \\ \hline \texttt{let square x = x * x} &
	\texttt{int -> int} & Default
\end{tabular}

\bigskip
\pause

{\blue A squaring function on floats:} \texttt{square: float ->
	float}

\medskip

\begin{tabular}{l|l}
	Declaration & \\ \hline \onslide<3->{\texttt{let
			square({\darkgreen x}:float) = x * x}} &
	\onslide<3->{\darkgreen Type the argument}\\
	\onslide<4->{\texttt{let {\darkgreen square x}:float = x * x}} &
	\onslide<4->{\darkgreen Type the result}\\
	\onslide<5->{\texttt{let square x = {\darkgreen x * x}: float}} &
	\onslide<5->{\darkgreen Type expression for the result}\\
	\onslide<6->{\texttt{let square x = {\darkgreen x}:float * x}} &
	\onslide<6->{\darkgreen Type a variable}\\
\end{tabular}

\bigskip
\onslide<7->{\blue You can mix these possibilities}
\end{frame}

\begin{frame}

\begin{center}\Large\redbrown
	On tuples and equality and comparison constraints 
\end{center}


\end{frame}




\begin{frame}[fragile]
\frametitle{Basic types: equality and comparison}

Equality and comparison are defined for the basic types of F\#, including integers, floats, booleans, characters and strings.

\medskip

Examples:
\begin{alltt}\blue
true < false;;
\ett{val it : bool = false}

'a' < 'A';;
\ett{val it : bool = false}

"a" < "ab";;
\ett{val it : bool = true}
\end{alltt}
\end{frame}

\begin{frame}[fragile]
\frametitle{Composite Types: equality and comparison}

Equality and comparison carry over to composite types\\
\ \hfill {\redbrown  as long as function types are not involved}:

\bigskip\pause


Equality is defined {\redbrown structurally} on values with the same type:  
\begin{alltt}\blue

[[1;2]; [3;4;5]] = [[1..2]; [3..5]];;
\ett{val it : bool = true}
\end{alltt}
%(1, true, 7.4) = (2-1, not false, 8.0 - 0.6);;
%\ett{val it : bool = true}
%	

\bigskip\pause

Comparison is typically defined using {\redbrown lexicographical ordering}:
\begin{alltt}\blue
[1; 2; 3] < [1; 4];;
\ett{val it : bool = true}
	
(2, [1; 2; 3]) > (2, [1;4]);;
\ett{val it : bool = false}
\end{alltt}



\end{frame}

\begin{frame}[fragile]{Tuples}

{\blue An ordered collection of $n$ values {\redbrown $(v_1, v_2,
		\ldots, v_n)$}
	is called an {\redbrown $n$-tuple}}

\medskip

{\blue Examples}

\begin{tabular}{l|l}
	\hline
	\begin{tabular}{l}
		\verb!(3, false);!\\
		\ett{val it = (3, false) : int * bool}
	\end{tabular}
	& $2$-tuples (pairs)\\ \hline
	\begin{tabular}{l}
		\verb!(1, 2, ("ab",true));!\\
		\ett{val it = (1, 2, ("ab", true)) :} {\redbrown ?}
	\end{tabular}
	& $3$-tuples (triples)\\ \hline
\end{tabular}


\bigskip
\pause

{\blue Equality defined componentwise, ordering lexicographically}

\medskip

\begin{tabular}{l}
	\verb!(1, 2.0, true) = (2-1, 2.0*1.0, 1<2);;!\\
	\ett{val it = true : bool}\\[2mm]
%	\verb!compare (1, 2.0, true) (2-1, 3.0, false);;!\\
%	\ett{val it : int = -1}
\end{tabular}

\hfill {\redbrown provided = is defined on components}

\end{frame}



\begin{frame}[fragile]{Tuple patterns}

{\redbrown Extract components of tuples}

\medskip

\begin{tabular}{l}
\verb!let ((x,_),(_,y,_)) = ((1,true),("a","b",false));;!\\
\ett{val x : int = 1}\\
\ett{val y : string = "b"}
\end{tabular}

\medskip
{\blue Pattern matching yields bindings}

\bigskip
\pause

{\blue Restriction}

\medskip

\begin{tabular}{l}
\verb?let (x,x) = (1,1);;?\\
\ett{...}\\
\ett{ ... ERROR ... 'x' is bound twice in this pattern}
\end{tabular}

\bigskip
\pause

Restriction can be circumvented using {\redbrown \verb-when-} clauses, for example:

\begin{alltt}\blue
let f = function
        | (x,y){\redbrown when} x=y -> x
        | (x,y)          -> x+y
\end{alltt}
\end{frame}


\begin{frame}[fragile]
\frametitle{Polymorphic types: equality and comparison constraints (I)}

Polymorphic types may be accompanied with equality and comparison constraints like:
\begin{itemize}
\item  {\redbrown when 'a : comparison}
\item  {\redbrown when 'b : equality}	
\end{itemize}	 

\medskip

For example, there is a built-in function:
\[\blue
\verb/compare/\ x\ y\ \ =\ \ \left\{ \begin{array}{rl}
> 0 & \mbox{if $x > y$} \\
0 & \mbox{if $x = y$} \\
< 0  & \mbox{if $x < y$}
\end{array}
\right.
\]
with the type: 
\begin{alltt}\redbrown 
	   'a -> 'a -> int  when 'a : comparison
\end{alltt}
	
\pause

For example:
\begin{alltt}\blue
compare (2, [1; 2; 3]) (2, [1;4]);;
\ett{val it : int = -1}
\end{alltt}

\end{frame}



\begin{frame}[fragile]
\frametitle{Polymorphic types: equality and comparison constraints (II)}

The built-in function {\blue List.contains} can be declared as follows:
\begin{alltt}\blue
let rec contains x = 
   function 
   | []    -> false
   | y::ys ->{\redbrown x=y} || contains x ys
\ett{contains: 'a -> 'a list -> bool when{\redbrown 'a : equality}}

contains [3;4] [[1..2]; [3..5]];;
\ett{val it : bool = false}
\end{alltt}

\pause 
\bigskip
Notice:
\begin{itemize}
\item The equality constraint in the type

\item Lazy (short-circuit) evaluation of $\blue e_1 || e_2$ causes termination as soon as an element $\blue y$ equal to $\blue x$ is found 

\item Yet a recursion following the structure of lists
\end{itemize}

\end{frame}

\begin{frame}
\begin{center}\Large\redbrown
On let-expressions and lists
\end{center}	
\end{frame}


\begin{frame}[fragile]\frametitle{Let-expressions}

A let-expression $\blue e_l$ has the (verbose) form 
\begin{alltt}\blue
let x = e1 in e2 
\end{alltt}
\pause
or the following short form exploiting indentation:
\begin{alltt}\blue
	let x = e1 
	e2
\end{alltt}

The expression provides a {\redbrown local} definition for {\blue x} in {\blue e2}. 

\pause 
\bigskip

A let-expression $\blue e_l$ is evaluated in an environment $\darkgreen env$ as follows:  

\bigskip
\pause

If
\begin{enumerate}
\item $\blue v_1$ is the value obtained by evaluating $\blue e_1$ in $\darkgreen env$,

\item<5-> $\darkgreen env'$ is obtained by adding binding $\darkgreen x \mapsto v_1$ to $\darkgreen env$ and
    
\item<6-> $\blue v_2$ is the value obtained by evaluating $\blue e_2$ in $\darkgreen env'$
\end{enumerate}
\pause[7]
then 
\[\blue (\mathtt{let}\ x = e_1\ \mathtt{in}\ e_2 , {\darkgreen env}) \leadsto (v_2, {\darkgreen env}) \]

\end{frame}



\begin{frame}[fragile]
\frametitle{Let-expression -- an example}

\begin{alltt}\blue
let g y = let a = 6
          let b = y + a
          y + b;;
\ett{val g : int -> int}
	
g 1;;
\ett{val it : int = 8}
\end{alltt}
Note: {\blue a} and {\blue b} are not visible outside of {\blue g}

\bigskip
\pause
Evaluation ?

\end{frame}

\begin{frame}[fragile]\frametitle{Pattern matching on results of recursive calls}
\vspace*{-5mm}

{\blue \begin{tabular}{lcl}
		\multicolumn{3}{l}{
			{\tt sumProd}\ {\tt [}$x_0${\tt ;}$x_1${\tt ;} $\ldots${\tt ;}$x_{n-1}${\tt ]}
		} \\
		& = &
		{\tt (} $x_0$ {\tt +} $x_1$ {\tt +} $\ldots$ {\tt +} $x_{n-1}$ {\tt ,}
		$x_0$ {\tt *} $x_1$ {\tt *} $\ldots$ {\tt *} $x_{n-1}$ {\tt )} \\
		{\tt sumProd []} &=& {\tt (0,1)}
\end{tabular}}

\medskip\noindent\pause
The declaration is based on the recursion formula:
\[\blue
\texttt{sumProd}\ \texttt{[}x_0\texttt{;}x_1\texttt{;}
\ldots\texttt{;}x_{n-1}\texttt{]} =
\texttt{(}x_0\ \texttt{+}\ \texttt{rSum} \texttt{,} x_0\ \texttt{*}\ \texttt{rProd} \texttt{)}
\]
where
$\blue
\texttt{(rSum,rProd)} =
\texttt{sumProd}\ \texttt{[}x_1\texttt{;}
\ldots\texttt{;}x_{n-1}\texttt{]}$

\bigskip\pause

This gives the declaration:
\begin{alltt}\blue
let rec sumProd = 
   function
   | []      -> (0,1)
   | x::rest ->{\redbrown let (rSum,rProd) = sumProd rest
                (x+rSum,x*rProd)};;
\ett{val sumProd : int list -> int * int}
	
sumProd [2;5];;
\ett{val it : int * int = (7, 10)}
\end{alltt}
\end{frame}


\begin{frame}[fragile]\frametitle{A blackboard exercise}

A function from the $\blue\verb|List|$ library:

\begin{itemize}


\item $\blue  \texttt{List.unzip([(}x_0,y_0\texttt{);(}x_1,y_1\texttt{);}\ldots\texttt{;(}x_{n-1},y_{n-1}\texttt{)]}$ \\
$\blue \qquad = \texttt{([}x_0\texttt{;}x_1\texttt{;}\ldots\texttt{;}x_{n-1}\texttt{],[}
y_0\texttt{;}y_1\texttt{;}\ldots\texttt{;}y_{n-1}\texttt{])}$
\end{itemize}


\end{frame}

\begin{frame}{Function expressions and match expressions}

Consider
\[\blue
\mbox{Let $\redbrown e_m$ be} \quad 
\left\{\begin{array}{l}
\mathtt{match}\ {\darkgreen e}\ \mathtt{with} \\
\begin{array}{rcl}
|\ \mathit{pat_1} & \to & e_1\\
\ & \vdots & \\
|\ \mathit{pat_n} & \to & e_n
\end{array}
\end{array}\right.
\]

and

\[\blue
\mbox{Let $\redbrown e_f$ be} \quad 
\left\{
\begin{array}{l}
\mathtt{function}\\
\begin{array}{rcl}
|\ \mathit{pat_1} & \to & e_1\\
\ & \vdots & \\
|\ \mathit{pat_n} & \to & e_n
\end{array}
\end{array}\right.
\]

\medskip
\pause

\begin{itemize}
\item Can you express $\redbrown e_f$ using $\redbrown e_m$ and ... ? 

\item Can you express $\redbrown e_m$ using $\redbrown e_f$ and ... ? 
\end{itemize} 


\end{frame}

\begin{frame}[fragile]{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 {\redbrown (p_1, \ldots, p_n)} \quad p_1\!::\!p_2 \quad [p_1; \ldots; p_n]$\\ 
	$\blue p_1 | p_2 \quad p\ \mathtt{when}\ e \quad p\ \mathtt{as}\ x \quad {\redbrown p\!:\!t}  \ldots$   
	
	\medskip
	
	\item<3-> Expressions: $\blue x \quad {\redbrown (e_1,\ldots,e_n)} \quad e_1\!::\!e_2 \quad [p_1; \ldots; p_n] $\\[2mm]
	$\blue e_1 e_2 \quad  e_1\! \oplus\! e_2 \quad {\redbrown (\oplus)} \quad {\redbrown \mathtt{let}\ p_1 = e_1\ \mathtt{in}\ e_2}$ \\[2mm]
	$\blue {\redbrown e\!:\!t} \quad  \mathtt{if}\ e\ \mathtt{then}\ e_1\  \mathtt{then}\ e_2 \qquad \mathtt{match}\ e\ \mathtt{with}\ clauses$\\[2mm] 
	$\blue {\redbrown \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}{Summary}
\begin{itemize}
	
	\item Functional decomposition
	
	\item Functions as "first-class citizens"
	
	\item Anonymous functions
	
	\item Types, type inference and overloading
	
	\item Tuples and equality and comparison constraints 
	
	\item Let expressions and lists 
	
	
\end{itemize}



\end{frame}

\end{document}


