# Hindley Milner Type System [source: wikipedia] ## Monotypes Monotypes are "concrete" or known types. Monotypes can be: 1. Type constants (`'int` for example), often referred to as $\tau$. 2. parametric types (`'List`). Note that `'List 'int` is an *application* of a *type function* Two monotypes are considered equal if they have the same terms. `'List 'int` == `'List 'int`. ## Polytypes Polytypes (also called a type scheme) are types containing variables bound by for-all qualifiers. $\forall \alpha. \text{List}( \alpha ) \to int$ This type could be used to describe `Len()`, which takes an arbitrary list and returns an int. Polytypes are a generalization of monotypes. $\forall \alpha . \tau$ is an example of a monotype represented as a polytype. ## Context Monotypes require no solving. Polytypes are solved within a *context*. A context is a list of pairs $x : \sigma$ , i.e. assumptions. ## Typing Judgment A typing judgment is formed by combining a context with syntax and types. $\Gamma \vdash e : \sigma $ This judgment means that the expression $e$ has the type $\sigma$ under the context (assumptions) provided in $\Gamma$. Note the similarity to sequent calculus, with the exception that the RHS is not a disjunction. ## Free and bound types In a type $\forall \alpha_1 ... \forall \alpha_n.\tau$ , the forall symbol ($\forall$) is the *quantifier* binding the type variables $\alpha_i$ in the monotype $\tau$. The variables $\alpha_i$ are called *quantified* and any occurrence of a quantified type variable in $\tau$ is called *bound*. All unbound type variables in $\tau$ are called *free*. Put another way, a free type variable in a monotype is a type variable without a $\forall$ quantifier. A type can also be bound by occurring in the context. These contextual variables are basically constant monotypes within the expression. > The presence of both bound and unbound type variables is a bit uncommon in programming languages. Often, all type variables are implicitly treated all-quantified. For instance, one does not have clauses with free variables in [Prolog](https://en.wikipedia.org/wiki/Prolog "Prolog"). Likewise in Haskell, [[note 4]](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#cite_note-10) where all type variables implicitly occur quantified, i.e. a Haskell type `a -> a` means ∀α.α→α here. Related and also very uncommon is the binding effect of the right hand side σ of the assignments. ## Type Order Structure and decidability is introduced into this system via parametric polymorphism, and levels of generality are determined with substitution rules. A substitution is written as $S = \{\alpha \mapsto \beta\}$. For example, a substitution $S$ that attempts to apply $\text{string}$ to $\alpha$ would be written as $S = \{\alpha \mapsto \text{string} \}$ A type $\sigma '$ is more general than a type $\sigma$ (written as $\sigma' \sqsubseteq \sigma$ ), if some bound variable in $\sigma'$ can be substituted to achieve $\sigma$. We can show that $\forall \alpha.\alpha \to \alpha$ is more general than $\text{string} \to \text{string}$ by applying the above substitution $S$ and achieving $\text{string} \to \text{string}$. When applying substitutions on a parametric type, you must lift the quantifiers (type parameters) to the outer context. A principal type is the *most general* form of a given type expression. # Inference Rules ## Syntax A *predicate* is given in a context, and it one of three forms: 1. $\sigma \sqsubseteq \sigma'$ ($\sigma$ is *more general*, or subsumes, $\sigma'$); 2. $\alpha \notin free(\Gamma)$ ($\alpha$ is not in the set of free variables in the assumption set); 3. $x : \alpha \in \Gamma$ (expression $x$ is assumed to have the type $\alpha$ within $\Gamma$) A judgment is a typing. A premise is a judgment *or* predicate. A conclusion is a judgment. A rule takes the form ((premises/assumptions...) / conclusion) and a name. ## Rules Syntactical: 1. `Var`: accessing a variable or function 2. `App`: a function application with one parameter 3. `Abs`: an *abstraction*, a.k.a. function declaration 4. `Let`: variable declaration Specialization and generalization: 5. `Inst`: instantiates (narrows) a type 6. `Gen`: Quantifies monotype variables not bound in the context. # Algorithm J and W Type Inference Algorithm J is a sort of short-hand that relies on side effects, while Algorithm W is more complicated, formal, and eliminates side effects. # Hindley Milner Problem Set For these problems, write out the solution *and* the sequence of inference rules required to achieve that solution. #### Problem 1: Basic Type Inference Given the following expression, infer the type using the Hindley-Milner type system: $\text{let } \text{id} = \lambda x. x \text{ in } \text{id}$ >[!solution]- Solution For the expression `let id = λx. x in id`: > 1. Assign a type variable to `x`: $x : \alpha$ > 2. The type of `λx. x` is $\alpha \rightarrow \alpha$ > 3. Therefore, the type of `id` is $\forall \alpha. \alpha \rightarrow \alpha$ #### Problem 2: Function Application Infer the type of the following expression: $(\lambda f. \lambda x. f (f x)) (\lambda y. y + 1)$ >[!solution]- Solution > For the expression `(\lambda f. \lambda x. f (f x)) (\lambda y. y + 1)`: > 1. Assign type variables: $( f : \beta \rightarrow \beta ), ( x : \beta )$ > 2. The type of `λf. λx. f (f x)` is $(\beta \rightarrow \beta) \rightarrow (\beta \rightarrow \beta)$ > 3. The type of `λy. y + 1` is $\text{int} \rightarrow \text{int}$ > 4. Substitute and infer the type: $(\text{int} \rightarrow \text{int}) \rightarrow (\text{int} \rightarrow \text{int})$ #### Problem 3: Polymorphic Functions Consider the polymorphic function: $\text{let } \text{compose} = \lambda f. \lambda g. \lambda x. f (g x)$. Infer the type of the `compose` function. >[!solution]- Solution >For the function `let compose = λf. λg. λx. f (g x)`: >1. Assign type variables: $( f : \beta \rightarrow \gamma ), ( g : \alpha \rightarrow \beta ), ( x : \alpha )$ >2. The type of `compose` is $(\beta \rightarrow \gamma) \rightarrow (\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \gamma)$ #### Problem 4: Type Generalization Given the expression: $\text{let } \text{const} = \lambda x. \lambda y. x$. Infer the type of `const` and explain the process of type generalization. >[!solution]- Solution For the expression `let const = λx. λy. x` > 1. Assign type variables: $( x : \alpha ), ( y : \beta )$ > 2. The type of `λx. λy. x` is $\alpha \rightarrow (\beta \rightarrow \alpha)$ > 3. Generalize the type: $\forall \alpha \forall \beta. \alpha \rightarrow (\beta \rightarrow \alpha)$ #### Problem 5: Recursive Functions Infer the type of the following recursive function: $\text{let rec } \text{fact} = \lambda n. \text{if } n = 0 \text{ then } 1 \text{ else } n \times \text{fact} (n - 1)$ >[!solution]- Solution For the recursive function `let rec fact = λn. if n = 0 then 1 else n * fact (n - 1)`: > 1. Assign type variables: $( n : \text{int} )$ > 2. The type of `fact` is $( \text{int} \rightarrow \text{int} )$