\documentclass[a4,slidesonly]{seminar}%CAML

\special{landscape}

\setlength\slidewidth{10in}
\setlength\slideheight{6.5in}
\renewcommand\sliderightmargin{0in}
\renewcommand\slideleftmargin{1in}
\renewcommand\slidetopmargin{0.8in}
\renewcommand\slidebottommargin{0in}
\centerslidesfalse
\slideframe{none}

\usepackage{graphicx}
\usepackage{pst-all}
\usepackage{advi}
\usepackage{advi-annot}
\usepackage{advi-graphicx}
\usepackage{superpose}

\usepackage{caml}

\definecolor{red}{rgb}{1.0,0.0,0.0}
\definecolor{green}{rgb}{0.0,1.0,0.0}
\definecolor{blue}{rgb}{0.0,0.0,1.0}
\definecolor{darkgreen}{rgb}{0.0,0.4,0.0}
\definecolor{yellow}{rgb}{1.0,1.0,0.0}
\definecolor{cyan}{rgb}{0.0,1.0,1.0}
\definecolor{magenta}{rgb}{1.0,0.0,1.0}
\definecolor{lightred}{rgb}{1.0,0.5,0.5}
\definecolor{lightgreen}{rgb}{0.5,1.0,0.5}
\definecolor{lightblue}{rgb}{0.6784,0.8471,0.9020}
\definecolor{lightlightblue}{rgb}{0.51,0.52,0.931}

\def\darkgreen{\color{darkgreen}}

\def\konstr#1{\Kappa\sb{\caml{#1}}}

\newcommand{\heading}[1]{%
  \centerslidesfalse%
  {\noindent\large{#1}}\\
  \mbox{\hspace{-0.02\textwidth}%
    \includegraphics[width=1.05\textwidth]{bar.jpg.eps}}}

\makeatletter
\gdef\ps@myslide{\def\@oddfoot{\hfil\large$\Rightarrow$}\let\@evenfoot\@oddfoot}
\makeatother
\pagestyle{myslide}

\begin{document}

\begin{slide}
  \begin{center}
    ~\vfill

    ~\vfill

    {\large Extensional polymorphism}\\
    -- theory and applications --

    ~\vfill

    {Jun FURUSE}\\
    {\small INRIA Rocquencourt\\
      Projet Cristal}

    ~\vfill
  \end{center}
\end{slide}

\begin{slide}
\heading{Extensional polymorphism}
Ad-hoc parametric (non parametric) 
polymorphism extension framework\\ over ML.

\adviwait
\begin{itemize}
\item Polymorphic primitives with type dependent semantics 
  \begin{itemize}
  \item Polymorphic overloaded arithmetic operators 
%caml (+){\rm,} (-){\rm, \ldots}
\caml{(+){\rm,} (-){\rm, \ldots}} %-caml
  \item Primitives for dynamic values, persistent data storage, \ldots
  \item Meta-programming tools: \caml{print}, \caml{eval} 
  \end{itemize}
\adviwait
\item User definition of overloaded values
  \begin{itemize}
  \item Pattern match based definition and semantics
%CAML generic plus = case
%CAML | int -> int -> int => plus_int
%CAML | float -> float -> float => plus_float
%CAML ;;
\CAML\begin{alltt}
\CAML     generic plus = case
\CAML     | int{\ra}int{\ra}int \Ra plus_int
\CAML     | float{\ra}float{\ra}float \Ra plus_float
\CAML     ;;
\CAML\end{alltt}
  \end{itemize}
\end{itemize}
\end{slide}

\begin{slide}
\heading{Motivation: Overloading in ML (SML)}
SML has overloaded arithmetic operators
%caml (+){\rm,}(-){\rm, etc.}
\caml{(+){\rm,}(-){\rm, etc.}} %-caml
  \begin{itemize}
  \item Predefined (not user definable)
  \item Not really polymorphic. The definition:
%CAML let double x = x + x
\CAML\begin{alltt}
\CAML     let double x = x + x
\CAML\end{alltt}
    \begin{itemize}
    \item is rejected in SML'90
    \item has a type 
%caml int -> int 
\caml{int \ra int } %-caml
      in SML'97, using the default type of
%caml (+){\rm,}\\
\caml{(+){\rm,}\\} %-caml
%
%caml int -> int -> int{\rm.}
\caml{int \ra int \ra int{\rm.}} %-caml
    \end{itemize}
\end{itemize}
\end{slide}

\begin{slide}
\heading{Motivation: Overloading in Haskell}
Haskell type classes support:
\begin{itemize}
\item User definition of overloaded values
\item Extension by class instances 
\end{itemize}

\adviwait
Problems:
\begin{itemize}
\item Some typing restrictions
  \begin{itemize}
  \item Multi type class parameters
  \item Overlap instances
  \end{itemize}
   are not allowed, or restricted.
\adviwait
\item Open extension scheme does not match with ML semantics
  \begin{itemize}
  \item Type classes must be global
  \item Mutual recursive module dependency 
  \end{itemize}
\end{itemize}
\end{slide}

\begin{slide}
\heading{Motivation: Overloading in ML (O'Caml)}
O'Caml has \ldots none!
  \begin{itemize}
  \item Each arithmetic type has its own set of operators.
\adviwait
  \item We have
{\blue 10} arithmetic types!\\
%caml int{\rm,}
\caml{int{\rm,}} %-caml
%
%caml int32{\rm,}
\caml{int32{\rm,}} %-caml
%
%caml int64{\rm,}
\caml{int64{\rm,}} %-caml
%
%caml nativeint{\rm,}
\caml{nativeint{\rm,}} %-caml
%
%caml float{\rm,}
\caml{float{\rm,}} %-caml
%
%caml Complex.t{\rm,}\\
\caml{Complex.t{\rm,}\\} %-caml
%
%caml nat{\rm,}
\caml{nat{\rm,}} %-caml
%
%caml big\_int{\rm,}
\caml{big\_int{\rm,}} %-caml
%
%caml ratio{\rm,}
\caml{ratio{\rm,}} %-caml
%
%caml num
\caml{num} %-caml
%
\\We need overloading!!
  \end{itemize}

\end{slide}


\begin{slide}
\heading{Extensional polymorphism}
{\blue Generic values}, 
our ad-hoc polymorphic values support:
\begin{itemize}
\item Polymorphic primitives with type dependent semantics 
  \begin{itemize}
  \item Polymorphic overloaded arithmetic operators 
%caml (+){\rm,} (-){\rm, \ldots}
\caml{(+){\rm,} (-){\rm, \ldots}} %-caml
  \item Primitives for dynamic values, persistent data storage, \ldots
  \end{itemize}
\adviwait
\item User definition of overloaded values
  \begin{itemize}
  \item Pattern match based definition and semantics
  \item No typing restrictions of overloaded instances
  \item Recursions on types are easily defined
  \end{itemize}
\adviwait
\item Simple design
  \begin{itemize}
  \item Two-layer typing: new typing extension is modular
    both in theory and implementation.
  \end{itemize}
\end{itemize}
\end{slide}

\begin{slide}
\heading{Generic primitives}
Example: value printer as a generic primitive:
%CAML val print : \cforall$a.$a -> unit
\CAML\begin{alltt}
\CAML     val print : \cforall\cdelta{}.\cdelta{}{\ra}unit
\CAML\end{alltt}
%CAMLEND
\adviwait
Type dependent semantics as a primitive:
%CAML print : \(\blue\tau\) -> unit \(\leadsto\) \(gen(\)print,\(\blue\tau\))
\CAML\begin{alltt}
\CAML     print : \(\blue\tau\){\ra}unit \(\leadsto\) \(gen(\)print,\(\blue\tau\))
\CAML\end{alltt}
%CAMLEND

\adviwait
Compilation with type application and abstraction like system F:
%CAML print 1 \(\Ra\) {\darkgreen{print {\blue<<int>>} 1}}
%CAML
%CAML let print\_twice = \(\lambda\)x.print x; print x
%CAML      \(\Ra\) {\darkgreen{let print\_twice = \({\blue\Lambda\delta}.\lambda\)x.print {\blue$a} x; print {\blue$a} x}}
%CAML
%CAML print\_twice (1,3.14) \(\Ra\) {\darkgreen{print\_twice {\blue<<int * float>>} (1,3.14)}}
\CAML\begin{alltt}
\CAML     print 1 \(\Ra\) {\darkgreen{print {\blue\runtype{int}} 1}}
\CAML     
\CAML     let print\_twice = \(\lambda\)x.print x; print x
\CAML          \(\Ra\) {\darkgreen{let print\_twice = \({\blue\Lambda\delta}.\lambda\)x.print {\blue\cdelta{}} x; print {\blue\cdelta{}} x}}
\CAML     
\CAML     print\_twice (1,3.14) \(\Ra\) {\darkgreen{print\_twice {\blue\runtype{int\tsp{.5}*\tsp{.5}float}} (1,3.14)}}
\CAML\end{alltt}
%CAMLEND
\end{slide}

\begin{slide}
\heading{Generic primitives -- typing and compilation}
Ad-hoc polymorphism is quantified by {\blue dynamic type variables}
$\textcolor{blue}{\delta}, \textcolor{blue}{\delta'}, \ldots$
to be distinguished from regular parametric polymorphism:

%CAML let id = \(\lambda\)x.x
%CAML val id : \cforall'a.'a -> 'a       val print : \cforall{\blue{$a}}.{\blue{$a}} -> {\blue{$a}}
\CAML\begin{alltt}
\CAML     let id = \(\lambda\)x.x
\CAML     val id : \cforall\calpha{}.\calpha{}{\ra}\calpha{}       val print : \cforall{\blue{\cdelta{}}}.{\blue{\cdelta{}}}{\ra}{\blue{\cdelta{}}}
\CAML\end{alltt}
%CAMLEND

\adviwait
Type application and abstraction are attached
{\blue only} to ad-hoc polymorphism:
%CAML let id = \(\lambda\)x.x => {\darkgreen{let id = \(\lambda\)x.x}}
%CAML id (1,3.14) \(\Ra\) {\darkgreen{id (1,3.14)}}
%CAML
%CAML let print\_twice = \(\lambda\)x.print x; print x
%CAML      \(\Ra\) {\darkgreen{let print\_twice = \({\blue\Lambda\delta.}\lambda\)x.print {\blue{$a}} x; print {\blue{$a}} x}}
%CAML
%CAML print\_twice (1,3.14) \(\Ra\) {\darkgreen{print\_twice {\blue{<<int * float>>}} (1,3.14)}}
\CAML\begin{alltt}
\CAML     let id = \(\lambda\)x.x \Ra {\darkgreen{let id = \(\lambda\)x.x}}
\CAML     id (1,3.14) \(\Ra\) {\darkgreen{id (1,3.14)}}
\CAML     
\CAML     let print\_twice = \(\lambda\)x.print x; print x
\CAML          \(\Ra\) {\darkgreen{let print\_twice = \({\blue\Lambda\delta.}\lambda\)x.print {\blue{\cdelta{}}} x; print {\blue{\cdelta{}}} x}}
\CAML     
\CAML     print\_twice (1,3.14) \(\Ra\) {\darkgreen{print\_twice {\blue{\runtype{int\tsp{.5}*\tsp{.5}float}}} (1,3.14)}}
\CAML\end{alltt}
%CAMLEND

Classical ML programs can be executed efficiently without any overhead.
\end{slide}

\begin{slide}
\heading{Application of generic primitives}
Primitive functions for dynamic values 
can be defined as generic primitives:
%CAML val dynamic : \cforall$a.$a -> dyn
%CAML let dynamic_comp = fun {\blue{t}} x -> (x,{\blue{t}})
%CAML \(gen(\caml{dynamic}{,}\tau) \equiv \caml{dynamic\_comp} \tau\)
%CAML
%CAML val coerce : \cforall$a.dyn -> $a
%CAML let coerce_comp = fun {\blue{t}} (v,t') -> if {\blue{t}} \(\leq\) t' then v 
%CAML                                  \hspace{0.7mm}else raise Coercion_failure
%CAML \(gen(\caml{coerce}{,}\tau) \equiv \caml{coerce\_comp} \tau\)
\CAML\begin{alltt}
\CAML     val dynamic : \cforall\cdelta{}.\cdelta{}{\ra}dyn
\CAML     let dynamic_comp = fun {\blue{t}} x{\ra}(x,{\blue{t}})
\CAML     \(gen(\caml{dynamic}{,}\tau) \equiv \caml{dynamic\_comp} \tau\)
\CAML     
\CAML     val coerce : \cforall\cdelta{}.dyn{\ra}\cdelta{}
\CAML     let coerce_comp = fun {\blue{t}} (v,t'){\ra}if {\blue{t}} \(\leq\) t' then v 
\CAML                                      \hspace{0.7mm}else raise Coercion_failure
\CAML     \(gen(\caml{coerce}{,}\tau) \equiv \caml{coerce\_comp} \tau\)
\CAML\end{alltt}
%CAMLEND
(We need more careful type checking for encapsulation of polymorphic values.)
\end{slide}

\begin{slide}
\heading{Coherence problem of generic primitives -- \caml{dyn}-unification}
Generic primitive instances with more than one possible types
may have incompatible semantics depending on types -- coherence problem:
\adviwait
%CAML val print : \cforall$a.$a -> unit      val read : \cforall$a.unit -> $a
\CAML\begin{alltt}
\CAML     val print : \cforall\cdelta{}.\cdelta{}{\ra}unit      val read : \cforall\cdelta{}.unit{\ra}\cdelta{}
\CAML\end{alltt}
\adviwait
%CAML print (read ())
\CAML\begin{alltt}
\CAML     print (read ())
\CAML\end{alltt}
%CAMLEND
\adviwait
\vspace{-5mm}
\begin{minipage}[c]{0.4\textwidth}
%CAML print (read () : int)
%CAML print (read () : float)
%CAML print (read () : \advirecord[play]{d}{$a})
\CAML\begin{alltt}
\CAML     print (read () : int)
\CAML     print (read () : float)
\CAML     print (read () : \advirecord[play]{d}{\cdelta{}})
\CAML\end{alltt}
%CAMLEND
\end{minipage}~~~
\begin{minipage}[b]{0.4\textwidth}
\[\left\}  \begin{array}{l}
    ~ \\
    \mbox{incompatible semantics!}\\ ~
  \end{array}\right.\]
\end{minipage}

\adviwait
\adviplay[blue]{d}
Solution: {\blue free dynamic type variables} are forced to be unified with
some {\blue closed} type: 
\adviwait
{\blue\caml{dyn}},
since so that use of the free variables 
can be virtually postponed at run time:
%CAML 1                                \,(1,int)     
%CAML 3.14  \(\Longrightarrow\)  (read () : {\blue{dyn}})  \(\Longrightarrow\)  (3.14,float)
%CAML "1"                              \,("1",string)
\CAML\begin{alltt}
\CAML     1                                \,(1,int)     
\CAML     3.14  \(\Longrightarrow\)  (read () : {\blue{dyn}})  \(\Longrightarrow\)  (3.14,float)
\CAML     "1"                              \,("1",string)
\CAML\end{alltt}
%CAMLEND    
\end{slide}

\begin{slide}
\heading{User defined generics}
Definition by type cases, a list of type indexed expressions:
%CAML generic plus = case
%CAML | int -> int -> int => plus_int
%CAML | float -> float -> float => plus_float
%CAML in \ldots
\CAML\begin{alltt}
\CAML     generic plus = case
\CAML     | int{\ra}int{\ra}int \Ra plus_int
\CAML     | float{\ra}float{\ra}float \Ra plus_float
\CAML     in \ldots
\CAML\end{alltt}
%CAMLEND

%CAML plus 1 2      \(\leadsto\) 3 
%CAML plus 1.2 3.4  \(\leadsto\) 4.6
\CAML\begin{alltt}
\CAML     plus 1 2      \(\leadsto\) 3 
\CAML     plus 1.2 3.4  \(\leadsto\) 4.6
\CAML\end{alltt}
%CAMLEND
\end{slide}

\begin{slide}
\heading{Type case selection semantics by pattern match}
Case selection priority like pattern matching allows
overlapped instance definitions:
%CAML generic find_int = case
%CAML | {\blue\cforall$a.(int * $a) -> int} => fun (x,y) -> x
%CAML | {\blue\cforall$a.($a * int) -> int} => fun (x,y) -> y
%CAML ;;
\CAML\begin{alltt}
\CAML     generic find_int = case
\CAML     | {\blue\cforall\cdelta{}.(int\tsp{.5}*\tsp{.5}\cdelta{}){\ra}int} \Ra fun (x,y){\ra}x
\CAML     | {\blue\cforall\cdelta{}.(\cdelta{}\tsp{.5}*\tsp{.5}int){\ra}int} \Ra fun (x,y){\ra}y
\CAML     ;;
\CAML\end{alltt}
%CAMLEND

%CAML find_int (1, 3.14) \(\leadsto\) 1
%CAML find_int (3.14, 2) \(\leadsto\) 2
\CAML\begin{alltt}
\CAML     find_int (1, 3.14) \(\leadsto\) 1
\CAML     find_int (3.14, 2) \(\leadsto\) 2
\CAML\end{alltt}
%CAMLEND

The first match is selected when there are more than one:
%CAML find_int (1, 2)    \(\leadsto\) 1
\CAML\begin{alltt}
\CAML     find_int (1, 2)    \(\leadsto\) 1
\CAML\end{alltt}
%CAMLEND
\end{slide}

\begin{slide}
\heading{User defined generics -- recursion over types}
Recursive generic binding easily defines complex recursive overloaded values:
%CAML generic rec flat = case (* super list flattening *)
%CAML | \cforall$a$b.\advirecord[play]{1}{$a} list list -> \advirecord[play]{1}{$b} list => 
%CAML      fun x -> {\blue{flat}} (List.flatten x)
%CAML | \cforall$a.$a list -> $a list => fun x -> x
\CAML\begin{alltt}
\CAML     generic rec flat = case (* super list flattening *)
\CAML     | \cforall\cdelta{}\cdeltb{}.\advirecord[play]{1}{\cdelta{}} list list{\ra}\advirecord[play]{1}{\cdeltb{}} list \Ra 
\CAML          fun x{\ra}{\blue{flat}} (List.flatten x)
\CAML     | \cforall\cdelta{}.\cdelta{} list{\ra}\cdelta{} list \Ra fun x{\ra}x
\CAML\end{alltt}
%CAMLEND
(Multiple parameters {\blue $\delta$} and {\blue $\delta'$}
can be used without any problem.)
\adviplay[blue]{1}
\adviwait

It flattens lists:
%CAML # flat [[1]; [2;3]];;
%CAML - : int list = [1; 2; 3]\adviwait
\CAML\begin{alltt}
\CAML     # flat [[1]; [2;3]];;
\CAML     - : int list = [1; 2; 3]\adviwait
\CAML\end{alltt}
%CAMLEND
From any depth to one!
%CAML # flat [[[[1]; [2;3]]; [[4;5;6]]]; []];;
%CAML - : int list = [1; 2; 3; 4; 5; 6]
\CAML\begin{alltt}
\CAML     # flat [[[[1]; [2;3]]; [[4;5;6]]]; [\,]];;
\CAML     - : int list = [1; 2; 3; 4; 5; 6]
\CAML\end{alltt}
%CAMLEND

\end{slide}

\begin{slide}
\heading{User defined generics -- other examples}
Tautology checker
%CAML generic rec taut = case
%CAML | bool -> bool => fun x -> x
%CAML | \cforall$a.(bool -> $a) -> bool => 
%CAML       fun form -> taut (form true) && taut (form false)
%CAML ;;
\CAML\begin{alltt}
\CAML     generic rec taut = case
\CAML     | bool{\ra}bool \Ra fun x{\ra}x
\CAML     | \cforall\cdelta{}.(bool{\ra}\cdelta{}){\ra}bool \Ra 
\CAML           fun form{\ra}taut (form true) && taut (form false)
\CAML     ;;
\CAML\end{alltt}
%CAMLEND
%CAML # taut (fun p -> not p or p);; (* checks \(\forall{P}.\,\neg{P}\vee{P}\) *)
%CAML - : bool = true
\CAML\begin{alltt}
\CAML     # taut (fun p{\ra}not p or p);; (* checks \(\forall{P}.\,\neg{P}\vee{P}\) *)
\CAML     - : bool = true
\CAML\end{alltt}
%CAMLEND
\end{slide}

\begin{slide}
\heading{User defined generics -- other examples}
Function with variable length of arguments
%CAML generic rec vprint = case
%CAML | unit => ()
%CAML | \cforall$a$b.$a -> $b => fun x -> {\blue{print}} x; vprint
%CAML ;;
\CAML\begin{alltt}
\CAML     generic rec vprint = case
\CAML     | unit \Ra ()
\CAML     | \cforall\cdelta{}\cdeltb{}.\cdelta{}{\ra}\cdeltb{} \Ra fun x{\ra}{\blue{print}} x; vprint
\CAML     ;;
\CAML\end{alltt}
%CAMLEND

%CAML # vprint 1 3.14 "hello";;
%CAML 1 3.14 hello
%CAML - : unit = ()
\CAML\begin{alltt}
\CAML     # vprint 1 3.14 "hello";;
\CAML     1 3.14 hello
\CAML     - : unit = ()
\CAML\end{alltt}
%CAMLEND
\end{slide}

\begin{slide}
\heading{Typing and compilation: big picture}
\def\circ#1#2#3#4{
  \rput(#2,#3){\rnode{#1}{\pscircle(0,0){1}}}
  \rput(#2,#3){#4}
}
\psset{xunit=\textwidth,yunit=0.85\textheight}%

\def\anma{
  \circ{A}{0.1}{0.5}{
    \begin{tabular}{c}
      untyped\\[-2mm] source
    \end{tabular}
  }}
\def\anmaa{
  \circ{B}{0.3666}{0.5}{
    \begin{tabular}{c}
      fully type\\[-2mm] annotated\\[-2mm] program
    \end{tabular}}
  \rput(0.4944,0.77){
    \small \begin{tabular}{c}
      $E\models e_t:\tau ~\Lra~ r$\\[-2mm] semantics with types
    \end{tabular}}
}
\def\anmb{
  \ncline[nodesep=1.2cm,linewidth=1mm]{->}{A}{B}
  \rput[t](0.2333,0.43){\rnode{T1}{
      \small \begin{tabular}{c}
        normal\\[-1mm] typing\\[-1mm] 
        $\Gamma\vdash e_t:\tau$
        \end{tabular}}}
%   \rput(0.36,0.1){\small\rnode{Te}{type errors}}
%   \ncangle[angleA=-90,angleB=180,nodesep=1mm,linestyle=dashed]{->}{T1}{Te}
  }
\def\anmc{
  \circ{B2}{0.6222}{0.5}{
    \begin{tabular}{c}
      constraint\\[-2mm] annotated\\[-2mm] program
    \end{tabular}}
  \ncline[nodesep=1.2cm,linewidth=1mm]{->}{B}{B2}
  \rput[t](0.4944,0.43){\rnode{T2}{
      \small \begin{tabular}{c}
        generic\\[-1mm] constraint\\[-1mm] typing\\[-1mm]
        $\Gamma,V\kdash e_t:\tau$
        \end{tabular}}}
%    \ncangle[angleA=-90,angleB=0,nodesep=2mm,linestyle=dashed]{->}{T2}{Te}
  }
\def\anmd{
  \circ{C}{0.9}{0.8}{
    \begin{tabular}{c}
      type\\[-2mm] dispatch\\[-2mm] compilation\\[4mm]
    \end{tabular}
  }
  \ncline[nodesep=1.2cm,linewidth=1mm]{->}{B2}{C}
  \rput(0.88,0.5){
    \small \begin{tabular}{c}
      $\eenv \models e ~\Lra~ r$\\[-2mm] untyped semantics
    \end{tabular}
  }}
\def\anme{
  \circ{D}{0.9}{0.2}{
    \begin{tabular}{c}
      flow\\[-2mm] compilation\\[4mm]
    \end{tabular}
  }
  \rput(0.9,0.01){No type dispatching}
  \ncline[nodesep=1.2cm,linewidth=1mm]{->}{B2}{D}
  }
\vspace{-0.5cm}
\begin{superpose}
  \noindent\begin{pspicture}(1,1)\anma\end{pspicture}\\
  \advirecord{aa}{\noindent\begin{pspicture}(1,1)\anmaa\end{pspicture}}\\
  \advirecord{b}{\noindent\begin{pspicture}(1,1)\anmb\end{pspicture}}\\
  \advirecord{c}{\noindent\begin{pspicture}(1,1)\anmc\end{pspicture}}\\
  \advirecord{d}{\noindent\begin{pspicture}(1,1)\anmd\end{pspicture}}\\
  \advirecord{e}{\noindent\begin{pspicture}(1,1)\anme\end{pspicture}}\\
\end{superpose}
\adviwait\adviplay[blue]{aa}
\adviwait\adviplay[black]{aa}\adviplay[blue]{b}
\adviwait\adviplay[black]{b}\adviplay[blue]{c}
\adviwait\adviplay[black]{c}\adviplay[blue]{d}
\adviwait\adviplay[black]{d}\adviplay[blue]{e}
\end{slide}

\begin{slide}
\heading{Type checking of generics -- two typing layers}
Normal typing layer: $\Gamma\vdash e_t:\tau$
  \begin{itemize}
  \item Regular ML typing with minimal extension (= dynamic variables)
  \item User defined generics have type schemes as 
    {\blue anti-unifiers} of type cases:
%CAML generic plus = case
%CAML | {\blue{int -> int -> int}} => plus\_int
%CAML | {\blue{float -> float -> float}} => plus\_float
%CAML ;;
\CAML\begin{alltt}
\CAML     generic plus = case
\CAML     | {\blue{int{\ra}int{\ra}int}} \Ra plus\_int
\CAML     | {\blue{float{\ra}float{\ra}float}} \Ra plus\_float
\CAML     ;;
\CAML\end{alltt}
%CAMLEND
\adviwait
%CAML val plus : {\blue\cforall$a.$a -> $a -> $a}
\CAML\begin{alltt}
\CAML     val plus : {\blue\cforall\cdelta{}.\cdelta{}{\ra}\cdelta{}{\ra}\cdelta{}}
\CAML\end{alltt}
%CAMLEND
\adviwait
  \item Types may be {\blue too general}.
%CAML plus "hello" "world"   \mbox{\rm{well-typed, but lacks semantics}}
\CAML\begin{alltt}
\CAML     plus "hello" "world"   \mbox{\rm{well-typed, but lacks semantics}}
\CAML\end{alltt}
%CAMLEND
  \item but are good {\blue approximation} to provide principal typings.
  \end{itemize}
\end{slide}

\begin{slide}
\heading{Type checking of generics -- two typing layers}
Generic constraint typing layer: $\Gamma,V\kdash e_t:\tau$
  \begin{itemize}
  \item For detecting illegal uses of user generics without semantics
  \item User generics are assigned with {\blue{generic constraints}}:
%CAML plus : \adviwait \adviplay[blue]{1}[ {\blue{int -> int -> int}} | {\blue{float -> float -> float}} ]
\CAML\begin{alltt}
\CAML     plus : \adviwait \adviplay[blue]{1}[ {\blue{int{\ra}int{\ra}int}} | {\blue{float{\ra}float{\ra}float}} ]
\CAML\end{alltt}
%CAMLEND    
    Generic constraints constraint type instantiations of
    too general type schemes obtaind in the normal layer.
%CAML val plus : \cforall$a.$a -> $a -> $a
\CAML\begin{alltt}
\CAML     val plus : \cforall\cdelta{}.\cdelta{}{\ra}\cdelta{}{\ra}\cdelta{}
\CAML\end{alltt}
%CAMLEND

%CAML plus : int -> int -> int             \mbox{\rm{ok}}
%CAML plus : float -> float -> float       \mbox{\rm{ok}}
%CAML plus : string -> string -> string    \mbox{\rm{type error}}
\CAML\begin{alltt}
\CAML     plus : int{\ra}int{\ra}int             \mbox{\rm{ok}}
\CAML     plus : float{\ra}float{\ra}float       \mbox{\rm{ok}}
\CAML     plus : string{\ra}string{\ra}string    \mbox{\rm{type error}}
\CAML\end{alltt}
%CAMLEND
  \end{itemize}

\end{slide}

\begin{slide}
\heading{Type checking of generics -- generic constraints}
Generic constraint represents the set of valid instance types.

%CAML generic plus = case
%CAML | {\blue{int -> int -> int}} => plus\_int
%CAML | {\blue{float -> float -> float}} => plus\_float
%CAML ;;
\CAML\begin{alltt}
\CAML     generic plus = case
\CAML     | {\blue{int{\ra}int{\ra}int}} \Ra plus\_int
\CAML     | {\blue{float{\ra}float{\ra}float}} \Ra plus\_float
\CAML     ;;
\CAML\end{alltt}
%CAMLEND

%CAML \(\konstr{plus} =\) [ {\blue{int -> int -> int}} | {\blue{float -> float -> float}} ]
\CAML\begin{alltt}
\CAML     \(\konstr{plus} =\) [ {\blue{int{\ra}int{\ra}int}} | {\blue{float{\ra}float{\ra}float}} ]
\CAML\end{alltt}
%CAMLEND

Intuitively, it is a list of type patterns. 

%CAML          int -> int -> int \(\kin \konstr{plus}\)
%CAML    float -> float -> float \(\kin \konstr{plus}\)
%CAML string -> string -> string \(\not\kin \konstr{plus}\)
\CAML\begin{alltt}
\CAML              int{\ra}int{\ra}int \(\kin \konstr{plus}\)
\CAML        float{\ra}float{\ra}float \(\kin \konstr{plus}\)
\CAML     string{\ra}string{\ra}string \(\not\kin \konstr{plus}\)
\CAML\end{alltt}
\end{slide}

\begin{slide}
\heading{Type checking of generics -- generic constraints}
Internal use of other generics also adds constraints:
%CAML let double x = {\blue{plus}} x x;;
\CAML\begin{alltt}
\CAML     let double x = {\blue{plus}} x x;;
\CAML\end{alltt}
%CAMLEND

%CAML \(\konstr{double} =\) [ \cforall$a.$a -> $a {\blue\{ $a -> $a -> $a \(\kin \Kappa\sb{\caml{plus}}\)\}} ]
\CAML\begin{alltt}
\CAML     \(\konstr{double} =\) [ \cforall\cdelta{}.\cdelta{}{\ra}\cdelta{} {\blue\{ \cdelta{}{\ra}\cdelta{}{\ra}\cdelta{} \(\kin \Kappa\sb{\caml{plus}}\)\}} ]
\CAML\end{alltt}
%CAMLEND

%CAML       int -> int \(\kin \konstr{double}\)
%CAML   float -> float \(\kin \konstr{double}\)
%CAML string -> string \(\not\kin \konstr{double}\)
\CAML\begin{alltt}
\CAML           int{\ra}int \(\kin \konstr{double}\)
\CAML       float{\ra}float \(\kin \konstr{double}\)
\CAML     string{\ra}string \(\not\kin \konstr{double}\)
\CAML\end{alltt}
%CAMLEND
\end{slide}

\begin{slide}
\heading{Type checking of generics -- generic constraints}
Recursive use of generics produce recursive constraints
%CAML generic rec flat = case
%CAML | \advirecord[play]{1}{\cforall$a$b. $a list list -> $b list} => 
%CAML     fun x -> (\advirecord[play]{2}{\advirecord[play]{3}{flat} : $a list -> $b list}) (List.flatten x)
%CAML | \advirecord[play]{1}{\cforall$a.$a list -> $a list} => fun x -> x
%CAML ;;
\CAML\begin{alltt}
\CAML     generic rec flat = case
\CAML     | \advirecord[play]{1}{\cforall\cdelta{}\cdeltb{}. \cdelta{} list list{\ra}\cdeltb{} list} \Ra 
\CAML         fun x{\ra}(\advirecord[play]{2}{\advirecord[play]{3}{flat} : \cdelta{} list{\ra}\cdeltb{} list}) (List.flatten x)
\CAML     | \advirecord[play]{1}{\cforall\cdelta{}.\cdelta{} list{\ra}\cdelta{} list} \Ra fun x{\ra}x
\CAML     ;;
\CAML\end{alltt}
%CAMLEND

%CAML \(\konstr{flat} =\)
%CAML    \advirecord[play]{3}{\(\mu\kappa\).}[ \advirecord[play]{1}{\cforall$a$b. $a list list -> $b list} \advirecord[play]{2}{\{ $a list -> $b list \(\kin\) \advirecord[play]{3}{\(\kappa\)} \}}
%CAML       \,| \advirecord[play]{1}{\cforall$a.$a list -> $a list} ]
\CAML\begin{alltt}
\CAML     \(\konstr{flat} =\)
\CAML        \advirecord[play]{3}{\(\mu\kappa\).}[ \advirecord[play]{1}{\cforall\cdelta{}\cdeltb{}. \cdelta{} list list{\ra}\cdeltb{} list} \advirecord[play]{2}{\{ \cdelta{} list{\ra}\cdeltb{} list \(\kin\) \advirecord[play]{3}{\(\kappa\)} \}}
\CAML           \,| \advirecord[play]{1}{\cforall\cdelta{}.\cdelta{} list{\ra}\cdelta{} list} ]
\CAML\end{alltt}
%CAMLEND

\adviwait\adviplay[blue]{1}
\adviwait\adviplay[black]{1}\adviplay[blue]{2}
\adviwait\adviplay[black]{2}\adviplay[blue]{3}

\adviwait
%CAML int list list list -> int list \(\kin \konstr{flat}\)
%CAML int list list list -> int list list \(\kin \konstr{flat}\)
%CAML int list list list -> int list list list \(\kin \konstr{flat}\)
%CAML \ldots
\CAML\begin{alltt}
\CAML     int list list list{\ra}int list \(\kin \konstr{flat}\)
\CAML     int list list list{\ra}int list list \(\kin \konstr{flat}\)
\CAML     int list list list{\ra}int list list list \(\kin \konstr{flat}\)
\CAML     \ldots
\CAML\end{alltt}
%CAMLEND
\end{slide}

\begin{slide}
\heading{Type inference of user generics -- coherence}
Instance of user generics may have more than one typing:
%CAML flat [[[1]]] : int list
%CAML flat [[[1]]] : int list list
%CAML flat [[[1]]] : int list list list
\CAML\begin{alltt}
\CAML     flat [[[1]]] : int list
\CAML     flat [[[1]]] : int list list
\CAML     flat [[[1]]] : int list list list
\CAML\end{alltt}
%CAMLEND

\adviwait
Usual pattern matching priority rule 
leads to the default typing selection rule.
%CAML generic rec flat = case
%CAML \advirecord{0}{\colorbox{white}{\begin{superpose}\advirecord{1}{| \cforall$a$b.$a list list -> $b list => fun x -> flat (List.flatten x)\\\advirecord{2}{| \cforall$a.$a list -> $a list => fun x -> x\hspace{5cm}}\end{superpose}}}}
%CAML \advirecord{0}{\colorbox{white}{\begin{superpose}\advirecord{1}{| \cforall$a.$a list -> $a list => fun x -> x\hspace{5cm}}\\\advirecord{2}{| \cforall$a$b.$a list list -> $b list => fun x -> flat (List.flatten x)}\end{superpose}}}
\CAML\begin{alltt}
\CAML     generic rec flat = case
\CAML     \advirecord{0}{\colorbox{white}{\begin{superpose}\advirecord{1}{| \cforall\cdelta{}\cdeltb{}.\cdelta{} list list{\ra}\cdeltb{} list \Ra fun x{\ra}flat (List.flatten x)\\\advirecord{2}{| \cforall\cdelta{}.\cdelta{} list{\ra}\cdelta{} list \Ra fun x{\ra}x\hspace{5cm}}\end{superpose}}}}
\CAML     \advirecord{0}{\colorbox{white}{\begin{superpose}\advirecord{1}{| \cforall\cdelta{}.\cdelta{} list{\ra}\cdelta{} list \Ra fun x{\ra}x\hspace{5cm}}\\\advirecord{2}{| \cforall\cdelta{}\cdeltb{}.\cdelta{} list list{\ra}\cdeltb{} list \Ra fun x{\ra}flat (List.flatten x)}\end{superpose}}}
\CAML\end{alltt}
%CAMLEND
%CAML # flat [[[1]]];;
%CAML - : \advirecord{a0}{\colorbox{white}{\begin{superpose}\advirecord{a1}{int list = [1]\hspace{2.6cm}}\\\advirecord{a2}{int list list list = [[[1]]]}\end{superpose}}} 
\CAML\begin{alltt}
\CAML     # flat [[[1]]];;
\CAML     - : \advirecord{a0}{\colorbox{white}{\begin{superpose}\advirecord{a1}{int list = [1]\hspace{2.6cm}}\\\advirecord{a2}{int list list list = [[[1]]]}\end{superpose}}} 
\CAML\end{alltt}
%CAMLEND
\adviplay{1}\adviplay{a1}
% \adviwait\adviplay[blue]{1}
% \adviwait
% \adviplay{0}\adviplay[blue]{2}
% \adviwait
% \adviplay{a0}
% \adviplay[blue]{a2}
% \adviwait
% \adviplay{2}\adviplay{a2}
\adviwait
Other typings can be selected by giving type information explicitly:
%CAML # (flat [[[1]]] : {\blue{int list list}});;
%CAML - : int list list = [[1]]
\CAML\begin{alltt}
\CAML     # (flat [[[1]]] : {\blue{int list list}});;
\CAML     - : int list list = [[1]]
\CAML\end{alltt}
%CAMLEND
\end{slide}

% \begin{slide}
% \heading{Type inference of user generics -- coherence}
% Another example:
% %CAML generic rec vprint = case
% %CAML | unit => ()
% %CAML | \cforall$a$b.$a -> $b => fun x -> {\blue{print}} x; vprint
% %CAML ;;
% \CAML\begin{alltt}
% \CAML     generic rec vprint = case
% \CAML     | unit \Ra ()
% \CAML     | \cforall\cdelta{}\cdeltb{}.\cdelta{}{\ra}\cdeltb{} \Ra fun x{\ra}{\blue{print}} x; vprint
% \CAML     ;;
% \CAML\end{alltt}
% %CAMLEND

%CAML # vprint 1 3.14 "hello";;
%CAML 1 3.14 hello
%CAML - : unit = ()
\CAML\begin{alltt}
\CAML     # vprint 1 3.14 "hello";;
\CAML     1 3.14 hello
\CAML     - : unit = ()
\CAML\end{alltt}
%CAMLEND

%CAML # (vprint 1 3.14 "hello" {\blue: bool -> unit});;
%CAML 1 3.14 hello
%CAML - : bool -> unit = ()
\CAML\begin{alltt}
\CAML     # (vprint 1 3.14 "hello" {\blue: bool{\ra}unit});;
\CAML     1 3.14 hello
\CAML     - : bool{\ra}unit = ()
\CAML\end{alltt}
%CAMLEND
\end{slide}

\begin{slide}
\heading{Compilation of user generics -- type passing}
Classical compilation by type passing:
%CAML generic rec flat = case
%CAML | \cforall$a$b.$a list list -> $b list => 
%CAML      flat (List.flatten x)
%CAML | \cforall$a.$a list -> $a list => fun x -> x
%CAML in flat [[[1]]]
\CAML\begin{alltt}
\CAML     generic rec flat = case
\CAML     | \cforall\cdelta{}\cdeltb{}.\cdelta{} list list{\ra}\cdeltb{} list \Ra 
\CAML          flat (List.flatten x)
\CAML     | \cforall\cdelta{}.\cdelta{} list{\ra}\cdelta{} list \Ra fun x{\ra}x
\CAML     in flat [[[1]]]
\CAML\end{alltt}
%CAMLEND
\adviwait

\vfill

{\darkgreen
%CAML       \(\black\Ra\)    let rec flat = fun \advirecord[play]{1}{ty ty'} ->
%CAML               \advirecord[play]{2}{match ty, ty' with}
%CAML               \advirecord[play]{2}{| <<t list, t'>> -> }
%CAML                   flat \advirecord[play]{3}{<<t>> <<t'>>} (List.flatten x)
%CAML               \advirecord[play]{2}{| <<t>>, <<t>> ->} fun x -> x
%CAML             in flat \advirecord[play]{1}{<<int list list>> <<int>>} [[[1]]]
\CAML\begin{alltt}
\CAML           \(\black\Ra\)    let rec flat = fun \advirecord[play]{1}{ty ty'} \ra
\CAML                   \advirecord[play]{2}{match ty, ty' with}
\CAML                   \advirecord[play]{2}{| \runtype{t list, t'}{\ra}}
\CAML                       flat \advirecord[play]{3}{\runtype{t} \runtype{t'}} (List.flatten x)
\CAML                   \advirecord[play]{2}{| \runtype{t}, \runtype{t} \ra} fun x{\ra}x
\CAML                 in flat \advirecord[play]{1}{\runtype{int list list} \runtype{int}} [[[1]]]
\CAML\end{alltt}
%CAMLEND
}
\adviwait\adviplay[blue]{1}\adviplay[blue]{3}
\adviwait\adviplay[darkgreen]{1}\adviplay[darkgreen]{3}\adviplay[blue]{2}
\adviwait\adviplay[darkgreen]{2}
Type case selection is performed statically during typing:
use it to compile!
\end{slide}

\begin{slide}
\heading{Compilation of user generics -- generic flow passing}
Dispatching {\blue generic flows}, witness of successful type case
selections obtained from generic constraint typing.

%CAML generic plus = case
%CAML | int -> int -> int => plus_int
%CAML | float -> float -> float => plus_float
%CAML in
%CAML plus 1 2
%CAML ;;
\CAML\begin{alltt}
\CAML     generic plus = case
\CAML     | int{\ra}int{\ra}int \Ra plus_int
\CAML     | float{\ra}float{\ra}float \Ra plus_float
\CAML     in
\CAML     plus 1 2
\CAML     ;;
\CAML\end{alltt}

{\darkgreen
%CAML         \(\black\Ra\)      let plus = 
%CAML                   let tcs = [| {\blue{plus_int}}; plus_float |] in
%CAML                   fun pos -> tcs.(pos)
%CAML                 in
%CAML                 plus {\blue{0}} (* flow to access plus_int *) 1 2
%CAML                 ;;
\CAML\begin{alltt}
\CAML             \(\black\Ra\)      let plus = 
\CAML                       let tcs = [| {\blue{plus_int}}; plus_float |] in
\CAML                       fun pos{\ra}tcs.(pos)
\CAML                     in
\CAML                     plus {\blue{0}} (* flow to access plus_int *) 1 2
\CAML                     ;;
\CAML\end{alltt}
%CAMLEND
}

\end{slide}

\begin{slide}
\heading{Compilation of user generics -- generic flow passing}
Generic flows are integer {\blue graphs}, 
corresponding to the graph of generic calls. 

%CAML generic rec flat = case
%CAML | \cforall$a$b.$a list list -> $b list => 
%CAML      {\blue{flat}} (List.flatten x)
%CAML | \cforall$a.$a list -> $a list => fun x -> x
%CAML ;;
\CAML\begin{alltt}
\CAML     generic rec flat = case
\CAML     | \cforall\cdelta{}\cdeltb{}.\cdelta{} list list{\ra}\cdeltb{} list \Ra 
\CAML          {\blue{flat}} (List.flatten x)
\CAML     | \cforall\cdelta{}.\cdelta{} list{\ra}\cdelta{} list \Ra fun x{\ra}x
\CAML     ;;
\CAML\end{alltt}
%CAMLEND

{\darkgreen
%CAML  \(\black\Ra\) type flow = int * flow array (* integer graph *)
\CAML\begin{alltt}
\CAML      \(\black\Ra\) type flow = int\tsp{.5}*\tsp{.5}flow array (* integer graph *)
\CAML\end{alltt}
%CAMLEND

%CAML     let rec flat = 
%CAML       let tcs = 
%CAML         [| \advirecord[play]{1}{fun {\blue{subs}} -> fun x -> flat {\blue{subs.(0)}} (List.flatten x)};
%CAML            \advirecord[play]{2}{fun {\blue{subs}} -> fun x -> x} |] 
%CAML       in
%CAML       fun (p,{\blue{subs}}) -> tm.(p) {\blue{subs}}
%CAML     ;;
\CAML\begin{alltt}
\CAML         let rec flat = 
\CAML           let tcs = 
\CAML             [| \advirecord[play]{1}{fun {\blue{subs}}{\ra}fun x{\ra}flat {\blue{subs.(0)}} (List.flatten x)};
\CAML                \advirecord[play]{2}{fun {\blue{subs}}{\ra}fun x{\ra}x} |] 
\CAML           in
\CAML           fun (p,{\blue{subs}}){\ra}tm.(p) {\blue{subs}}
\CAML         ;;
\CAML\end{alltt}
%CAMLEND
}

\end{slide}

\begin{slide}
\heading{Compilation of user generics -- generic flow passing}
Generic flows are integer graphs, 
following the tree structure of generic calls. 

{\darkgreen
%CAML let rec flat = 
%CAML   let tcs = 
%CAML     [| \advirecord[play]{1}{fun subs -> fun x -> flat subs.(0) (List.flatten x)};
%CAML        \advirecord[play]{2}{fun subs -> fun x -> x} |] 
%CAML   in
%CAML   fun (p,subs) -> tm.(p) subs
%CAML ;;
\CAML\begin{alltt}
\CAML     let rec flat = 
\CAML       let tcs = 
\CAML         [| \advirecord[play]{1}{fun subs{\ra}fun x{\ra}flat subs.(0) (List.flatten x)};
\CAML            \advirecord[play]{2}{fun subs{\ra}fun x{\ra}x} |] 
\CAML       in
\CAML       fun (p,subs){\ra}tm.(p) subs
\CAML     ;;
\CAML\end{alltt}
%CAMLEND
}

%CAML flat [[[1]]] : int list  =>   {\darkgreen{flat (\advirecord[play]{a0}{0} -> 0 -> 1) [[[1]]]}}
%CAML \advirecord{a1}{                         \(\black\leadsto\)   {\darkgreen{flat (\advirecord{a11}{0} -> 1) [[1]]}}}
%CAML \advirecord{a2}{                         \(\black\leadsto\)   {\darkgreen{flat (\advirecord{a21}{1}) [1]}}}
%CAML \advirecord{a3}{                         \(\black\leadsto\)   [1]}
\CAML\begin{alltt}
\CAML     flat [[[1]]] : int list  \Ra   {\darkgreen{flat (\advirecord[play]{a0}{0}{\ra}0{\ra}1) [[[1]]]}}
\CAML     \advirecord{a1}{                         \(\black\leadsto\)   {\darkgreen{flat (\advirecord{a11}{0}{\ra}1) [[1]]}}}
\CAML     \advirecord{a2}{                         \(\black\leadsto\)   {\darkgreen{flat (\advirecord{a21}{1}) [1]}}}
\CAML     \advirecord{a3}{                         \(\black\leadsto\)   [1]}
\CAML\end{alltt}
%CAMLEND
\adviwait
\adviplay[blue]{1}\adviplay[blue]{a0}
\adviwait
\adviplay[darkgreen]{a0}\adviplay[blue]{1}
\adviplay[darkgreen]{1}\adviplay{a1}\adviplay[darkgreen]{a11}
\adviwait
\adviplay[blue]{a11}\adviplay[blue]{1}
\adviwait
\adviplay[darkgreen]{a21}
\adviplay[darkgreen]{1}\adviplay[darkgreen]{a11}\adviplay[darkgreen]{a2}
\adviwait
\adviplay[blue]{a21}\adviplay[blue]{2}
\adviwait
\adviplay[darkgreen]{2}\adviplay[darkgreen]{a21}
\adviplay[darkgreen]{a3}
\end{slide}

\begin{slide}
\heading{Compilation of user generics -- generic flow passing}
Generic flow passing supersedes type passing:
\begin{itemize}
\item Type case selection is performed in constant time,
  regardless of type pattern complexity.
\item Upward compatible and better type case selection semantics
  with {\blue static backtracking}, precomputed at {\blue static
    typing} time. 
%CAML generic rec flat = case
%CAML | \cforall$a$b.$a list list -> $b list => 
%CAML      flat (List.flatten x)
%CAML | \cforall$a.$a list -> $a list => fun x -> x
%CAML ;;
\CAML\begin{alltt}
\CAML     generic rec flat = case
\CAML     | \cforall\cdelta{}\cdeltb{}.\cdelta{} list list{\ra}\cdeltb{} list \Ra 
\CAML          flat (List.flatten x)
\CAML     | \cforall\cdelta{}.\cdelta{} list{\ra}\cdelta{} list \Ra fun x{\ra}x
\CAML     ;;
\CAML\end{alltt}
%CAMLEND

%CAML flat : int list list -> int list list
\CAML\begin{alltt}
\CAML     flat : int list list{\ra}int list list
\CAML\end{alltt}
%CAMLEND
\begin{itemize}
\item Run time type pattern matching cannot give 
  semantics 
\item Flow passing can select the second case
\end{itemize}
\end{itemize}
\end{slide}

% \begin{slide}
% \heading{Compilation of user generics -- generic flow passing}
% Generic flow passing can be compared with Haskell's dictionary passing:
% \begin{itemize}
% \item Generic flow passing allows local definitions of overloaded values.
% \item Compiled code is not typable unfortunately.
% \end{itemize}
% \end{slide}

\begin{slide}
\heading{Other topics...}
\begin{itemize}
\item Primitives for type safe data exchange between arbitrary ML programs
  \begin{itemize}
  \item Data type identification 
    using encrypted check-sums of type definitions. 
  \end{itemize}
\adviwait
\item Incremental generic definition by inclusion:
%CAML generic rec plus' = case
%CAML | {\blue{include plus}}
%CAML | $a * $b -> $a * $b -> $a * $b => 
%CAML       fun (x,y) (z,w) -> (plus' x z, plus' y w)
\CAML\begin{alltt}
\CAML     generic rec plus' = case
\CAML     | {\blue{include plus}}
\CAML     | \cdelta{}\tsp{.5}*\tsp{.5}\cdeltb{}{\ra}\cdelta{}\tsp{.5}*\tsp{.5}\cdeltb{}{\ra}\cdelta{}\tsp{.5}*\tsp{.5}\cdeltb{} \Ra 
\CAML           fun (x,y) (z,w){\ra}(plus' x z, plus' y w)
\CAML\end{alltt}
%CAMLEND
\adviwait
    Open recursion within closed extension:
%CAML generic plus'' = case
%CAML | {\blue{include plus'}}
%CAML | string -> string -> string => String.concat
\CAML\begin{alltt}
\CAML     generic plus'' = case
\CAML     | {\blue{include plus'}}
\CAML     | string{\ra}string{\ra}string \Ra String.concat
\CAML\end{alltt}
%CAMLEND
Internal recursive calls in 
%caml plus'
\caml{plus'} %-caml
are automatically redirected to 
%caml plus'':
\caml{plus'':} %-caml

%CAML plus'' ("hello ",1) ("world,2) \(\leadsto\) ("hello world", 3)
\CAML\begin{alltt}
\CAML     plus'' ("hello ",1) ("world,2) \(\leadsto\) ("hello world", 3)
\CAML\end{alltt}
%CAMLEND

\end{itemize}
\end{slide}

\begin{slide}
\heading{Future work}
\begin{itemize}
\item Refinement of type inference:
  \begin{itemize}
  \item ex. functional dependencies of Haskell type class
  \end{itemize}
\item Open extension ? (maybe with Haskell like typing restrictions)
\item Implementation: 
  \begin{itemize}
  \item Prototype has been developed.
  \item Coexistence with other type extensions:
    (O'Caml's classes, polymorphic variants, etc...)
%  \item Political struggle for integration into the official release
%    \caml{:-)}
  \end{itemize}
\end{itemize}
\end{slide}

\begin{slide}
\heading{Conclusion}
Extensional polymorphism\ldots
\begin{itemize}
\item is non-parametric polymorphism extension over ML
\item supports type passing based ad-hoc polymorphic generic
  primitives,
  including almighty ML value printer, dynamic values, etc.
\item provides user definition of overloaded values
  \begin{itemize}
  \item pattern matching based definitions allow
    nice semantics and typing
  \item independent typing system for generics
    simplifies both theory and implementation
  \item new generic flow compilation performs
    powerful case selection
  \end{itemize}
\item new type-value computation methodology:
  ex. \caml{taut}, \caml{flat}, \caml{vprint} etc.
\end{itemize}
\end{slide}

\end{document}