the expression. Substitution in typings The type order defined above can be extended to typings because the implied all-quantification of typings enables consistent replacement: Contrary to the specialisation rule, this is not part of the definition, but like the implicit all-quantification rather a consequence of the type rules defined next. Free type variables in a typing serve as placeholders for possible refinement. The binding effect of the environment to free type variables on the right hand side of that prohibits their substitution in the specialisation rule is again that a replacement has to be consistent and would need to include the whole typing. This article will discuss four different rule sets: declarative system syntactical system algorithm J algorithm W Deductive system The syntax of HM is carried forward to the syntax of the inference rules that form the body of the formal system, by using the typings as judgments. Each of the rules define what conclusion could be drawn from what premises. Additionally to the judgments, some extra conditions introduced above might be used as premises, too. A proof using the rules is a sequence of judgments such that all premises are listed before a conclusion. The examples below show a possible format of proofs. From left to right, each line shows the conclusion, the of the rule applied and the premises, either by referring to an earlier line (number) if the premise is a judgment or by making the predicate explicit. Typing rules The side box shows the deduction rules of the HM type system. One can roughly divide the rules into two groups: The first four rules (variable or function access), (application, i.e. function call with one parameter), (abstraction, i.e. function declaration) and (variable declaration) are centered around the syntax, presenting one rule for each of the expression forms. Their meaning is obvious at the first glance, as they decompose each expression, prove their sub-expressions and finally combine the individual types found in the premises to the type in the conclusion. The second group is formed by the remaining two rules and . They handle specialization and generalization of types. While the rule should be clear from the section on specialization above, complements the former, working in the opposite direction. It allows generalization, i.e. to quantify monotype variables not bound in the context. The following two examples exercise the rule system in action. Since both the expression and