7 | | [Started Jan 2010.] |

| 7 | == Terminology == |

| 8 | |

| 9 | A type system is usually specified by |

| 10 | * A '''specification''', in the form of some '''declarative typing rules'''. These rules often involve "guessing types". Here is a typical example, for variables: |

| 11 | {{{ |

| 12 | (f : forall a1,..,an. C => tau) \in G |

| 13 | theta = [t1/a1, ..., tn/an] -- Substitution, guessing ti |

| 14 | Q |= theta( C ) |

| 15 | ------------------------- (VAR) |

| 16 | Q, G |- f :: theta(tau) |

| 17 | }}} |

| 18 | The preconditions say that f is in the environment G with a suitable polymorphic type. |

| 19 | We "guess" types t1..tn, and use them to instantiate f's polymorphic type variables |

| 20 | a1..an, via a substitution `theta`. Under this substitution f's instantiated constraints |

| 21 | `theta(C)` must be deducible (using `|=`) from the ambient constraints Q. |

| 22 | |

| 23 | The point is that we "guess" the ai. |

| 24 | |

| 25 | * An '''inference algorithm''', often also presented using similar-looking rules, but in a form that can be read as an algorithm with no "guessing". Typically |

| 26 | * The "guessing" is replaced by generating fresh unification variables. |