Type inference is the process through which the Haskell compiler deduces the type of an expression or a function without requiring explicit type annotations from the programmer. Haskell’s type system is based on the Hindley-Milner type system, which is a powerful type inference system that provides strong static typing and support for polymorphism.
The mechanism behind Haskell’s type inference is based on unification and constraint solving. It starts by assigning unification variables (also called metavariables or type variables) to each expression in the program. These type variables represent the unknown types that the compiler needs to figure out. Then, it generates a set of equations expressing constraints over these type variables based on the structure of the program. Finally, it applies a unification algorithm to find a consistent substitution of the type variables in the constraint set. If successful, this substitution represents the inferred type signature of the expressions and functions.
To illustrate this process, let’s go through a simple example:
f x y = x + yThe function ‘f‘ takes two arguments, ‘x‘ and ‘y‘, and returns their sum. To determine the type variables, the compiler assigns a fresh type variable to each expression without a known type:
f :: α -> β -> γ
x :: α
y :: β
(+) :: δ -> ε -> ζNext, the compiler generates constraints based on the structure of the program. In this case, since ‘x‘ and ‘y‘ are used as arguments to ‘(+)‘, their types must be consistent with the types of ‘(+)‘. In Haskell, ‘(+)‘ has a type of ‘(Num a) => a -> a -> a‘, where ‘a‘ is a polymorphic type variable. Thus, we have the following constraints:
$$\begin{aligned}
\delta = \alpha \\
\epsilon = \beta \\
\zeta = \gamma \\
\alpha = \beta \\
\beta = \gamma \\
\text{Num } \alpha\end{aligned}$$
Now, we apply the unification algorithm to solve the constraints. The unification process replaces some of the type variables in the constraint set with others to obtain a consistent substitution:
$$\begin{aligned}
&\text{Substitution } S = \{ \delta \mapsto \alpha, \epsilon \mapsto \alpha, \zeta \mapsto \alpha, \beta \mapsto \alpha, \gamma \mapsto \alpha \}\end{aligned}$$
Finally, the inferred type signature of the function ‘f‘ can be obtained by applying the substitution ‘S‘ to its type metavariables:
$$\begin{aligned}
&\text{Applying } S \text{ to } f\text{'s type: } \alpha \to \beta \to \gamma \\
&f :: (\text{Num } \alpha) \Rightarrow \alpha \to \alpha \to \alpha\end{aligned}$$
As a result, the inferred type of the function ‘f‘ is ‘(Num a) => a -> a -> a‘. This means that ‘f‘ can work with any numeric type ‘a‘ in Haskell, such as ‘Int‘, ‘Integer‘, ‘Float‘, or ‘Double‘. This showcases the power of Haskell’s type inference and its support for polymorphic functions.