System F and the [[Hindley Milner Algorithm]] are both influential in the realm of type theory and functional programming languages, but they have distinct characteristics and applications.
System F, also known as the polymorphic lambda calculus, is a more expressive type system that allows for universal quantification over types. This means that in System F, you can have types that are parameterized by other types, and these type variables can be universally quantified at any position within the type. This flexibility allows for more powerful abstractions and type definitions, but it also makes type inference undecidable without explicit type annotations
On the other hand, the Hindley-Milner type system, also known as Damas-Milner, is a simpler and more practical type system used in many functional programming languages like ML and Haskell. Hindley-Milner supports parametric polymorphism, where types can be parameterized by other types, but the universal quantifiers must appear at the beginning of the type. This restriction simplifies type inference, making it decidable and allowing the system to infer the most general type of a given program without requiring type annotations from the programmer
While System F offers greater expressiveness and flexibility, it requires explicit type annotations due to the undecidability of type inference. Hindley-Milner, with its more restricted form of polymorphism, provides a practical balance by enabling efficient type inference without sacrificing too much expressiveness
System F has similar inference rules to Hindley-Milner, see the [[Hindley Milner Algorithm]] page for more information on how to read the below notation.
$
\begin{prooftree}
\AxiomC{}
\RightLabel{(Var)}
\UnaryInfC{$\Gamma, x: \tau \vdash x: \tau$}
\end{prooftree}
$
$ \begin{prooftree}
\AxiomC{$\Gamma, x: \tau_1 \vdash e: \tau_2$}
\RightLabel{(Abs)}
\UnaryInfC{$\Gamma \vdash \lambda x: \tau_1. e: \tau_1 \rightarrow \tau_2$}
\end{prooftree}
$
$
\begin{prooftree}
\AxiomC{$\Gamma \vdash e_1: \tau_1 \rightarrow \tau_2$}
\AxiomC{$\Gamma \vdash e_2: \tau_1$}
\RightLabel{(App)}
\BinaryInfC{$\Gamma \vdash e_1 e_2: \tau_2$}
\end{prooftree}
$
$
\begin{prooftree}
\AxiomC{$\Gamma \vdash e: \tau$}
\RightLabel{(Gen)}
\UnaryInfC{$\Gamma \vdash \Lambda \alpha. e: \forall \alpha. \tau$}
\end{prooftree}
$
$
\begin{prooftree}
\AxiomC{$\Gamma \vdash e: \forall \alpha. \tau$}
\RightLabel{(Inst)}
\UnaryInfC{$\Gamma \vdash e [\tau'] : \tau [\alpha := \tau']$}
\end{prooftree}
$