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

\input{../Common/common}



\title % (optional, use only with long paper titles)
{02157 Functional Programming}
\subtitle
{Lecture 7: Module System -- briefly} % (optional)

\date {MRH 25/10/2024}% (optional)

\begin{document}

\begin{frame}
  \titlepage


\end{frame}



\begin{frame}{Overview}

\begin{itemize}

\item On critical looks at programs
\begin{itemize}
\item simplification for readability reasons
\item simplifications for computational reasons
\end{itemize}


\bigskip



\item The Module System 


\bigskip

\item F\# is integrated on .Net \hfill briefly
\begin{itemize}
\item free, open source
\item cross platform for Linux, MacOS, Windows, ...
%\end{itemize}

%\bigskip

\item A three project solution for polynomials containing 
\begin{itemize}
\item An F\# library (class library)
\item An F\# console application
\item A C\# console application
\end{itemize}
\ \hfill {\redbrown on Learn}
\end{itemize}

\bigskip
\item A brief look at type inference

\end{itemize}
\end{frame}




\begin{frame} 

\begin{center}
\Large\darkgreen On critical looks at programs
\end{center}


\pause 

\begin{itemize}
	
\item<2-> Aim at succinct programs\\ \pause[3]
have a critical look at your own programs


\item<4-> Correctness has top priority\\ \pause[5]
but have an eye to sensible use of resources
\end{itemize}

\end{frame}


\begin{frame}[fragile]{Can we simplify?}

Have a look at:
\begin{alltt}\blue
let f(x) = match (x) with 
           |(a,z) -> if (not(a) = true) then true 
                     else if (fst(z) = true) then snd(z) 
                          else false;; 	
\end{alltt}

\pause
\bigskip

\begin{itemize}
	\item What is the type of $\blue f$?
	\item What is $\blue f$ computing?
\end{itemize}

\pause
\bigskip


Can we improve readability?

%\end{verbatim}	
\end{frame} 
%\end{document}



\begin{frame}[fragile]{Is a use of library functions adequate?}


Have a look at 
\begin{alltt}\blue 
let h a xs = let xs1 = List.filter (fun (a',t) -> a=a') xs
             let xs2 = List.map (fun (a,t:int) -> t) xs1
             List.sum xs2 	
\end{alltt}

\pause
\bigskip

\begin{itemize}
\item Can this problem easily be solved in a less resource demanding manner?  
\end{itemize}


\end{frame}
%



\begin{frame}[fragile]{Resource sensible versions}

Have a look at:
\begin{alltt}\blue
let rec h1 a = 
   function 
   | []                     -> 0
   | (a',t)::rest when a=a' -> t + h1 a rest
   | _::rest                -> h1 a rest;;

let rec h2 a xs = 
  List.fold (fun s (a',t) -> if a=a' then s+t else s) 0 xs;;
\end{alltt}

\pause

Solutions are based on a simple algorithmic idea
\begin{itemize}
\item traverse the list $\blue xs$ one time and
\item build up the result during the traversal 
\end{itemize}


\pause
\bigskip

Correctness has top priority\\ \pause
\qquad -- but have an eye to sensible use of resources

\pause
\bigskip
More when the topic: Tail recursion, is covered


\end{frame}






\begin{frame} 

\Large\darkgreen The module system

\end{frame}




\begin{frame}{Overview}

\begin{itemize}
	
	\item<1-> Supports modular program design including
	
	\begin{itemize}
		\item encapsulation
		
		\item abstraction and
		
		\item reuse of software components.
		
	\end{itemize}
	
	
	\item<2-> A module is characterized by:
	
	\begin{itemize}
		\item a {\em\redbrown signature} -- an interface specifications and
		
		\item a matching {\em\redbrown implementation} -- containing declarations of the interface specifications.
		
	\end{itemize}
	
	
	\item<3-> Example-based presentation to give the flavor \\
	\qquad incomplete -- no object interface types, for example
\end{itemize}

\medskip
\pause[4]

Sources:
\begin{itemize} \item Chapter 7: Modules. (A fast reading suffices.)
	
\end{itemize}
\end{frame}



\begin{frame}[fragile]
\frametitle{\redbrown On hiding: Polynomial program}

\vspace*{-3mm}

An violation of a representation invariant \hfill  {\redbrown without hiding}

\begin{alltt}\blue
// A misuse: [0] is not legal polynomial	
let p1 = mulX [0];;  
// val p1 : int list = [0; 0]

// Pretty print
toString p1;;
// val it : string = "0"
\pause
let p2 = mulX [];;                  // [] is legal
// val p2 : int list = []

// Pretty print
toString p2;;
// val it : string = "0"
\pause\redbrown
// But
p1 = p2;;
// val it : bool = false	
\end{alltt}
\begin{itemize}
\item<3-> {\redbrown\Large may cause unpredictable results}
\end{itemize}

\end{frame}


\begin{frame}[fragile]
\frametitle{\redbrown Protection of a representation invariant}

\begin{alltt}\blue
#r @"Polynomial.dll"

open Polynomial

let p1 = mulX (ofList [0]);;  
// val p1 : Poly = 0         pretty print

let p2 = mulX (ofList []);;
// val p2 : Poly = 0         pretty print

p1 = p2;;
// val it : bool = true	
	\end{alltt}
\begin{itemize}
\item<2-> internal representation is hidden
\item<3-> {\blue ofList} gives legal representations
\item<4-> functions preserve the invariant: isLegal 
\end{itemize}

\pause[5]

\begin{center}
\redbrown\Large Unpredictable results are prevented
\end{center}

\end{frame}




\begin{frame}{Module}

A {\redbrown module} is a combination of a
\begin{itemize}
\item<1-> {\redbrown signature}, which is a specification of an
interface to the module (the user's view), and an

\item<2-> {\redbrown
implementation}, which provides declarations for the specifications in the signature.

\end{itemize}

\end{frame}

\begin{frame}[fragile]
\frametitle{Geometric vectors: Signature}

The signature specifies one type and eight values:

{\small
\begin{alltt}\blue
// Vector signature
module Vector
type vector
val ( ~-. ) : vector -> vector             // Vector sign change
val ( +. )  : vector -> vector -> vector   // Vector sum
val ( -. )  : vector -> vector -> vector   // Vector difference
val ( *. )  : float  -> vector -> vector   // Product with number
val ( &. )  : vector -> vector -> float    // Dot product
val norm    : vector -> float              // Length of vector
val make    : float * float -> vector      // Make vector
val coord   : vector -> float * float      // Get coordinates
\end{alltt}
}
\bigskip
\pause

\begin{center}\redbrown The specification 'vector' does not reveal the
implementation \end{center}

\medskip
\pause
\begin{itemize}
\item Why is {\blue make} and {\blue coord} introduced?
\end{itemize}


\end{frame}

\begin{frame}[fragile]
\frametitle{Geometric vectors (2): Simple implementation}

An implementation must declare each specification of the signature:

\begin{alltt}\blue
// Vector implementation
module Vector
type vector ={\redbrown V of} float * float
let (~-.) (V(x,y))             = V(-x,-y)
let (+.) (V(x1,y1)) (V(x2,y2)) = V(x1+x2,y1+y2)
let (-.)  v1         v2        = v1 +. -. v2
let ( *.) a         (V(x1,y1)) = V(a*x1,a*y1)
let (&.) (V(x1,y1)) (V(x2,y2)) = x1*x2 + y1*y2
let norm  (V(x1,y1))           = sqrt(x1*x1+y1*y1)
let make  (x,y)                = V(x,y)
let coord (V(x,y))             = (x,y)
\end{alltt}


\bigskip
\pause

\begin{itemize}
\item Since the representation of 'vector' is {\redbrown hidden in the signature}, the type must be {\redbrown implemented by either a tagged value or a record}.
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Geometric vectors (3): Compilation}

Suppose
\begin{itemize}
\item the signature is in a file {\blue 'Vector.fsi'}
\item the implementation is in a file {\blue 'Vector.fs'}
\end{itemize}

\bigskip


A library file {\blue 'Vector.dll'} is constructed by the following command:
{\blue\begin{verbatim}
D:\MRH data\ ... \Libraries\fsc -a Vector.fsi Vector.fs
\end{verbatim}
}

\bigskip

The library {\blue 'Vector'} can now be used just like other libraries, such as {\blue 'Set'} or {\blue 'Map'}.

\bigskip

\bigskip

\pause
\begin{itemize}
\item Compiler on Linux and Mac systems: {\blue fsharpc} 
\end{itemize}


\bigskip
\pause
An alternative is to use the {\blue Command Line Interface (CLI)} tool\\
\ \hfill {\redbrown mentioned later in this lecture}



\end{frame}


\begin{frame}[fragile]
\frametitle{Geometric vectors (4): Use of library}

A library must be referenced before it can be used.

{\small
\begin{alltt}\blue
{\redbrown #r @"d:{\ttbsl}MRH data{\ttbsl} ... {\ttbsl}Libraries{\ttbsl}Vector.dll";;}
\ett{--> Referenced 'd:{\ttbsl}MRH data{\ttbsl} ... {\ttbsl}Libraries{\ttbsl}Vector.dll'}
open Vector ;;

let a = make(1.0,-2.0);;
\ett{val a : vector}
let b = make(3.0,4.0);;
\ett{val b : vector}
let c = 2.0 *. a -. b;;
\ett{val c : vector}

coord c ;;
\ett{val it : float * float = (-1.0, -8.0)}

let d = c &. a;;
\ett{val d : float = 15.0}

let e = norm b;;
\ett{val e : float = 5.0}
\end{alltt}
}

\medskip

Notice: the implementation of \texttt{\blue vector} is not visible and it
cannot be exploited.

\end{frame}


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

A {\em\blue type augmentation}
\begin{itemize}

\item adds declarations to the definition of a tagged type or a record type
\item allows declaration of (overloaded) operators.
\end{itemize}

\bigskip
\pause

In the 'Vector' module we would like to
\begin{itemize}

\item overload  \verb/+/, \verb/-/ \ and \ \verb/*/ to also denote {\blue vector} operations.

\item overload \verb/*/ \  to denote {\blue two} different
operations on vectors.


\end{itemize}
\end{frame}


\begin{frame}[fragile]
\frametitle{Type augmentation -- signature}

{\blue
\begin{verbatim}
module Vector

[<Sealed>]
type vector =
  static member ( ~- ) : vector -> vector
  static member ( + )  : vector * vector -> vector
  static member ( - )  : vector * vector -> vector
  static member ( * )  : float  * vector -> vector
  static member ( * )  : vector * vector -> float
val make : float * float -> vector
val coord: vector -> float * float
val norm : vector -> float
\end{verbatim}
}
\pause
\bigskip

\begin{itemize}

\item<2->
The {\em attribute} \verb/[<Sealed>]/ is mandatory when
a type augmentation is used. %It protects the library against unintentional use in the %OO-world.


\item<3->
The ``\verb/member/'' specification and declaration of an infix operator (e.g. \verb/+/) correspond
to a type of form \ {\it type}$_1$\;\verb/*/\;{\it type$_2$}\;\verb/->/\;{\it type}$_3$ %while the earlier
%\verb/val/ specification and \verb/let/ declaration (of e.g. \verb/(+.)/) use a %higher-order  type of form \
%{\it type}$_1$\;\verb/->/\;{\it type$_2$}\;\verb/->/\;{\it type}$_3$. The indicated
%type is required to get the overloading.
%The resulting prefix function (e.g. \verb/(+)/) will, nevertheless, get the usual %higher-order type.

\item<4-> The operators can still be used on numbers.

\end{itemize}

\end{frame}

\begin{frame}[fragile]
\frametitle{Type augmentation -- implementation and use}

{\small\blue
\begin{alltt}
module Vector

type vector =
  | V of float * float
  static member (~-) (V(x,y))           = V(-x,-y)
  static member (+) (V(x1,y1),V(x2,y2)) = V(x1+x2,y1+y2)
  static member (-) (V(x1,y1),V(x2,y2)) = V(x1-x2,y1-y2)
  static member (*) (a, V(x,y))         = V(a*x,a*y)
  static member (*) (V(x1,y1),V(x2,y2)) = x1*x2 + y1*y2
let make (x,y)     = V(x,y)
let coord (V(x,y)) = (x,y)
let norm (V(x,y))  = sqrt(x*x + y*y)
\end{alltt}
}

\medskip
\pause

The operators \verb/+/, \verb/-/, \verb/*/ are available on vectors even without opening:

\begin{alltt}\blue
let a = Vector.make(1.0,-2.0);;
\ett{val a : Vector.vector}

let b = Vector.make(3.0,4.0);;
\ett{val b : Vector.vector}

let c = 2.0 * a - b;;
\ett{val c : Vector.vector}

Vector.coord c ;;
\ett{val it : float * float = (-1.0, -8.0)}
\end{alltt}

\end{frame}

\begin{frame}[fragile]
\frametitle{Customizing the string function}

{\small
\begin{alltt}\blue
module Vector
type vector =
   | V of float * float
  {\redbrown override v.ToString() =
           match v with | V(x,y) -> string(x,y) }

let make (x,y)     = V(x,y)
   ...
type vector with
  static member (~-) (V(x,y))           = V(-x,-y)
  ...
\end{alltt}
}

\begin{itemize}

\item The default ToString function that does not reveal a meaningful value is overridden to give a string for the pair of coordinates.

\item A type extension is used.
\end{itemize}

\pause
\bigskip

Example:
\begin{alltt}
let a = Vector.make(1.0,2.0);;
\ett{val a : Vector.vector = (1, 2)}

string(a+a);;
\ett{val it : string = "(2, 4)"}
\end{alltt}
\end{frame}


\begin{frame}{Summary}

Modular program development

\begin{itemize}
	
	\item program libraries using signatures and structures
	
	\item type augmentation, overloaded operators, customizing string (and other) functions
	
	\item Encapsulation, abstraction, reuse of components, division of concerns, ...
	
	\item ...
	
\end{itemize}

\end{frame}


\begin{frame}

\begin{center}\LARGE\darkgreen 
	A three project solution for polynomials containing 
\end{center}
\ \hfill {\redbrown on Learn}

\end{frame}



\begin{frame}\frametitle{Nano-solution to Polynomial exercise on Learn}

A {\darkgreen three-project solution} to a minimal part of the polynomial exercise:

\begin{itemize}
	\item {\darkgreen PolyLib}: an F\# library for polynomials \hfill a class library	
	\item {\darkgreen CSharpApp} a C\# console application using the library
	\item {\darkgreen FSharpApp} an F\# console application using the library
\end{itemize}

\pause \bigskip


The solution is formed using the {\blue Command Line Interface (CLI)} tool
\begin{itemize}
\item \url{https://docs.microsoft.com/en-us/dotnet/fsharp/get-started/get-started-command-line}

\item \url{https://docs.microsoft.com/en-us/dotnet/core/tools}

\end{itemize}
\ \hfill {\redbrown works for Linux, MacOS, Windows operating systems}


\pause \bigskip

Consult DTU Learn concerning:
\begin{itemize}
	\item How the solution is formed using the CLI tools
	\item How to run the applications and the script
	\item How executables and libraries (assemblies / binaries) are build 
\end{itemize}

\end{frame}


\begin{frame}[fragile]\frametitle{Overview of Solution}

Solution with three projects

\begin{itemize}

\item<1-> PolyLib \hfill {\redbrown F\# class library}
\begin{itemize}
\item PolyLib.fsproj \qquad includes compilation information
\item Polynomial.fsi \qquad signature (interface) file
\item Polynomial.fs   \qquad implementation file
\item script.fsx \qquad \qquad reference to PolyLib.dll
\end{itemize}
	
\bigskip

\bigskip
	
\item<2-> FSharpApp \hfill {\redbrown F\# console application}
\begin{itemize}
\item FSharpApp.fsproj \quad includes reference to PolyLib
\item Program.fs   \qquad \qquad a free-standing F\# program
\end{itemize}	

\bigskip

\bigskip	

\item<3-> CSharpApp \hfill {\redbrown C\# console application}
\begin{itemize}
	\item CSharpApp.csproj \quad  includes reference to PolyLib
	\item Program.cs   \qquad \qquad a free-standing C\# program\\
\ \qquad \qquad \qquad \qquad \quad 	Using the F\# type $\blue\verb|'a list|$
	
\end{itemize}
	
\end{itemize}	


\bigskip
\pause[4]
Let us have a look at the solution

\end{frame}



\begin{frame}
	\begin{center}
		\LARGE\darkgreen On Type Inference
	\end{center}
\end{frame}

\begin{frame}{Type inference}
	
	Automated generation of the (most general) type for a program that do not contain type annotations.	
	
	\begin{itemize}
		
		\medskip
		\item<2-> Avoid cluttering beautiful programs with type annotations while
		
		\medskip
		\item<3-> Preserving static type safety
	\end{itemize}
\end{frame}


\begin{frame}[fragile]
	\frametitle{Type inference: Examples}
	
	For the two programs:
\begin{alltt}\blue
   let f x y = 2 * x + y;;
		
   let rec append xs ys = match xs with 
                          | []      -> ys
                          | x::rest -> x::append rest ys;; 
\end{alltt} 
	the F\# compiler infers the types:
\begin{alltt}\blue
   f: int -> int -> int	
   append: 'a list -> 'a list -> 'a list 
\end{alltt}
	
	\bigskip 
	\pause
	
	The F\# type inference includes
	\begin{itemize}
		
		\item {\darkgreen Overloading} \\  
		Functions with different types and implementations can share name, e.g.\ $\blue\verb|+|$
		
		\bigskip
		
		\item<3-> {\darkgreen Parametric polymorphism}\\
		A single implementation of a function works for type-consistent input data, , e.g.\ $\blue\verb|append|$
	\end{itemize}
	
\end{frame}



\begin{frame}[fragile]\frametitle{Type inference: Background}	
	\begin{itemize}
		\item Hindley type-schema for Combinatory Logic 1969 
		\item Milner ML-style type inference with algorithm W 1978 
		\item Damas-Milner 1982: correctness of type inference algorithm W    
		\item ... SML ... OCAML ... Haskell ... F\# ...
	\end{itemize}
	
	\bigskip
	\pause
	
	Type inference in  SML, ...F\#, ... allows {\darkgreen let-polymorphism}; where, for example,
\begin{alltt}\blue
let rec map f xs = match xs with 
                   | []    -> [] 
                   | x::xs -> f x :: map f xs 		 
\end{alltt}
	is typable $\blue \verb|map|: \forall \alpha, \beta. (\alpha \to \beta) \to \alpha\ \verb|list| \to \beta\ \verb|list|$ 
	
	\bigskip\pause
	The following program is {\redbrown NOT typable}:
\begin{alltt}\blue
   let f g = (g 1, g true) in f id
\end{alltt}
	as it would require two different instantiations of argument $\redbrown \verb|g|$'s type\\
	\ \hfill {\redbrown such extra power makes type inference problem undecidable}
	
\end{frame}

\begin{frame}[fragile]
	\frametitle{About type rules and inference algorithm}
	\onslide<1>{	
		The type-inference problem is specified using a few rules like:
		\[\blue
		\frac{\rho[x\mapsto t_x, f \mapsto t_x \to t_r] \vdash e_r: t_r \quad \rho[f\mapsto \forall \alpha_1, \ldots, \alpha_n.t_x \to t_r] \vdash e_b : t }{\rho \vdash \mathrm{let}\ f\ x\ =\ e_r\ \mathrm{in}\ e_b\ \mathrm{end} : t} 
		\begin{array}{l}
			\mbox{rule 8 out of 9}\\
			(\mbox{Sestoft2012})
		\end{array}
		\]
		where \mbox{$\blue \alpha_1, \ldots, \alpha_n$ are not free in $\blue \rho$}.  \hfill {\darkgreen don't worry}
	}	
	%that can be used to derive types for expressions. 
	\pause
	\bigskip
	
	The identity function: $\blue \verb|let id x = x|$ has infinity many types
\begin{alltt}\blue
'a->'a   int list->int list   int list list->int list list 	
\end{alltt}
	including a {\blue most general (or principal)} type $\blue\verb|'a -> 'a|$\\ \pause
	\ \hfill {\redbrown having all other types of $\blue\verb|id|$ as instances}
	
	\bigskip
	\pause
	
	The step from a rule-based formulation to an algorithm is huge.
	\begin{itemize}
		\item rules and algorithm by Milner in 1978
		\item correctness proof of algorithm by Damas-Milner in 1982
		\item ML typability is complete for DEXPTIME by Mairson and KfouryTiurynUrzyczyn in 1990  
	\end{itemize}
	\pause
	Nice presentations in
	\begin{itemize}
		\item Sestoft: Programming language concepts, Springer 2012 (Ch 6) 
		\item Schwartzbach: Polymorphic type inference, BRICS LS 95-3  
	\end{itemize}
	
	
\end{frame}

\begin{frame}[fragile]
	\frametitle{A program with a complex type: Sestoft 2012}
\begin{alltt}\blue
   let pair x y p = p x y;; 
	
   let p1 p = pair id id p;; 
   let p2 p = pair p1 p1 p;; 
   let p3 p = pair p2 p2 p;; 
   let p4 p = pair p3 p3 p;; 
   let p5 p = pair p4 p4 p;;
\end{alltt}
	
	\pause
	\bigskip
	
	\begin{itemize}
		\item $\blue\verb|p1|$'s type contains 3 type variables  
		\item $\blue\verb|p2|$'s type contains 7 type variables
		\item $\blue\verb|p3|$'s type contains 15 type variables
		\item ...    	
	\end{itemize}
	
	\pause
	\bigskip
	
	Observe 
	\begin{itemize}
		\item a doubling of the number of type variables from $\blue\verb|p|_i$ to $\blue\verb|p|_{i+1}$
		\item the number of type variable is exponential in the program size
		%\end{itemize}
		
		
		%\begin{itemize}
		\item programmers rarely make programs having such complex types
		
		\item type checking appears to be efficient in practice
		
	\end{itemize}
	
	
\end{frame}

\begin{frame}[fragile]
	\frametitle{An informal approach to type inference}
	
	Given a declaration 
\begin{alltt}\blue
   let rec f x y ... = e	
\end{alltt}
	and knowing typing and rules for ``bits and pieces''. 
	
	\bigskip
	
	\onslide<2->{
		\begin{itemize}
			\item Choose two fresh type variables for the unknown types of the arguments $\blue x, y, \ldots$
			
			\item Analyse $\blue e$ adding new fresh type variables and constrains as needed when typing the parts of $e$ 
		\end{itemize}
	}
	
	\bigskip
	
	\onslide<3->{
		Two possibilities:
		\begin{itemize}
			\item An inconsistency is detected and the program cannot be typed.
			
			\item A most general type can be establish as constraints on the introduced type variables arise from the program only.
		\end{itemize}
	}
	
	%	\bigskip
	%	\onslide<1->{
		%		\[\blue
		%		\frac{\rho[x\mapsto t_x, f \mapsto t_x \to t_r] \vdash e_r: t_r \quad \rho[f\mapsto \forall \alpha_1, \ldots, \alpha_n.t_x \to t_r] \vdash e_b : t }{\rho \vdash \mathrm{let}\ f\ x\ =\ e_r\ \mathrm{in}\ e_b\ \mathrm{end} : t} 
		%		\]
		%		where \mbox{$\blue \alpha_1, \ldots, \alpha_n$ are not free in $\blue \rho$}. }
	%	
	
	
\end{frame}

\begin{frame}[fragile]
	\frametitle{An example of an informal type inference}
	
\begin{alltt}\blue
let rec map f xs = match xs with 
                   | []      -> []                 (1) 
                   | x::tail -> f x :: map f tail  (2)	 
\end{alltt}
	
	\begin{itemize}
		\item<1-> Let $\blue\verb|'a|$ and  $\blue\verb|'b|$ be fresh type variables so that  $\blue\verb|f:'a|$ and  $\blue\verb|xs:'b|$. 
		\item<2-> Since  $\blue\verb|xs|$ is matched with pattern  $\blue\verb|[]|$ in (1), xs must have type  $\blue\verb|'c list|$ ( $\blue\verb|'c|$ fresh) and  $\blue\verb|'b = 'c list|$
		\item<3-> The value of the function must have type  $\blue\verb|'d list|$ ( $\blue\verb|'d|$ fresh) due to the expression  $\blue\verb|[]|$ in (1)
		\item<4-> Since  $\blue\verb|xs:'c list|$ is matched with pattern  $\blue\verb|x::tail|$ in (2), we have  $\blue\verb|x:'c|$ and  $\blue\verb|tail:'c list|$ due to the type of cons  $\blue\verb|::|$.
		\item<5-> Since the value of the function has type  $\blue\verb|'d list|$, we have that  $\blue\verb|f x::map f tail:'d list|$ and hence  $\blue\verb|f x:'d|$,  $\blue\verb|map f tail:'d list|$ and  $\blue\verb|f:'c->'d|$ because  $\blue\verb|x:'c|$. Therefore,  $\blue\verb|'a = 'c->'d|$. 
	\end{itemize}
	\pause[6]
	There are no further constraints and the most general type of $\blue \verb|map|$ is 
	\begin{alltt}\blue
		('c -> 'd) -> 'c list -> 'd list
	\end{alltt}
	Due to implicit universal quantification, the type can be renamed to 
	\begin{alltt}\blue
		('a -> 'b) -> 'a list -> 'b list
	\end{alltt}
	
\end{frame}


\begin{frame}[fragile]\frametitle{An even more informal approach}
	
	Explain in your own words .....  
	
	\pause
	\bigskip
	Explanation must
	\begin{itemize}
		
		\item justify that every sub-expression is well-typed and
		
		\item that the establish type is the most general one.
		
	\end{itemize}
	
	\pause\bigskip
	
	An explanation concerning the type of $\blue\verb+map+$ should address:
	\begin{itemize}
		\item the arguments $\blue\verb|f|$ and $\blue\verb|xs|$,
		\item the patterns $\blue\verb|[]|$ and $\blue\verb|x::tail|$,
		\item the expressions $\blue\verb|[]|$ and $\blue\verb|f x :: map f tail|$,
		\item the sub-expressions $\blue\verb|f x|$ and $\blue\verb|map f tail|$, and
		\item the type of cons $\blue\verb|::|$.
	\end{itemize}
	
	
\end{frame}





\end{document}
