\documentstyle[11pt,proof]{article}
\bibstyle{plain}
\parindent=0.0cm
\parskip=0.4cm
\setlength{\textwidth}{15cm}
\setlength{\oddsidemargin}{+0.4cm}
\setlength{\evensidemargin}{0.4cm}
\setlength{\topmargin}{+0.0cm}
\setlength{\headheight}{1cm}
\setlength{\textheight}{22cm}
\setlength{\headsep}{1cm}
\renewcommand{\baselinestretch}{1.0}
\def\nvec#1,#2{#1_{1}, \ldots, #1_{#2}}

\pagestyle{plain}

%\marginparwidth 0pt \oddsidemargin 0pt
%\evensidemargin 0pt \marginparsep 0pt
%\topmargin 0pt

%\textwidth 6.5in \textheight 8.5in

%\setlength{\parskip}{6pt}
%\pagestyle{plain}
%\newcommand\Pscr {{\cal P}}
\newcommand\rrr  {\rightarrow}
\newcommand\lrr  {\longrightarrow}
\newcommand\lrrs {\stackrel{\ast}{\longrightarrow}}
\newcommand\lrrb {\stackrel{\ast}{\longleftrightarrow}}

\begin{document}

\begin{center}
  {\LARGE\bf Class Notes on Type Inference}\\[5pt]
  {\normalsize\bf 2024 edition}\\  
  {\normalsize\bf Chuck Liang}\\
  {\normalsize\bf Hofstra University Computer Science}
\end{center}

\normalsize

\bigskip
\subsection*{Background and Introduction}

Many modern programming languages that are designed for applications
programming impose typing disciplines on the construction of programs.
In constrast to untyped languages such as Scheme/Perl/Python/JS, etc, and
weakly typed languages such as C, a strongly typed language (C\#/Java, Ada,
F\#, etc ...) place constraints on how programs can be written.  A
type system ensures that programs observe logical structure.  The
origins of type theory stretches back to the early twentieth century
in the work of Bertrand Russell and Alfred N. Whitehead and their {\em
``Principia Mathematica.''\/} They observed that our language, 
if not restrained, can lead to unsolvable paradoxes.

Specifically, let's say a mathematician defined $S$ to be 
{\em the set of all sets that do not contain themselves.\/}  That is:
\[S =\{all~A ~:~ A \not\in A \}\]  Then it is valid to ask the question {\em
does $S$ contain itself\/} ($S\in S$?).  If the answer is yes, then
by definition of $S$, $S$ is one of the '$A$'s, and thus $S\not\in S$.
But if $S\not\in S$, then $S$ is one of those sets that do not contain
themselves, and so it must be that $S\in S$!  

This observation is known as {\em Russell's Paradox.\/} In order to
avoid this paradox, the language of mathematics (or any language for
that matter) must be {\em constrained\/} so that the set $S$ cannot be
defined.  This is one of many discoveries that resulted from the
careful study of language, logic and meaning that formed the
foundation of twentieth century analytical philosophy and abstract
mathematics, and also that of computer science.  The type theory used
in computer science today is derived from a 1940 paper by Alonzo
Church called {\it``A Formulation of the Simple Theory of Types.''\/}
It was given in the context of Church's $\lambda$-calculus.


\subsection*{The Syntax of Types}

Programming languages have a variety of syntax for expressing types.
In general, type expressions are categorized into atomic or primitive
types such as \verb+int+, \verb+double+, \verb+char+, etc..., and
compound types that involves a {\em type constructor.\/} Examples of
type constructors include structs and classes.  A struct (or class)
containing an int and a char can be represented as $int * char$ type
(a cartesian product).  Additional type constructors depends on the
language, such as * in C/C++ that indicates a pointer type.  Functions
have types of the form $A\rrr B$ where A represents the type of its
parameters (domain) and B represents the return type (codomain).  For
example, a C function
\begin{verbatim}
int f(int x, char y)
\end{verbatim}
can be said to have type $(int * char)\rrr int$.  The $\rrr$ constructor
associates to the right.
\verb+void+ is the empty
set and can be given the label $0$ (in F\#, it's called 'unit').  The void type should be associated with
all formulas that generate side effects as opposed to returning a value.
For example, a \verb+cout+ statement in C++ can be said to have the void type.

We write $S:\tau$ if expression $S$ has type $\tau$.  Such formulas are
called {\em type judgements.\/}  


\subsection*{Type Checking Expressions}

  To say that a program is ``well-typed'' is to be able to assign a
type to every subexpression of the program.  A statement such as
\verb+cout+ is well-typed if every expression processed by the
statement is well-typed.  However, just because a program is
well-typed does not mean it's correct, only that it is logically
structured.  Each typed language defines a set of rules for
determining what (if any) types each expression should have.  We can study
type theory in a pure setting using the 
{\em typed\/} $\lambda$-calculus.  The
$\lambda$-calculus contains two basic forms of expressions:
applications of the form $(A~B)$ and abstractions of the form $\lambda
x. A$.  Types for constants are assumed: for example, $3:int$ is
assumed to always be a true type judgement.  Built-in functions are
also considered constants: for example, '+' has type $(int * int) \rrr
int$.  Whether a function such as '+' is infix (in C) or prefix (in
Scheme) is a purely syntactic matter and is irrelevant here: what
matters is that it's a function that takes two integers and returns an
integer\footnote{Of course, '+' is an overloaded operator that can
also be used to add floats - which '+' we're talking about are often
inferred from context.}.

Types for variables depend on a {\em type environment,\/} which is a
set of type judgements of the form $x:\tau$.  The type environment is
usually labeled $\Gamma$.  For example, if we make the
following declarations
\begin{verbatim}
int x, y;
char z;
double u;
\end{verbatim}
Then $\Gamma$ will include $x:int, ~y:int, ~ z:char, ~u:double$ for
this section of the code.  The set $\Gamma$ is referred to as a {\it
signature.\/} Java/C\# interfaces and C/C++ header files are 
manifestations of the signature concept, but the idea of a signature is
much more general than either of these constructs.

  Given a signature, type judgements are inferred using one of the
  following rules:

\[
\infer[id]{S:\tau}{S:\tau \in \Gamma} ~~~~~~~
\]
\[
\infer[app]{(A ~B) :\tau}{A: \sigma \rrr \tau & B:\sigma}
\]
\[
\infer[abs]{\lambda x.A : 
\sigma\rrr \tau}{A:\tau ~~{\mbox{\small with $x:\sigma$ temporarily added
to $\Gamma$}}}
\]

These rules can be read in both a forward and a backward
(``goal-directed'') manner.  The first rule (id) simply says that if
$\Gamma$ already contains a judgement, then it's trivial to infer that
judgement.  For example, $x:int$ can be inferred trivially from the
C-style declarations earlier.  The second rule says that when you apply a
function to an argument, the type of the argument must match the type
of the domain of the function, and that the result of the application
will be the type of the codomain of the function.  The third
rule is most interesting: it says that to show that a function has
type $\sigma \rrr \tau$, {\em temporarily\/} assume that its parameter
has type $\sigma$, and under this temporary assumption show that the
body or return value of the function has type $\tau$.  Why
temporarily?  Because, as you should know well by now, formal
parameters ($\lambda$-bound variables) have LOCAL scope.   We must
discard the assumption after applying this type inference rule so that
it does not interfere with other parts of the program.
If you were writing a compiler or interpreter, $\Gamma$ is your ``symbol table.''

\subsection*{Product Types and Currying}

  When dealing with a cartesian-product type (for functions that take
more than one paramenters, for example), we need the following rules:

\[
\infer{(A,B): \sigma * \tau}{A:\sigma & B:\tau}
\]
\[
\infer{A:\sigma}{(A,B): \sigma * \tau} ~~~~~~
\infer{B:\tau}{(A,B): \sigma * \tau}
\]
These rules will combine multiple parameters into one parameter.  It also
allows us to use structs (or classes) that combine multiple elements into one
object.  

It is also always possible to convert a function that takes two (or
more) parameters into a function that takes one parameter using a
process called ``Currying'', after the logician Haskell Curry.  That
is, a function of type $A*B\rrr C$ can be converted to a function of
type $A\rrr (B\rrr C)$.  The second function takes the first parameter
and {\em returns a function\/} that takes the second parameter.  The
technique also allows us to simplify our theory to deal only with
functions that take one parameter.  The language Ruby contains a feature
that creates the curried version of a function; that is, if a function that
takes two parameters is given only one actual parameter, a {\em
function\/} that expects the other parameter will be returned.
Currying is also used in code optimization.  We can also implement currying
fairly easily in langauges that allow the free manipulation of functions
as lambda terms:
\newpage
\begin{verbatim}
// In C#
using System;
public class curry
{
  public static Func<A,Func<B,C>> Curry<A,B,C>(Func<A,B,C> f)
  {     return x => y => f(x,y);   }
  public static Func<A,B,C> Uncurry<A,B,C>(Func<A,Func<B,C>> g)
  {    return (x,y) => g(x)(y);    }

  public static int h(int x, int y) { return x+y; } // test functions
  public static Func<int,int> g(int x) { return y=>x*y; }   
  public static void Main()
  {
    Func<int,Func<int,int>> ch = Curry<int,int,int>(h);
    Console.WriteLine( ch(2)(3) );
    Console.WriteLine( Uncurry<int,int,int>(g)(4,5) ); 
  }//main
}


// in F#:
let Curry f = fun x -> fun y -> f(x,y);
let Uncurry g = fun (x,y) -> g x y;

let h(x:int,y:int) = x+y
let g x y = x*y
printfn "%d" (Curry h 2 3) 
printfn "%d" (Uncurry g (4,5));;

\end{verbatim}


\subsection*{Application}

The type inference rules above can be used in an algorithm to
determine if a program is well typed.  For example, let $\Gamma$ be the
type signature $\{ x:int, ~y:int, ~ z:char, ~u:double,~ atoi:char\rrr int\}$ 
We can infer that $x+atoi(z)$ has type int using these rules\footnote
{\verb+atoi+ is a C library function that converts chars to their ascii values.}

\[
\infer[app]{x+atoi(z) : int}
        {\infer{(x,atoi(z)):int * int}  
	      {x:int ~(\in \Gamma)&
	          \infer[app]{atoi(z):int} 
			{z:char ~(\in \Gamma) & atoi: char\rrr int}
              }
		& + : int*int\rrr int}
\]

Note that if we had $x+atoi(u)$ the inference above would fail because
the {\it app\/} rule cannot be applied to $atoi(u)$, since $double$
does not match the domain type of $atoi$ (char).  Also note how we
used the product rules to combine the two arguments of $+$ into one.

Now let's infer that the function f below
\begin{verbatim}
int g(int x, char y) { return x + atoi(y); }  // assume well-typed
int f(int x)
{
  return g(x,'a');
}
\end{verbatim}
is well-typed (that is, f has the type as declared).
Assume it's already been established that
function $g$ has type $int*char\rrr int$.

\[
\infer[abs]{f:int\rrr int}
   {\infer[app]{g(x,'a'),:int ~(assume ~ x:int)}
    {   \infer{(x,'a'):int*char} {x:int ~(assumed) & 'a':char ~(constant)}
	&
	g:int*char\rrr int ~ (previous ~inference)
    }
   }
\]


\subsection*{The Curry-Howard Isomorphism}

When we type check a program, we making sure that the program's structure
is logical.
We're not using the word {\em logical\/} gratuitously here.  Type theory
holds a close relationship with formal mathematical logic.
If we equate $\rrr$ with logical implication, product $*$ with
conjunction (and), and every atomic type (int, char, etc) as {\it
true,\/} then every type expression corresponds to a logical formula.
Applying the type checking rules above under a signature $\Gamma$ then
corresponds to deducing that something is true under a set of logical
assumptions.  This important correspondance is called the {\em
Curry-Howard Isomorphism.\/} It formally equates the process of
writing programs with the process of formulating mathematical proofs.
A particular consequence of this isomorphism is that {\em the type of
every typable pure lambda term (combinator) is a propositional
tautology.\/}

Unfortunately, not every lambda term is typable.  The untyped lambda
calculus is powerful enough to express all computations, but only a
subset of computations are considered ``type safe.''  In particular,
the ``bad'' lambda term that has no normal form when applied to
itself, namely $(\lambda x.x~x)$, is not typable.  To see why, apply
the type inference rules above to try and derive a general type.  We
first associate some type variable $\sigma$ temporarily with $x$. But
in applying the typing rule for applications (labeled $app$), we see
that in order for $x~x$ to be typable, $x$ must have type $\sigma$
{\em and\/} $\sigma \rrr \tau$ for some type $\tau$.  These types are
not compatible.  In fact, in pure typed lambda calculus every term is
guaranteed to have a normal form. You can't have infinite loops! We
cannot derive the fixed-point combinator for recursion - we must
import it as an addition to the calculus.

\subsection*{Typing Rules for Other Language Constructs}

  The rules above form the foundation of any type system.  Specific
langauges will require additional rules corresponding to the
constructs that are in that language.  For example, to type an
assignment statement (\verb+x=A;+)  you will need to introduce an inference
rule that checks that the left and right hand sides of \verb+=+ have the
same type.  Typing pointer expressions in C/C++ will require the following
rules:

\[
\infer{\& L : \tau *} {L: \tau} ~~~~~~~~~~~~~~~~~
\infer{*A : \tau} {A : \tau *}
\]
The first rule, however, does not distinguish $L$ as an {\em L-value,\/} which
is required before we place $\&$ before it.  Only L-values have well-defined
memory addresses.  The typing rules must be used with additional restrictions
of any given language.

Constructs such as nested $\{\}$'s in C can be modeled directly using
$\lambda$-terms, and can be typed directly.

Conditionals such as if-else are interesting.  We need to verify the
types of three elements: the boolean and the types of both options.
In many languages, the options for if-else are statements of type
\verb+void+.  However, we should really consider the type of
\verb+return+ construct as the type of the value that it returns. To
make matters consistent, we should not think of if-else constructs as
having type void, but rather the type of the values that it could
return.

\[
\infer {return~ A: \tau}{A: \tau}~~~~~~~~~~~~~~~~~
\infer{if ~(A)~ B~ else~ C : \tau}
{ A:bool & B:\tau & C:\tau
}
\]
In any typed language, you cannot have expressions such as 
\begin{center}
\verb+if (A) return "abc"; else return 2;+
\end{center}
although such expressions are legal (and sometimes useful) in untyped
languages such as Python.  The down side of the flexibility
of these languages is that it becomes impossible for the compiler to
detect type errors before runtime.

\subsection*{Typing Recursive Functions}

  Recursive functions are manifestations of mathematical induction in 
computing.  In type checking recursive code (tail or otherwise), we are
essentially doing an inductive proof.  Consider the factorial function:
\begin{verbatim}
unsigned int f(unsigned int n) 
  { if (n==1) return 1; else return n*f(n-1); }
\end{verbatim}
To prove that this function is well-typed for all positive integers,
we first show that $f(1)$ is well typed (the base case), and under the
{\em inductive hypothesis,\/} that $f(n-1)$ is well-typed: 

\[
\infer[app]{n*f(n-1) : uint}
  {\infer{(n,f(n-1)) : uint*uint}
      {  n:uint~ (\in \Gamma) & f(n-1):uint ~(ind.~ hypothesis)
      }   
    & *:uint*uint\rrr uint
  }
\]


\subsection*{Homework Assignment (optional)}

Using the typing rules described here, and following the examples shown
(both here and in class), show that the following program fragments are
well (or not well) typed:

1. 
\begin{verbatim}
int f(double x, char y);  // assume well-typed
...

int x;       
char y;
double z;
...
cout << (x+1) + f(z,y);   // type check this cout'ed expression.
\end{verbatim}
That is, under a type environment $\Gamma$ containing the declared
types for $f,x,y,z$, show that the expression in the cout statement
is well-typed.


2. \begin{verbatim}
int g(int x, int y)
{ 
  return 3 + (y*x);
}
\end{verbatim}

Please pay careful attention to how the rules should be applied and
write out everything clearly and carefully.  The type inference rules
may seem tedious but they have to be in order to form the basis of
an implementation, so observe them carefully.  Be mechanical.


\bigskip
\section*{Subtyping and Parametric Types}
 
 ``Subtype'' is the word used to describe inheritance in
type-theoretic research.  A subclass is a subtype of the
superclass. Types are related to sets in mathematics.  However, when
we speak of a ``class'' we are really talking about the {\em
description\/} of a set, not the set itself.  Thus the subclass is
seen as larger than the superclass, but in fact it describes a
tighter set. Types such as $int$ can also be considered a subtype of $double$,
because there's a well-defined injective function from ints to doubles.  
If a term $A$ is of type $\sigma$, which is a subtype of $\tau$, then 
$A$ is also of type $\tau$.  

A parametric type is a type expressions with variables, such <A> in C\#or 'a in F\#.
However, {\bf the rules of type checking described above can
also be used to check the consistency of parametrically typed code.}
Because of the relationship between logic and type theory, type
expressions with variables are often written as being (second order) universally
quantified with $\forall$.  For example, if a function is of type
$\forall a(a\rrr a)$, then the function can accept a value of any type
as a parameter, as long as the value it returns is of the same type.
If a function $f$ has type $\forall a(a\rrr a)$ but we write:
\begin{center}
\verb+ int x = f("abc");+
\end{center}
then we know this code is not typable {\em at compile time,\/} because
the single type variable $a$ cannot be instantiated with both \verb+int+ and
\verb+string+ at the same time.  

\subsection*{Type Inference}

  Just because a language has the syntax of types (C++) doesn't mean it
has a meaningful type system.  On the other hand, some languages may appear
to not require types in its syntax, but in fact the opposite is true. In
F\#, types are 
seldom used directly by programmers.  Instead, they're 
inferred from context.  For example, the (tail-recursive) factorial function
\begin{verbatim}
let rec fact = function
  | (0,ax) -> ax
  | (n,ax) when n>0 -> fact(n-1,n*ax)
\end{verbatim}
ML and F\# allow definitions of functions by cases, similar to Prolog
predicates and to a certain extent, the Visitor pattern in oop
languages.  But what is even more relevant is the absence of typing
keywords in the code (i.e, ``int'').  ML {\em infers\/} that the type
of this function is $int*int\rrr int$.  From the type of $1$ and $*$, it
infers that the parameters and the return value must all be integers.
The algorithm used for type inference is similar to the unification
algorithm used in Prolog and AI.  Furthermore, ML is able to infer
{\em Hindley-Milner type schemes,\/} which are types with generic type
variables.  The significance of this ability is profound.  It means
that ML can automatically recognize the {\em naturally polymorphic\/}
characteristics of programs.  For example, one can define the length
of a linked list in F\# as follows:
\begin{verbatim}
let rec length = function
  | [] -> 0
  | head::tail -> 1 + length(tail);
\end{verbatim}
F\# is able to infer that the type of this function is \verb+'a list ->
int+ where \verb+'a+ is a general type variable.  This means that the function
can be applied to linked lists containing data of any type.  In stark
contrast, the C++ type system is not powerful enough to even allow the
{\em expression\/} of natural polymorphism, let alone infer it.
Templates are not statically type checked.  Instead, a new copy of the
code is made for each new instantiation of the type variables,
regardless of whether a new piece of code is really necessary (such as
in the case of the length function).  Java is a little better, but you
have to write out the types yourself: it can't infer them.

ML is the language with which most of the applications of type theory
was researched.  One can think of ML as a typed version of Scheme: it
is based on the {\em typed\/} lambda calculus.  Slowly but surely, as
technology becomes available to support the overhead of advanced
language features, the research done with ML is finding its way into
more popular, conventional languages.  Generics were added to Java and C\#
around 2005, and now C\# has increased type inference capabilities.


{\flushleft\bf Exercise: }

a. Using the rules of logical inference, derive the most general type
(aka principal type scheme) of the S combinator,
lambda x.lambda y.lambda z.(x z)(y z)


Check your answer with F\#:

\verb+let S = fun x y z -> x z (y z):+

b. Verify that the type of S is a propositional tautology by constructing
a truth table.
\end{document}

